The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

Hi Assia, 

Thank you for your help. 

You have changed a bit the specification of the problem 

but I guess I should be able to do a similar change in 

my coq development, and it makes sense.

Best,

-- Nicolas

On Sat, Apr 11, 2015 at 12:32 AM, Assia Mahboubi <Assia.Mahboubi AT inria.fr> wrote:

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.
>

--

Nicolas Tabareau
Researcher at Inria
Ascola Group, Nantes