Доказывая `T b`, когда` b` уже согласованы на

Question

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

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 не работает.

Answer 1

Как Андраш Ковач говорит индуктивный случай требует 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 

Она также может быть иногда полезно использовать the protect pattern:

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 от быть переписано, как хорошо.

Answer 2

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

Однако, когда вы делаете рекурсивный filter-repeat вызов, снова поставить x в качестве аргумента там, и T (p x) в filter-repeat зависит от чтоx, а не старый во внешнем контексте, даже если они равны definitionally , Мы могли бы пройти нечто, отличное от 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)