coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] how many type indexes for a particular type?
- Date: Fri, 22 Jul 2016 14:24:23 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f175.google.com
- Ironport-phdr: 9a23:898sBBeCCF75iVqQUIpdJx2NlGMj4u6mDksu8pMizoh2WeGdxc68bB7h7PlgxGXEQZ/co6odzbGH6+a9BidZuMnJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mj6bvpNaKOloArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLHzX8BWC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijb7cyUCii5qEjbBLplioBK3Zt8mbRi899iK9WiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vkYg==
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.
- [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jason Gross, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jason Gross, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/21/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Emilio Jesús Gallego Arias, 07/21/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jason Gross, 07/21/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/22/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/21/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jason Gross, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jonathan Leivent, 07/20/2016
- Re: [Coq-Club] how many type indexes for a particular type?, Jason Gross, 07/20/2016
Archive powered by MHonArc 2.6.18.