The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you want the general solution, see if your tactic can handle W-types (https://coq.inria.fr/cocorico/WtypesInCoq).  Most indexed types are isomorphic to a corresponding indexless type, so if you really want a sledgehammer, you could convert the indexed type you're given into the corresponding indexless W-type, prove decidable equality under the assumption of function extensionality there, and port the proof across the isomorphism, and then flatten the ismorphism and strip out the uses of function extensionality from the proof.

Alternatively, the goal you probably want for Fin is something like

Goal forall n m (a : Fin n) (b : Fin m), { pf : n = m | transport Fin pf a = b}+{forall pf : n = m, transport Fin pf a <> b}.

The more general way to do this for types, I think, is to define something like

code : forall n, Fin n -> forall m, Fin m -> Type

decode : forall n a m b, code n a m b -> { pf : n = m | transport Fin pf a = b }

with

forall n a, { x : code n a n a | forall y, x = y }

From this, you can classify the equality equality space of Fin; if [code] is decidable, then so is [Fin].

-Jason

On Mon, Jul 4, 2016 at 7:58 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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