The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Ltac strip_useless_binders term :=

  lazymatch term with

  | _ -> ?T => strip_useless_binders T

  | fun _ => ?T => strip_useless_binders T

  | _ => term

  end.

Ltac count_prods term :=

  lazymatch (eval hnf in term) with

  | forall x : ?T, @?f x

    => let v := constr:(fun x : T => ltac:(let v := count_prods (f x) in exact v)) in

       let v := strip_useless_binders v in

       constr:(S v)

  | _ => constr:(0)

  end.

Ltac get_prods_of_type_of term :=

  let T := type of term in

  count_prods T.

Ltac get_type_after_case_count ty :=

  let v := constr:(ltac:(let x := fresh in

                         evar (x : nat);

                         let xv := (eval cbv [x] in x) in

                         assert (ty -> True);

                         [ let term := fresh in

                           intro term; case term;

                           [ let G := match goal with |- ?G => G end in

                             let v := count_prods G in

                             unify xv v;

                             intros; exact I

                           | intros; exact I.. ]

                         | eexact xv ])) in

  eval cbv zeta in v.

Ltac head term :=

  match term with

  | ?f _ => head f

  | _ => term

  end.

Ltac get_first_ctor ty :=

  let v := constr:(ltac:(let x := fresh in

                         let T := fresh in

                         evar (T : Type);

                         evar (x : T); subst T;

                         let xv := (eval cbv [x] in x) in

                         assert (ty -> True);

                         [ let p := fresh in

                           intro p;

                           let H := fresh in

                           destruct p eqn:H;

                           [ let ty := match type of H with

                                       | _ = ?RHS => RHS

                                       end in

                             let ty := head ty in

                             unify xv ty;

                             intros; exact I

                           | intros; exact I.. ]

                         | eexact xv ])) in

  eval cbv zeta in v.

Ltac get_parameter_count_of_ty ty :=

  let first_ctor := get_first_ctor ty in

  let total_args := get_prods_of_type_of first_ctor in

  let non_parameter_args := get_type_after_case_count ty in

  eval compute in (total_args - non_parameter_args).

Ltac under_type_binders term tac :=

  let ty := type of term in

  lazymatch eval hnf in ty with

  | forall x : ?T, _

    => let x' := fresh x in

       let v := constr:(fun x' : T => ltac:(let v := under_type_binders (term x') tac in eexact v)) in

       strip_useless_binders v

  | ?ty => let v := constr:(ltac:(tac term)) in

           v

  end.

Ltac get_parameter_count ty_family :=

  let v := under_type_binders ty_family ltac:(fun ty => let v := get_parameter_count_of_ty ty in eexact v) in

  v.

Inductive Foo : nat -> Set := foo(n : nat) : Foo n.

Inductive Bar(n : nat) : Set := bar.

Inductive eq' : forall {A}, A -> A -> Prop := eq_refl' A x : @eq' A x x.

Goal True.

  let t := constr:(@Foo) in let v := get_parameter_count t in idtac t v. (* Foo 0 *)

  let t := constr:(@Bar) in let v := get_parameter_count t in idtac t v. (* Bar 1 *)

  let t := constr:(@Logic.eq) in let v := get_parameter_count t in idtac t v. (* @eq 2 *)

  let t := constr:(@eq') in let v := get_parameter_count t in idtac t v. (* @eq' 0 *)

On Wed, Jul 20, 2016 at 2:30 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 07/20/2016 05:04 PM, Jonathan Leivent wrote:
>
>
> 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

This might work - based on the fact that case alters index fields in the
conclusion but not parameters.  So, given an inductive type completely
parameterized by individual distinct hyps, casing an instance with
another matching instance in the conclusion will cause the conclusion's
copy to differ from the cased one by exactly just the indexes:

Inductive Foo(i :nat) : bool -> Set := foo(n:nat) : Foo i true.

Goal forall i b, Foo i b -> Foo i b -> True.
intros i b f.
case f.  (*conclusion will have fields, then Foo i true -> True *)

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