[Agda] ordering uniqueness

[Sergei Meshveliani]

On Thu, 2013-10-10 at 01:10 +0200, 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.
> 

I have an impression that this is a similar problem as I had with the 
type  
         data Power (x : C) (e : Nat)

with the three constructors.
(This represents the algorithm for binary exponentiation. I succeeded
with the proofs based on it. But the proof is lengthy, and using the 
library conversion to Bin allows a much shorter proof). 


Each type  Power x e  has a unique value. And I needed to start with a
proof for 
      e == e' -> (s : Power x e) -> s' : (Power x e') ->
                                         extractV s == extractV s' 

And I was forced to write 12 large clauses with the same head function
name. I hoped for using dotted patterns, but failed to make them work.

Regards,

------
Sergei