[Agda] proofs with "with"

[Peter Selinger]

Sorry, I was obviously asleep when I responded to Wolfram's suggestion
last night. He had suggested eliminating "with" from the definition,
and I only eliminated "with" from the lemma instead.

When I am actually awake and do as Wolfram said, it does indeed work
correctly. First, I eliminate "with" from the lemma like this:

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

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

Then the proof works just fine, like this:

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

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

The point is that in this case, the auxiliary lemma states a more
general property of the auxiliary function; namely, it states that
(newNat-aux L x ∉ L), rather than the less general (newNat L ∉ L).
This can then be proved without using any "inspect"-like feature.

-- Peter

Peter Selinger wrote:
> 
> 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 ]) = {!!}  
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>