[Agda] ordering uniqueness

[Marco Maggesi]

Hello Twan,

thank you for your nice solution and for taking the time to write it.
It teaches me a lot of things!

In fact, the induction on m and n was my first attempt, but for some reason
I failed to finish the proof (probably I mechanically performed case
analysis also on x and y in the hope to "clarify" the hypothesis but I got
lost instead).

Marco


2013/10/10 Twan van Laarhoven <twanvl at gmail.com>

> Hello Marco,
>
>
> I think this is easiest to prove by induction on m and n. See the
> attachment for my alternative proof.
>
> I just typed in the theorem, used C-c,C-c to split on m and n. The only
> interesting case is (suc m) (suc n). There you need induction, together
> with some lemmas to show that this is actually possible. To prove the
> lemmas, again I used case splitting together with auto to fill in the right
> hand side.
>
>
> As a remark on style, the case splitting often exposes hidden variables
> with irrelevant arguments. You can often clean that up quite a bit. For
> example your 'swap' function can be written as just
>
>     swap : ∀ {m n} → Ordering m n → Ordering n m
>     swap (less m k) = greater m k
>     swap (equal n) = equal n
>     swap (greater n k) = less n k
>
>
> Twan
>
>
> On 10/10/13 00:10, Marco Maggesi wrote:
>
>> Hello!
>>
>> I'm new to Agda.
>> I wrote a proof of the following theorem
>> ​ (see
>> attached file)​:
>>
>>
>> ​  ​
>> ordering-uniqueness : {m n : ℕ} {x y : Ordering m n} → x ≡ y
>>
>> I'd be interested to see if there
>> ​are​
>>   simpler proof
>> ​s​ of the same fact.
>> Also general remarks about idiom and style are welcome.
>>
>> Thanks,
>> Marco
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>
> _______________________________________________
> 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/20131011/43ac404a/attachment.html