[Agda] ordering uniqueness

[Twan van Laarhoven]

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
>

-------------- next part --------------
module 2013-10-10-ordering-uniqueness where

open import Function
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

ordering-suc : {m n : ℕ} → Ordering m n → Ordering (suc m) (suc n)
ordering-suc (less m k) = less (suc m) k
ordering-suc (equal m) = equal (suc m)
ordering-suc (greater m k) = greater (suc m) k

ordering-pred : {m n : ℕ} → Ordering (suc m) (suc n) → Ordering m n
ordering-pred (less ._ k) = less _ k
ordering-pred (equal ._) = equal _
ordering-pred (greater ._ k) = greater _ k

ordering-suc-pred : {m n : ℕ} → (x : Ordering (suc m) (suc n)) → ordering-suc (ordering-pred x) ≡ x
ordering-suc-pred (less ._ _) = refl
ordering-suc-pred (equal ._) = refl
ordering-suc-pred (greater ._ _) = refl

ordering-unique : (m n : ℕ) (x y : Ordering m n) → x ≡ y
ordering-unique zero zero (equal .0) (equal .0) = refl
ordering-unique zero (suc n) (less .0 .n) (less .0 .n) = refl
ordering-unique (suc m) zero (greater .0 .m) (greater .0 .m) = refl
ordering-unique (suc m) (suc n) x y = 
  sym (ordering-suc-pred x) ⟨ trans ⟩
  cong ordering-suc (ordering-unique m n (ordering-pred x) (ordering-pred y)) ⟨ trans ⟩
  ordering-suc-pred y

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