[Agda] proofs with "with"

[Peter Selinger]

Thanks to all who replied.

Liam O'Connor wrote:
> 
> You probably want to use the “inspect” idiom.
> 
> See here:
> 
> https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/PropositionalEquality.agda
> 
> Under “inspect on steroids”

Yes, that is exactly the kind of thing I was looking for.

Wolfram Kahl wrote:
> The "with" notation just generates an auxiliary function;
> it is usually only a minor nuisance to generate that function
> yourself.

Point well taken. Although writing the auxiliary function by hand does
not entirely make the problem go away. In my example, if I write

  aux : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L) -> newNat L ∉ L
  aux L [ n , p ] = ?

  lemma-newNat : (L : List Nat) -> newNat L ∉ L
  lemma-newNat L = aux L (theorem-infinite L)

then in the context "?", I still end up with the hypothesis n ∉ L and
the goal newNat L ∉ L, and no way to prove it. So I must pass the
required equality as an additional argument to aux, like this:

  aux : (L : List Nat) -> (x : ∃[ n ∈ Nat ] (n ∉ L)) -> x == theorem-infinite L -> newNat L ∉ L
  aux L [ n , p ] eq = ?

  lemma-newNat : (L : List Nat) -> newNat L ∉ L
  lemma-newNat L = aux L (theorem-infinite L) refl

At this point, the solution is essentially equivalent to what
"inspect" does, and arguably the auxiliary function has not increased
transparency.

-- Peter

> On 15 December 2014 at 4:28:07 pm, Peter Selinger (selinger at mathstat.dal.ca) wrote:
> 
> 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 ]) = {!!}