Доказательство `T b`, когда` b` уже совпадает с

Я пытаюсь доказать простое:

open import Data.List
open import Data.Nat
open import Data.Bool
open import Data.Bool.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Unit

repeat : ∀ {a} {A : Set a} → ℕ → A → List A
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x

Я думал, что доказать filter-repeat будет легко, сопоставив шаблон на p x:

filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x
filter-repeat p x () (suc n) | false
filter-repeat p x prf (suc n) | true  = cong (_∷_ x) (filter-repeat p x prf n)

Однако он жалуется, что prf : ⊤ не относится к типу T (p x). Итак, я подумал, хорошо, это похоже на знакомую проблему, давайте разберемся inspect:

filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true  | [ eq ] rewrite eq = cong (_∷_ x) (filter-repeat p x {!!} n)

но, несмотря на rewrite, тип отверстия по-прежнему T (p x) вместо T true. Это почему? Как уменьшить его тип до T true, чтобы заполнить tt?

Временное решение

Мне удалось обойти это, используя T-≡:

open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true  | [ eq ] = cong (_∷_ x) (filter-repeat p x (Equivalence.from T-≡ ⟨$⟩ eq) n)

но я все же хотел бы понять, почему решение на основе inspect не работает.


boolean inspect agda
person Cactus    schedule 08.04.2016    source источник

Ответы (2)


arrow_upward
5
arrow_downward

Как говорит Андраш Ковач, индуктивный регистр требует, чтобы prf имел тип T (p x), хотя вы уже изменили его на просто ⊤ путем сопоставления с образцом на p x. Одно простое решение - просто вызвать filter-repeat рекурсивно перед сопоставлением с образцом на p x:

open import Data.Empty

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf  0      = refl
filter-repeat p x prf (suc n) with filter-repeat p x prf n | p x
... | r | true  = cong (x ∷_) r
... | r | false = ⊥-elim prf

Иногда также может быть полезно использовать шаблон защиты:

data Protect {a} {A : Set a} : A → Set where
  protect : ∀ x → Protect x

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x q  0      = refl
filter-repeat p x q (suc n) with protect q | p x | inspect p x
... | _ | true  | [ _ ] = cong (x ∷_) (filter-repeat p x q n)
... | _ | false | [ r ] = ⊥-elim (subst T r q)

protect q сохраняет тип q от перезаписи, но это также означает, что в случае false тип q по-прежнему T (p x), а не ⊥, отсюда и дополнительный inspect.

Другой вариант той же идеи:

module _ {a} {A : Set a} (p : A → Bool) (x : A) (prf : T (p x)) where
  filter-repeat : ∀ n → filter p (repeat n x) ≡ repeat n x
  filter-repeat  0      = refl
  filter-repeat (suc n) with p x | inspect p x
  ... | true  | [ r ] = cong (x ∷_) (filter-repeat n)
  ... | false | [ r ] = ⊥-elim (subst T r prf)

module _ ... (prf : T (p x)) where также предотвращает перезапись типа prf.

person user3237465    schedule 08.04.2016

arrow_upward
3
arrow_downward

Зависимое сопоставление с образцом влияет только на цель и контекст в точном месте их использования. Сопоставление p x обновляет текущий контекст и уменьшает тип prf до ⊤ в ветви true.

Однако, когда вы выполняете рекурсивный вызов filter-repeat, вы снова указываете здесь x в качестве аргумента, и T (p x) в filter-repeat зависит от этого x, а не от старого во внешнем контексте, хотя они по определению равный. Мы могли бы передать что-то другое, кроме x, гипотетически, поэтому нельзя делать никаких предположений об этом до вызова filter-repeat.

x можно сделать инвариантным в контексте, вычленив его из индукции:

open import Data.Empty

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf = go where
  go : ∀ n → filter p (repeat n x) ≡ repeat n x
  go zero    = refl
  go (suc n) with p x | inspect p x
  go (suc n) | true  | [ eq ] = cong (_∷_ x) (go n)
  go (suc n) | false | [ eq ] = ⊥-elim (subst T eq prf)
person András Kovács    schedule 08.04.2016