The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jonathan,

  the Equations plugin embarks a [Derive Equality for ind] command that

accomplishes that using dependent elimination without recourse to JMeq etc...

if possible, for example:

Require Import Program Equations.Equations.

From Equations Require Import EqDec DepElimDec EqDecInstances.

Inductive fin : nat -> Set :=

| fz : forall {n}, fin (S n)

| fs : forall {n}, fin n -> fin (S n).

Inductive Fin3 : forall n (f1 f2 : fin n), Set :=

| F31 : forall m (f1 f2 : fin m), (f1 = f2) -> Fin3 (S m) (fs f1) (fs

 f2)

| F3S : forall m (f1 f2 : fin m), Fin3 m f1 f2 -> Fin3 (S m) (fs f1)

(fs f2).

Derive Signature for fin.

Derive NoConfusion for fin.

Derive DependentElimination for fin.

Derive Equality for fin.

Solve Obligations with eqdec_proof.

Print Assumptions fin_eqdec.

Derive Signature for Fin3.

Derive NoConfusion for Fin3.

Derive DependentElimination for Fin3.

Derive Equality for Fin3.

Solve Obligations with eqdec_proof.

Print Assumptions Fin3_eqdec.

Both fin_eqdec and Fin3_eqdec are closed under the global context, as they are using instances of decidable equality for nat and fin.

This eqdec_proof tactic is not able to handle your Finx example currently though, it's also work in progress. How did you implement your tactic?

Best,

-- Matthieu

On Wed, Jul 6, 2016 at 8:02 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

BTW: am making good progress here.  I was able to get it to decide
equality for Fin, and even multiple type index cases, without using
axioms, as long as the types of the indexes are themselves decidable.
For example, it handled this beastie with ease:


Inductive Fin3 : forall n (f1 f2 : Fin n), Set :=
| F31 : forall m (f1 f2 : Fin m), (f1 = f2) -> Fin3 (S m) (FS _ f1) (FS
_ f2)
| F3S : forall m (f1 f2 : Fin m), Fin3 m f1 f2 -> Fin3 (S m) (FS _ f1)
(FS _ f2).


once it had done Fin.  It still needs more work, though...

For the "using JMeq" case when not all indexes are decidable - this
leads to an interesting general question.  Some tactics are able to
conditionally use something, like JMeq, only if it was previously
Required, and do something else instead if not - but those are probably
all using plugins to accomplish this choice. How would this be done in
pure Ltac?

AFAICT, the only non-plugin mechanism(s) that could be used for such "do
things one way if X is not Required, else another way if X is Required"
would be based on typeclasses, canonical structures, or hints - but
these all require some amount of declaration to exist already in X to
set up the search.

Would it make sense to have a way for Ltac to attempt to determine if
some things are Required or not, without relying on particular
declarations (instances or hints)?  For example, the following does not
work:

Goal True.
Fail try let x := uconstr:(JMeq.JMeq) in idtac.

because Coq complains very early that JMeq.JMeq isn't in the current
environment - earlier than uconstr formation, evidently.  It does work
for just an unqualified "JMeq" alone, however:

Goal True.
try let x := uconstr:(JMeq) in idtac.

so it is the lookup of id qualifiers that is happening too soon for
uconstr - and it thus is possible to conditionalize on Require Import,
just not on Require alone.

Would it make sense if uconstrs were allowed to refer to undefined
qualified symbols, with the requirement that their qualifications be
defined deferred just as is done for unqualified symbols?  Should there
be some kind of "moral equivalence" between the use of an unqualified
symbol and a qualified one when both are undefined?

Or, would it be better to have another form that does this environment
querying?

-- Jonathan


On 07/05/2016 02:38 AM, Jason Gross wrote:
> 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
>>>>
>>>>
>>>>
>>