The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

My own $0.02:

I agree that using Ltac, in its current incarnation, to do fairly 
complex things can lead to maintenance difficulties across releases.  
However, I still think it is the right thing to do, for these reasons:

1. Writing plugins does not rid one of the maintenance issue across 
releases - rather, it alters the issue to be about how internal Coq 
interfaces are likely to change instead of about how external Ltac 
semantics are likely to change.  One could argue (and I would agree!) 
that determining indexes vs. params of inductive types is something so 
basic to the Gallina language that there should be a built-in way to do 
it.  Perhaps - but being a plugin vs. being built-in is not much of a 
maintenance advantage over being a tactic vs. being built-in.

2. Tactic writers, while they need to understand Ltac semantics and be 
aware of Ltac changes across releases, shouldn't be additionally 
burdened with the requirements to understand OCaml code and Coq 
internals, and how Coq internals change across releases.

3. A domain-specific language for goal manipulation - tactics - is the 
proper home of routines that are specific to the task of proving goals - 
for all of the standard reasons that DSLs are considered good 
solutions.  Note that this doesn't imply that the tactic language can do 
without a well-rounded set of built-in tactics - rather, the opposite is 
true - and perhaps a built-in tactic to determine indexes/params of 
inductive types would be worth adding.

4. While we can all agree that Ltac has its warts, and that development 
of enhancements and better alternatives is an excellent idea (and being 
actively pursued), that development likely needs help from tactic 
writers to determine what kinds of semantics and power such enhancements 
and alternatives should have.  Steering clear of complex tactic 
definitions means that this space would not be adequately explored.  We 
should not let complex tactics vs. a suitably robust tactic language 
become a chicken-and-egg problem for Coq ;-)

But, there are also precautions that a tactic writer can take to ease 
the maintenance burden - as Jason suggests.  The solution I came up with is:


Ltac last_hyp := lazymatch goal with H :_ |- _ => H end.

Ltac get_value H := eval cbv delta [H] in H.

Ltac wrap_typewise T inside :=
  let rec f T :=
      lazymatch type of T with
      | (forall (a : ?X), _) =>
        let a' := fresh a in
        constr:(forall (a' : X), ltac:(let R := f (T a') in exact R))
      | _ => inside T
      end in
  f T.

Ltac head_of term :=
  lazymatch term with
  | ?F ?A => head_of F
  | _ => term
  end.

Local Record Sandbox : Prop := {}.

Ltac sandbox_value tac :=
  lazymatch
    constr:(
      ltac:(
        let V := fresh in
        refine (let V := _ in _);
        let e := get_value V in
        let giving value := unify value e in
        let unused := constr:(ltac:(clear V;
                              tac giving;
                              intros; constructor)
                        : Sandbox) in
        exact e)) with
    (let _ := _ in ?R) => R end.

Local Ltac common_head trip :=
  lazymatch trip with
  | (?X, ?A, ?A) => X
  | (?F _, ?G1 _, ?G2 _) => common_head (F, G1, G2)
  end.

Local Ltac get_paramed_type_head_internal term giving :=
  let T := type of term in
  let hT := head_of T in
  let inside C := constr:(C -> C -> True) in
  let w := wrap_typewise hT inside in
  assert w;
  [intros;
   let H := last_hyp in
   revert H;
   let H := last_hyp in
   let TH := type of H in
   case H; intros;
   let H' := last_hyp in
   let TH' := type of H' in
   let x := common_head (T, TH, TH') in
   giving x;
   exact I
  |].

Ltac get_paramed_type_head term :=
  sandbox_value ltac:(get_paramed_type_head_internal term).

(**********************************************************************)

Inductive Bar : nat -> Type := bar(n:nat) : Bar n.

Inductive Foo (n:nat)(b:bool) : nat -> Bar n -> Prop :=
| foo1(i : nat) : Foo n b n (bar n)
| foo2(x : bool)(j : nat) : x = b -> Foo n b (S j) (bar n).

Goal forall a b c d (f:Foo a b c d), unit.
  intros a b c d f.
  let x := get_paramed_type_head f in idtac x.


which I think illustrates some of the precautions: keep tactics small 
and doing single, well modularized, very specific things (especially 
when kludges are used - as with the sandbox_value tactic), try to stay 
away from unusual tactic behaviors that are much more likely to change 
across releases, etc.  Also, I do think whatever elegance one can get is 
worth the extra work, as it tends to produce tactics that are easier to 
understand and re-use.

-- Jonathan

On 07/20/2016 08:56 PM, Jason Gross wrote:
> 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.