The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/20/2016 04:45 PM, Jonathan Leivent wrote:
> On 07/20/2016 04:37 PM, Jason Gross wrote:
> > Here is a way to distinguish based on the results of typechecking:
> > Inductive eq : forall {A}, A -> A -> Prop := eq_refl A x : @eq A x x.
> > Inductive eq' {A} (x : A) : A -> Prop := eq_refl' : @eq' A x x.
> > Check fun A x y (p : @eq A x y) => match p in (@eq A' x' y') with _ => I
> > end.
> > Fail Check fun A x y (p : @eq' A x y) => match p in (@eq' A' x' y') 
> > with _
> > => I end. (* Error: The parameters do not bind in patterns; they must be
> > replaced by '_'. *)
> >
> > I wish you luck in making this work in general; it seems that the [in]
> > clause does special name-resolution and ignores ltac-variables.
> >
> > Here's another way that may prove more fruitful:
> >
> > Goal forall A x y, @eq A x y -> True.
> >    intros ??? p.
> >    case p. (* forall A0 : Type, A0 -> True *)
> > Abort.
> > Goal forall A x y, @eq' A x y -> True.
> >    intros ??? p.
> >    case p. (* True *)
> > Abort.
>
> Using case this way looks promising.   So, the number of intros will 
> be the number of non-index parameter.
> I'll try making a tactic that uses that...

On second thought - that doesn't work.  We're confusing ctor fields with 
indexes.  Of course case will produce intros for the fields.

-- Jonathan

> Thanks!
>
> -- Jonathan
>
> > On Wed, Jul 20, 2016 at 1:25 PM Jonathan Leivent 
> > <jonikelee AT gmail.com>
> > wrote:
> >
> > > Is there any way accessible via Ltac that one can get the count of the
> > > number of indexes for a particular inductive type?  Not the total 
> > > number
> > > of parameters - just the indexes.
> > >
> > > Examining the inductive type doesn't tell you which of that type's args
> > > are indexes or just parameters.
> > >
> > > Examining the constructors usually helps some, because the point where
> > > the args of the constructors differ from each other or the args of the
> > > type indicates that there are no more non-indexes after that point.
> > > But, there may be indexes that don't vary. Hence, in:
> > >
> > > Inductive Foo : nat -> Set := foo(n : nat) : Foo n.
> > >
> > > Inductive Bar(n : nat) : Set := bar.
> > >
> > > Foo and Bar have the same type nat -> Set, and their constructors foo
> > > and bar have similar type structure as well (modulo Foo/Bar). Yet, Foo
> > > has a type index while Bar doesn't.
> > >
> > > -- Jonathan