[Agda] proofs with "with"

[Sergei Meshveliani]

On Mon, 2014-12-15 at 01:27 -0400, Peter Selinger 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)
> [..]


The difference to my code below is only that I do not use the `['
brackets 
(I am half a newbie, and do not know whether "∃[ n ∈ Nat ]" or 
"([ n , p ])"  is allowed in Agda).

At least, the below code is type-checked:

-------------------------------------------------------------------
module TT where
open import Relation.Binary.PropositionalEquality as PE using ()
open import Data.Product  using (∃; _,_)
open import Data.List     using (List)
open import Data.List.Any using (Any; module Any; module Membership)
open import Data.Nat      using (ℕ; _≤_)

open Any
open Membership (PE.setoid ℕ)

postulate
  maximum : (L : List ℕ) → ℕ

  lemma-maximum : (L : List ℕ) → ∀ m → m ∈ L → m ≤ maximum L

  theorem-infinite : (L : List ℕ) -> ∃ (\n → n ∉ L)

newNat : (L : List ℕ) → ℕ
newNat L with theorem-infinite L
newNat L | (n , _) = n

lemma-newNat : (L : List ℕ) → newNat L ∉ L
lemma-newNat L with theorem-infinite L
lemma-newNat L | (_ , n∉L) = n∉L
--------------------------------------------------------------------

This is exactly of what you wrote.


Another point
-------------
I use this style in most cases: 

  maximum :  ∀ x xs → ∃ (\m →  m ∈ (x ∷ xs) × All (_≥_ m) (x ∷ xs))
  maximum x xs = ...

This is both a notion definition and an implementation.
This often reduces repetition of the code fragments.
  
Regards,

------
Sergei











I do not know