R-Ragionamento e modelli "con"

Question

Stavo dimostrando alcune proprietà di filter e map, tutto è andato abbastanza bene fino a quando non sono inciampato in questa proprietà: filter p (map f xs) ≡ map f (filter (p ∘ f) xs). Ecco una parte del codice che è rilevante:

open import Relation.Binary.PropositionalEquality 
open import Data.Bool 
open import Data.List hiding (filter) 

import Level 

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A 
filter _ [] = [] 
filter p (x ∷ xs) with p x 
... | true = x ∷ filter p xs 
... | false = filter p xs 

Ora, perché amo la scrittura di prove utilizzando il modulo ≡-Reasoning, la prima cosa che ho provato è stato:

open ≡-Reasoning 
open import Function 

filter-map : ∀ {a b} {A : Set a} {B : Set b} 
      (xs : List A) (f : A → B) (p : B → Bool) → 
      filter p (map f xs) ≡ map f (filter (p ∘ f) xs) 
filter-map []  _ _ = refl 
filter-map (x ∷ xs) f p with p (f x) 
... | true = begin 
    filter p (map f (x ∷ xs)) 
    ≡⟨ refl ⟩ 
    f x ∷ filter p (map f xs) 
-- ... 

Ma, ahimè, che non ha funzionato . Dopo aver provato per un'ora, Alla fine ho rinunciato e si è dimostrato in questo modo:

filter-map (x ∷ xs) f p with p (f x) 
... | true = cong (λ a → f x ∷ a) (filter-map xs f p) 
... | false = filter-map xs f p 

Ancora curioso di sapere il motivo per passare attraverso ≡-Reasoning non ha funzionato, ho provato qualcosa di molto banale:

filter-map-def : ∀ {a b} {A : Set a} {B : Set b} 
       (x : A) xs (f : A → B) (p : B → Bool) → T (p (f x)) → 
       filter p (map f (x ∷ xs)) ≡ f x ∷ filter p (map f xs) 
filter-map-def x xs f p _ with p (f x) 
filter-map-def x xs f p() | false 
filter-map-def x xs f p _ | true = -- not writing refl on purpose 
    begin 
    filter p (map f (x ∷ xs)) 
    ≡⟨ refl ⟩ 
    f x ∷ filter p (map f xs) 
    ∎ 

Ma typechecker non è d'accordo con me. Sembrerebbe che l'obiettivo corrente rimanga filter p (f x ∷ map f xs) | p (f x) e anche se il modello corrisponde allo p (f x), filter non si ridurrà a f x ∷ filter p (map f xs).

C'è un modo per farlo funzionare con ≡-Reasoning?

Grazie!

Answer 1

Il problema con with -clausi è che Agda dimentica le informazioni apprese dalla corrispondenza del modello a meno che non si disponga in anticipo affinché tali informazioni vengano conservate.

Più precisamente, quando Agda vede una clausola with expression, sostituisce tutte le occorrenze di expression nel contesto attuale e l'obiettivo con una variabile nuova w e poi ti dà quella variabile con il contesto aggiornato e obiettivo nel con-clausola, dimenticando tutto sulla sua origine

Nel tuo caso, si scrive filter p (map f (x ∷ xs)) all'interno del con-blocco, così si va in ambito dopo Agda ha eseguito la riscrittura, in modo Agda ha già dimenticato il fatto che p (f x) è true e non riduce il termine.

È possibile conservare la dimostrazione di uguaglianza utilizzando uno dei modelli "Ispeziona" dalla libreria standard, ma non sono sicuro di come possa essere utile nel vostro caso.