The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Hi Nicolas,

  with an isomorphic version of type GS1, things seem much easier (see the
attachment).

I guess I would need more context to know if this remark is of any help beyond
the toy example.

Best,

assia

Le 09/04/2015 17:22, nicolas tabareau a écrit :
> order and (L) are ok.
> 
> Definition order: forall {x y}, GS1 x y -> nat :=
>   fun x y =>
>     match decpaths_nat x y as z return
>           match z with inl _ => nat | inr _ => False end -> nat with
>       | inl _ => fun (n:nat) => n
>       | inr _ => fun (abs:False) => match abs return nat with end
>     end.
> 
> Definition L x y : forall (g h : GS1 x y), order g = order h -> g = h.
>   unfold GS1, order.
>   destruct (decpaths_nat x y); intros.
>   - exact H.
>   - destruct g.
> Defined.
>  
> 
>     The proof of "order (Compo a b) = order b + order a" might be a little
>     tricky, I did not tried it.
> 
> 
> This seems just to have change the dependent issue to this new lemma 
> which I don't know how to prove ...
>  
> 
>     Also, I would add, that I am not very found of the use of terms defined 
> with
>     tactics, when the definition is relevant.
>     Such terms tend to be quite big, and totally unreadable. Having a "nice"
>     definition of Compo could also help you in your proofs.
> 
> 
> Agreed, I usually avoid it too. But here I think the definition will look 
> the same,
> except maybe for the rewrite if I use a transport.
>

Attachment: nicolas.v
Description: application/save-to-disk