The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi folks,

I am not expert here but I was wondering if this use of Ltac could be
classified as "not robust", and thus, likely not to be supported between
Coq releases.

It seems a frequent complaint that Coq breaks compatibility between
releases, however, if you depend on the semantics of tactics in ways
that they were not designed to be relied upon, IMVHO little can be done.

Maybe more expert people could comment.

Best regards,
Emilio

p.s: A more principled way to support querying an inductive definition
could be of course defined.

Jonathan Leivent 
<jonikelee AT gmail.com>
 writes:

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