The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/04/2016 09:26 PM, Jason Gross wrote:
> What types are you looking to decide equality on?

I'm actually making some progress towards such a decide equality tactic 
- and was wondering if I might be re-inventing the wheel. Also, having 
an idea how to do this is far removed from having a robust solution...

The most important additional types I'm interested in are when difficult 
dependent-indexed-type cases are replaced by equivalent but 
not-as-difficult dependent parameterized types with equality fields.  A 
primary example is Fin:

Inductive Fin : nat -> Set :=
| F1 : forall n : nat, Fin (S n)
| FS : forall n : nat, Fin n -> Fin (S n).

Goal forall n (a b : Fin n), {a=b}+{a<>b}.
Fail decide equality.
Abort.

It seems to be very hard to automatically via tactics derive anything 
useful for types like Fin in this direction without using additional 
axioms like JMeq_eq.  However, consider Finx, which is semantically 
equivalent to Fin, but index-less:

Inductive Finx(n : nat) : Set :=
| Fx1(i : nat)(e : n = S i)
| FxS(i : nat)(f : Finx i)(e : n = S i).

Goal forall n (a b : Finx n), {a=b}+{a<>b}.
Fail decide equality.
Abort.

I have a prototype tactic which will decide equality for Finx (and 
hopefully other types like it) without additional axioms.  It leverages 
Coq.Logic.Eqdep_dec to handle the equality ("e") fields in the 
constructors, provided that they are themselves equalities on decidable 
types (and hence have UIP via the theorems in Eqdep_dec) - which it will 
then try to solve recursively, etc.  It also handles cases where 
injection yields sigma-typed equalities, again using theorems from 
Eqdep_dec, again provided with the necessary sub-decidables, which it 
will again try to solve recursively.  It will also use existing 
typeclass instances of decidable equality instead of trying to solve 
them itself.

It should leave behind subgoal equalities it can't solve - so it can be 
composed with other means.  Hopefully, it will always solve what can be 
solved using the above techniques - unlike decide equality which 
currently fails in any case where something like Fin or Finx is a 
sub-equality.

For extra credit, maybe if JMeq is around, it should use that for 
indexed types.  However, I prefer using index-less equivalents to 
indexed types (Finx instead of Fin) for other reasons, so I don't really 
need to solve indexed cases for my own purposes.


-- Jonathan

> On Mon, Jul 4, 2016 at 3:55 PM Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> > Does anyone know of a version of the "decide equality" tactic that works
> > on more types?
> >
> > -- Jonathan