Proving `T b` quando` B` è già abbinato a

Question

sto cercando di dimostrare qualcosa di semplice:

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 

ho pensato dimostrando filter-repeat sta per essere facile da pattern matching on 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) 

Tuttavia questo si lamenta che prf : ⊤ non è di tipo T (p x). Così ho pensato, ok, questo sembra un problema familiare, cerchiamo di tirar fuori 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) 

ma nonostante il rewrite, il tipo di foro è ancora T (p x) invece di T true. Perché? Come faccio a ridurne il tipo a T true in modo che possa riempirlo con tt?

Soluzione

sono stato in grado di lavorare intorno ad esso utilizzando 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) 

ma mi piace ancora di capire il motivo per cui la soluzione basata su inspect non funziona.

Answer 1

Come András Kovács dice che il caso richiede induttiva prf essere di tipo T (p x) mentre hai già stata modificata a solo ⊤ per corrispondenza di modelli su p x. Una soluzione semplice è solo per chiamare filter-repeat ricorsivamente prima di pattern matching on 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 

Anche può a volte essere utile utilizzare 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 salva il tipo di q di essere riscritto, ma significa anche che nel caso false il tipo di q è ancora T (p x) anziché ⊥, da cui l'ulteriore inspect.

Un'altra variante della stessa idea è

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 impedisce il tipo di prf vengano riscritti pure.

Answer 2

La corrispondenza del modello dipendente influisce solo sull'obiettivo e sul contesto nel punto esatto del loro utilizzo. Corrispondenza su p x riscrive il contesto corrente e riduce il tipo di prf a ⊤ nel ramo true.

Tuttavia, quando si fa il ricorsiva filter-repeat chiamata, è ancora una volta fornire x come argomento lì, e T (p x) in filter-repeat dipende chex, non quello vecchio nel contesto esterno, anche se sono per definizione pari . Potremmo aver superato qualcosa di diverso da x, ipoteticamente, quindi non è possibile formulare alcuna ipotesi al riguardo prima della chiamata filter-repeat.

x può essere fatto invariante nel contesto dal factoring fuori dalla induzione:

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)