[Agda] proofs with "with"

[Andrea Vezzosi]

The other difference with Peter's code is that your theorem-infinite
is a postulate, so Agda has an easier time figuring out that newNat L
in the goal type should be affected by "with theorem-infinite L".

The fact that newNat L reduces to succ (maximum L) is what's throwing
the implementation of "with" off here, It would need some kind of
currying transformation.

Cheers,
Andrea

On Mon, Dec 15, 2014 at 9:31 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda