[Agda] proofs with "with"

[Wolfram Kahl]

Hallo Peter,

On Mon, Dec 15, 2014 at 01:27:26AM -0400, Peter Selinger wrote:
> This is a newbie question. I am being driven mad by proofs about
> definitions that use the "with" notation.

My pragmatic suggestion: Don't!  ;-)

That is, it usually makes your life easier if you don't use "with"
in definitions that you later will want to prove something about.


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

(Sometimes, Function.case_of_ with a pattern-matching lambda
 is also an alternative (with the disadvantage that the auxiliary function
 does not have a name of your choice).
)


Wolfram



P.S.: If you redo your example with Data.Product from the standard library,
  then

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

becomes

newNat L = proj_1 (theorem-infinite L)