The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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