Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] decide equality on more types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] decide equality on more types


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] decide equality on more types
  • Date: Wed, 6 Jul 2016 14:01:45 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
  • Ironport-phdr: 9a23:aeWQFhDrO950rT/iI3vbUyQJP3N1i/DPJgcQr6AfoPdwSP7/rsbcNUDSrc9gkEXOFd2CrakV06yM7eu5ADFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD14LtiavrosCbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGxmkql+rIsYDe26Ivx5HvRkC2EtNHlw78n2vzHCSxGO7z0SSDY4iB1NVirC6hjmXp73+g/3t/Rw3jXSac/xS7E3VDCv4o9kTRbpjGEMMDtvozKfsdB5kK8O+EHpnBd42YOBPdmY

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








Archive powered by MHonArc 2.6.18.

Top of Page