Proving `T b 'wenn' b 'bereits auf

Question

abgestimmt ist Ich versuche, etwas einfach zu beweisen:

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 

dachte ich beweisen filter-repeat durch Muster auf p x passend zu leicht sein wird:

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) 

Allerdings beschwert sich prf : ⊤ nicht vom Typ T (p x). Also dachte ich, OK, das wie ein bekanntes Problem scheint, lassen Sie uns inspect zücken:

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) 

aber trotz der rewrite, die Art des Lochs ist noch T (p x) statt T true. Warum das? Wie reduziere ich den Typ auf T true, damit ich es mit tt füllen kann?

Umgehung

konnte ich durch T-≡ mit um ihn arbeiten:

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) 

aber ich würde immer noch zu verstehen, warum die inspect -basierte Lösung funktioniert nicht.

Answer 1

Als András Kovács sagt der induktive Fall erfordert prf von T (p x) Typ zu sein, während Sie es bereits geändert haben zu nur ⊤ durch Musterabgleich auf p x. Eine einfache Lösung ist nur filter-repeat ruft rekursiv vor Pattern-Matching auf 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 

Es kann auch manchmal hilfreich sein, verwenden 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 speichert die Art des q von neu geschrieben werden, aber es bedeutet auch, dass in dem false Fall der Typ immer noch T (p x) statt ⊥ ist, daher der zusätzliche inspect.

Eine weitere Variante der gleichen Idee ist

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 als auch die Art der prf von umgeschrieben verhindert.

Answer 2

Der abhängige Musterabgleich wirkt sich nur auf das Ziel und den Kontext genau an der Verwendungsstelle aus. Matching on p x schreibt den aktuellen Kontext um und reduziert den Typ prf auf ⊤ im Zweig true.

Wenn Sie jedoch die rekursive filter-repeat Anruf tun, Sie noch einmal x als Argument liefern dort, und T (p x) in filter-repeat hängt von dassx, nicht die alte im äußeren Rahmen, auch wenn sie definitorisch gleich sind . Wir hätten hypothetisch etwas anderes als x passieren können, also kann vor dem filter-repeat Aufruf keine Annahme darüber gemacht werden.

x kann es im Rahmen unveränderlich gemacht werden aus der Induktion durch Factoring:

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)