[Agda] proofs with "with"

[Liam O'Connor]

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”



-- 
Liam O'Connor
Sent with Airmail

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  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141215/9ba41c7d/attachment.html