Imports:
open import Data.Nat using (ℕ; zero; suc)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.List using (List; _∷_; [])
Example 1:
postulate
a : ℕ
p : a ≡ zero
b : ℕ
b with a
... | zero = zero
... | _ = suc zero
q : b ≡ zero
q = ?
This is a minimum working example. If I want to prove q, how should I fill the hole?
The part that I'm clueless about, is how to reason, in the proof of q, about the pattern matching that happened in b. I don't know of any syntax that allows me to do this (I'm not very familiar with Agda).
Example 2 (slightly more complex):
postulate
a : List ℕ
p : a ≡ zero ∷ []
b : List ℕ
b with a
... | zero ∷ ns = ns
... | _ = []
q : b ≡ []
q = ?
Again, if I want to prove q, how should I fill the hole?
Difference between example 1 & 2: In example 1 we only care about "which branch in the with-abstraction was entered", while in example 2 we also care about "what was the value ns resulted from the pattern matching". I'm not sure if this is a relevant difference though.
You're going to make your life complete hell if you define implicit functions like this. Why not make b an actual function of a instead? Plus, reasoning with incomplete cases is harder too. But here's a solution to your first puzzle:
b : ℕ
b with a
... | zero = zero
... | suc _ = suc zero -- first change
q : b ≡ zero
q = Eq.trans (Eq.sym (f≡b a Eq.refl)) (r a p)
where
f : ℕ → ℕ
f zero = zero
f (suc _) = suc zero
r : (x : ℕ) → x ≡ zero → f x ≡ zero
r .zero Eq.refl = Eq.refl
f≡b : ∀ x → x ≡ a → f x ≡ b
f≡b .a Eq.refl with a
... | zero = Eq.refl
... | suc x = Eq.refl
Note how my answer was essentially forced to make a function f that is equivalent to b? There's probably some convoluted way to do this with with and inspect too, but I can't quite see it.
To work in the same file, your question is:
postulate
a′ : List ℕ
p′ : a′ ≡ zero ∷ []
c : List ℕ
c with a′
... | zero ∷ ns = ns
... | suc _ ∷ _ = []
... | [] = []
qq : c ≡ []
qq = {!!}
Which is simply not worth it. Instead, compare how easy this is:
cc : List ℕ → List ℕ
cc [] = []
cc (zero ∷ ns) = ns
cc ((suc _) ∷ _) = []
qqq : (x : List ℕ) → x ≡ zero ∷ [] → cc x ≡ []
qqq .(zero ∷ []) Eq.refl = Eq.refl