The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 29 Aug 2012 15:59:13 +0200,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> Hello friends.
> 
> Consider the following definition
> 
> Inductive def : Type :=
>   | Cons1 : nat -> list nat ->def.
> 
> Now, let's say I want to prove decidability of this structure's
> equality. Trivially, the following does work.
> 
> Lemma def_dec:
>   forall d d': def, {d = d'} + {d <> d'}.
> Proof.
>   intros.
>   repeat decide equality.
> Qed.
> 
> Now, say we have this definition instead:
> 
> Inductive def :Type :=
>   | Cons1 : list def -> def.
> 
> The above proof would not work in this case. In fact, since I'm using
> repeat, it would actually never terminate.
> 
> As you've guessed by now :), I would like to know what is the
> approach you guys use for proving decidable equality of inductive
> definitions with self-referenced projections.

Here you have to deal with nested fixpoint.

In general, the easiest way I know to deal with that is to manually
embed the [list] definition inside of [def].

That is:

>>>>>>>
Inductive def :Type :=
  | Cons1 : list_def -> def
with list_def :Type :=
  | Nil_def : list_def
  | Cons_def : def -> list_def -> list_def.

I think [decide equality] deals nicely with such a definition.

If it does not, you still can do something like:

Fixpoint def_eq_dec (a b : def) : {a=b}+{a<>b}
with list_def_eq_dec (a b : list_def) : {a=b}+{a<>b}.

  decide equality; apply list_def_eq_dec.
  decide equality; apply def_eq_dec.
Defined.
<<<<<<<<

But doing so, you will lack the List module functions. That is the cost
to pay for having an often easier way to prove by induction.


Alternatively, with nested functions (so using your original type), you
can do something like that:

>>>>>>>>>
Definition list_dec {A} (eqd : forall (a b : A), {a=b}+{a<>b})
: forall (a b : list A), {a=b}+{a<>b}.

  decide equality.
Defined.

Fixpoint def_eq_dec (a b : def) : {a=b}+{a<>b}.

  decide equality.
  apply list_dec; auto.
Defined.
<<<<<<<<<


Note also, that if you want to spend time writing down the decider by
hand, you can have a more efficient decider than those defined by
[decide equality], since you can use the abstract tactic, and improve
some parts which do a job similar to the one done by inversion.

I do not advice "not to use [decide equality]", because it is really
handful, but just be aware that for big inductives it can produce quite
big terms. I think that using the [abstract] tactic inside of its
engine could be a plus.


> 
> 
> On a related note: I use CoqIDE and it does not seem to have any way
> to kill the current applied tactic, meaning that for the above
> infinite scenario I have no other way besides killing the application
> and restart it. Right?
> 
> Please note that this 'problem' may also arise in situations like
> 'repeat inversion H; subst', which is something that I use from time
> to time..
> 
> What's your input on that? I should treat using 'repeat' as some kind
> of "bad practice" or? Yeah, I know some of you could tell me that I
> should know beforehand what are the effects of the tactic before
> applying it :), but the thing is that sometimes I forget how I
> defined the structures and in the case of repeating inversions it was
> not that easy to predict - consider a respectable number of
> hypothesis in your context.
> 
> Anyway, some thoughts please :)
> 
>