The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Le 10/12/2014 01:53, Saulo Araujo a écrit :
> Hi,
>
> I need to compare values of the type PATH defined below
>
> Definition ID := string.
>
> Inductive STEP : Type :=
>   | LastStep : ID -> STEP | Step : ID -> PATH -> STEP | Init : ID -> STEP
> with PATH : Type := Path : list STEP -> PATH.
>
> Is there a way to compare those values in Gallina like we compare them 
> in SML?
>
> I tried the suggestion in 
> http://stackoverflow.com/questions/6636131/searching-through-a-list-recursively-in-coq
>
> Definition PATH_dec : forall x y : ID, {x = y} + {x <> y}.
I guess you want x y : PATH instead...

> Proof. decide equality. Defined.
To prove this, you need to proceed by induction on PATH. Unfortunately, 
the induction principle automatically generated by Coq is not correct 
because Coq does not recognize the argument of Path as recursive. But 
you can redefine it yourself by using "fix". See for instance the file 
Term/Varyadic/VTerm.html in http://color.inria.fr 
(http://color.inria.fr/doc/CoLoR.Term.Varyadic.VTerm.html does not 
contain proofs). You also need list_eq_dec and string_dec in the List 
and String modules.

Best regards,

Frédéric.

> but Coq says Error: Attempt to save an incomplete proofCompilation output:
>
> Thanks in advance,
> Saulo