[Agda] proofs with "with"

[Peter Selinger]

This is a newbie question. I am being driven mad by proofs about
definitions that use the "with" notation. The situation is typically
like this:

lemma : A -> B
lemma x with expr
lemma x | y = ?

Within the proof context '?', a variable y is available, of the same
type as expr. However, often, to complete the proof, one has to use
the fact that y == expr. This fact is obviously true, but typically
does not follow from anything in the proof context.

The "rewrite" notation does not help here, because its purpose is to
use an equation, not to prove one. 

Here is a concrete example (full definitions and proofs appended
below). I have defined an operation for computing the maximum of a
list of natural numbers:

maximum : (L : List Nat) -> Nat

I have also proved a lemma showing that the maximum is indeed an upper
bound for the list:

lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L

One can then easily prove a theorem stating that there are infinitely
many natural numbers:

theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)

Since existential witnesses are not very convenient to use, I'd like
to split this theorem into a first and second component: the first
component is a function computing a natural number not in a given
list, and the second component is the lemma saying that the number is
indeed not in the list:

-- Return a natural number not in L.
newNat : (L : List Nat) -> Nat
newNat L with theorem-infinite L
newNat L | ([ n , p ]) = n

-- The defining property of newNat.
lemma-newNat : (L : List Nat) -> newNat L ∉ L
lemma-newNat L with theorem-infinite L
lemma-newNat L | ([ n , p ]) = ?

However, I cannot complete the last proof. In principle, the question
mark should just be "p". However, the prover (modulo beta reduction)
serves

Goal: newNat L ∉ L

as the goal, and gives

p : n ∉ L
n : Nat
L : List Nat

as the hypotheses. Obviously, [ n , p ] was obtained by pattern
matching theorem-infinite L, so we know that

[ n , p ] == theorem-infinite L.

>From this, we could immediately conclude that newNat L == n, which
would immediately prove the goal. But I have not been able to find any
combination of dot-patterns that the type checker would actually
accept.

Two questions:

(1) what is the concrete solution to my problem?

   I realize that I can solve the problem by defining general first
   and second projections from the existential type:
   
   ∃fst : {A : Set} {B : A -> Set} -> ∃[ x ∈ A ] B x -> A
   ∃snd : {A : Set} {B : A -> Set} -> (p : ∃[ x ∈ A ] B x) -> B (∃fst p) 

   and then I can just define newNat and lemma-newNat in terms of
   these. However, I am more concerned with what one can do when one
   is stuck in a proof context, rather than such an "external"
   solution to the problem.

(2) why doesn't Agda do the obvious, namely, when matching a "with"
    expression "expr" against a pattern "p", just add the equation
    "expr == p" to the proof context? Is there an existing mechanism
    that can achieve this?

Thanks, -- Peter

Here's the full example. It requires no libraries.

module InfNat where

-- Falsity.
data False : Set where
  -- no constructors.

-- Negation.
Not : Set -> Set
Not A = A -> False

-- Existential quantifier.
data Exists (A : Set) (B : A -> Set) : Set where
  [_,_] : (a : A) -> B a -> Exists A B
syntax Exists A (λ x -> B) = ∃[ x ∈ A ] B

-- The natural numbers.
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- Order.
data _<=_ : Nat -> Nat -> Set where
  z<=n : ∀ {n} → zero <= n
  s<=s : ∀ {m n} (m<=n : m <= n) → succ m <= succ n

-- Order is reflexive.
lemma-order-refl : ∀ {n} -> n <= n
lemma-order-refl {zero} = z<=n
lemma-order-refl {succ n} = s<=s lemma-order-refl

-- Order is transitive.
lemma-order-trans : ∀ {n m k} -> n <= m -> m <= k -> n <= k
lemma-order-trans z<=n q = z<=n
lemma-order-trans (s<=s p) (s<=s q) = s<=s (lemma-order-trans p q)

-- Successor is not smaller.
lemma-order-succ : ∀ {n} -> Not (succ n <= n)
lemma-order-succ (s<=s h) = lemma-order-succ h

-- The maximum of two numbers.
max : Nat -> Nat -> Nat
max zero m = m
max n zero = n
max (succ n) (succ m) = succ (max n m)

-- Introduction rules for maximum.
lemma-max-intro1 : ∀ n m -> n <= max n m
lemma-max-intro1 zero m = z<=n
lemma-max-intro1 (succ n) zero = lemma-order-refl
lemma-max-intro1 (succ n) (succ m) = s<=s (lemma-max-intro1 n m)

lemma-max-intro2 : ∀ n m -> m <= max n m
lemma-max-intro2 zero m = lemma-order-refl
lemma-max-intro2 (succ n) zero = z<=n
lemma-max-intro2 (succ n) (succ m) = s<=s (lemma-max-intro2 n m)

-- Lists.
data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

-- Membership.
data _∈_ {A : Set} (x : A) : (B : List A) -> Set where
  mem-head : {xs : List A} -> x ∈ (x :: xs)
  mem-tail : {xs : List A} {y : A} -> x ∈ xs -> x ∈ (y :: xs)

-- Not member.
_∉_ : {A : Set} -> (x : A) -> (B : List A) -> Set 
x ∉ B = Not (x ∈ B)

-- Calculate the maximum of a list of numbers.
maximum : (L : List Nat) -> Nat
maximum [] = zero
maximum (n :: L) = max n (maximum L)

-- The maximum is an upper bound.
lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L
lemma-maximum (n :: L) .n mem-head = lemma-max-intro1 n (maximum L)
lemma-maximum (n :: L) m (mem-tail p) = lemma-order-trans (lemma-maximum L m p) (lemma-max-intro2 n (maximum L))

-- Theorem: there are infinitely many natural numbers.
theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)
theorem-infinite L = [ n , p ]
  where
    n = succ (maximum L)
    p : n ∉ L
    p h = let q = lemma-maximum L n h in lemma-order-succ q

-- Return a natural number not in L.
newNat : (L : List Nat) -> Nat
newNat L with theorem-infinite L
newNat L | ([ n , p ]) = n

-- The defining property of newNat.
lemma-newNat : (L : List Nat) -> newNat L ∉ L
lemma-newNat L with theorem-infinite L
lemma-newNat L | ([ n , p ]) = {!!}