In Agda, how to prove properties about matched patterns in with-abstractions?

Question

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.

user_278132 · Answer

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

In Agda, how to prove properties about matched patterns in with-abstractions?

1 Answers