The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

OK - I'm impressed.  But I wrote my own version that spits out what I 
really needed: the parameterized (up to but not including indexes) head 
of the type of a term.

Thanks!

-- Jonathan


On 07/20/2016 05:55 PM, Jason Gross wrote:
> 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