The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

I think the problem is that STEP and PATH refer to one another:

Inductive STEP : Type := 

  | LastStep : ID -> STEP | Step : ID -> PATH -> STEP | Init : ID -> STEP

with PATH : Type := Path : list STEP -> PATH.

Is "repeat decide equality tactic" supposed to handle such cases?

Thanks,

Saulo

On Tue, Dec 9, 2014 at 11:41 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:

Hi Nuno,

Does your suggestion defines equality for ID and not for PATH? I tried (note that x and y are of PATH type)

Definition PATH_dec : forall x y : PATH, {x = y} + {x <> y}.

Proof. repeat decide equality. Defined.

But then Coq seems to enter in some kind of very heavy task because after some minutes it still did not finish compiling...

Saulo

On Tue, Dec 9, 2014 at 10:48 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Hi.

try

Definition PATH_dec : forall x y : ID, {x = y} + {x <> y}.

Proof. repeat decide equality. Defined.

Cheers.

2014-12-10 1:53 GMT+01:00 Saulo Araujo <saulo2 AT gmail.com>:

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

Proof. decide equality. Defined.

but Coq says Error: Attempt to save an incomplete proofCompilation output:

Thanks in advance,

Saulo

--

Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.