The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hey, Emilio,

The only thing I'm relying on for possibly unintended semantics is that [case] will give fresh names for all of the non-parameter arguments for each constructor.  The rest is very kludgy, but I wouldn't call it fragile; anything that breaks it is probably a deeper bug (fresh no longer working for binders, or not taking the ltac environment into account (this would break [let x := fresh in let y := fresh in ...] also)).  I wouldn't say that the code I wrote is terribly pretty or maintainable, either, though each tactic does do a single very specific thing, so it should be relatively easy to debug.

The compatibility problems that I actually run into in the wild come from more subtle things.  Here's a sampling:

- In 8.4, [foo; (bar; baz)] meant "run [bar; baz] on each subgoal generated by [foo], one at a time".  In 8.5, you need "foo; [ bar; baz.. ]"

- In 8.4 and 8.6, if you [Open Scope nat_scope], "match goal with H : context[x + y] |- _ => idtac end" picks up "+" in nat_scope.  In 8.5, it's type_scope.

- Minor changes in unification mean that things like [auto] and [autorewrite] will lead to different results in some cases

- [setoid_rewrite] looks for different instances by default in 8.4 and 8.5, which leads to a performance penalty when you write code for one and move to the other

- (not yet seen in the wild) adding a lemma to *any* database in the standard library will change the behavior of [intuition] in any file that imports the relevant stdlib file, which uses [auto with *] by default

- the handling of evars has changed in subtle ways; when you repeatedly refine evars with expressions involving other evars, which refinements will fail and which will succeed differs between 8.4 and 8.5; this basically means that you can't do any interesting proof by refinement involving evars that runs in both unless you put in a lot of work  (it took me an hour or so to debug why a [refine (_ : <some new type>)] was failing in 8.5 but working in 8.4)

In my experience, the sledgehammer / brute force tactics suffer the most from compatibility woes, while the precision / well-spec'ed tactics tend to either keep working, or completely break in obvious ways that allow rewriting.

However, I agree with you, figuring out the indices is really a task for ML, not Ltac.  I suspect the actual right way to do it might be to use the template-coq plugin and inspect the reified datastructure.

-Jason

On Wed, Jul 20, 2016 at 3:41 PM Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

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