Add an "especialize" tactic

[MSoegtropIMC]

This is a follow up on the discussion with subject "Is there something like especialize?" in coqclub on April 30th 2018.

The idea is to have a variant of specialize which allows using holes and evars in the same way as eapply. If one has a hypothesis H: P->Q the effect of

especialize (H SomeLemma)

should be similar to

assert (P) as HP by eapply SomeLemma. specialize (H HP).

with obvious extensions to hypothesis with several preconditions / parameters.

@Matafou suggested on coqclub to have a syntax which is extended compared to the syntax of eapply in that it allows to specify precoditions of the hypothesis by number in a with clause:

especialize H with (x:=t) (y:=u) (2:=?).

would mean: instantiate x by t, y by u, make an evar for the 2nd hypothesis (knowing that x:=t and y:=u) and use it, but let 1st hyp where it is (and all other non unifiable args of H).

[tchajed]

Is this basically specialize (H ltac:(eapply SomeLemma))? It would be nice to have some easy and tricky use cases as part of the feature request (a thinly disguised request for tests), to see how far we can get with Ltac. I do like the with syntax, which I think would be hard to provide using pure Ltac and tactic notations.

[MSoegtropIMC]

Yes, specialize (H ltac:(eapply SomeLemma)) would also do it in this simple case. There are many ways to achieve the same, e.g. also

lapply H. intros HP. all: swap 1 2. eapply SomeLemma.

would work. The idea is that specializing hypothesis is a sufficiently common task to be well supported by built in tactics with a nice, readable syntax, especially for complicated cases. It is not so that currently it doesn't work or is really complicated to achieve. It is just not very readable and/or easy to write - in short it is inconvenient.

Let's look at the case @Matafou described: For the (2:=?) I guess one could use ltac:(refine ?), but it gets a bit lengthy to achieve that the first hypothesis remains, that is to come from

H: forall (x : X) (y : Y), SomeP -> SomeQ -> SomeR

to

H: SomeP -> SomeR

[Matafou]

I see 2 layers here. First I need a way to say "now I want to prove the 2nd dep hyp of this hyp." without copy-pasting the statement. We can see this kind of tactics as forward reasoning BUT non declarative ones, i.e. they don't need to input (every now and then) statements in the script. They can also be viewed as tactics that help the user figure out how to prove things ("At this point I think NoDup l is the right instantiation for h but let me prove it first to be sure").

Require Import List.
Variable A: Type.
Variable a:A.
Variable P: Prop.
Lemma foo: forall l l':list A,
    (forall (l l' : list A) ,incl l l' ->  NoDup l -> length l <= length l')
    -> NoDup l -> P.
Proof.
  intros l l' h HnoDup. 
  specialize (h l).
  (*Now I want to prove the 2nd hyp of h:*)
  assert (NoDup l) as h'. {
    admit. (* arbitrarily long proof *)
  }
  specialize h with (2:=h').
  (* I would have preferred:

     (e)specialize h with (2:=?). {
       admit. (* arbitrarily long proof of NoDup l *)
     } *)
Abort.

2nd layer, if the hypothesis I want to instantiate is not closed, we
need to define evars (or create existential quantification):

Lemma foo: forall l l':list A,
    (forall (l l' : list A) ,incl l l' ->  NoDup l -> length l <= length l')
    -> NoDup l -> P.
Proof.
  intros l l' h HnoDup. 
  (* Suppose I want to instantiate the 2nd dep hyp of h (NoDup l), but
     I don't know yet which l I would like. Here how I would do that. *)
  assert (exists somel:list A, NoDup somel) as hex. {
    admit. (* arbitrarily long proof *)
  }
  destruct hex as (x,h').
  specialize h with (2:=h').
  (* I would have preferred:

     especialize h with (2:=?). { 
        admit. (* arbitrarily proof of either "NoDup ?x" or: "exists x, NoDup x" *) }
   *)

Note that we may prefer existential quantification (+ auto destruct at the end) because evars have constraints on the environment in which they are defined.

[MSoegtropIMC]

Interesting approach with existentials - but shouldn't it be close to eapply, which I guess would more correspond to:

Lemma foo: forall l l':list A,
    (forall (l l' : list A) ,incl l l' ->  NoDup l -> length l <= length l')
    -> NoDup l -> P.
Proof.
  intros l l' h HnoDup.
  (* equivalent of especialize h with (2:=?). *)
  evar (l'':list A). clear l''.
  assert (NoDup ?l'') as h'. {
    admit. (* arbitrarily long proof *)
  }
  specialize h with (2:=h').

Do you think one should have the option to choose between evars and existential quantification?

[Matafou]

I don't know evar machinery well enough to have a firm opinion on this. Existentials have there drawbacks too (you lose access to the actual witness when destructing the exists).

Anyway this is a problem with all "e" tactics. So this corresponds to another feature wish that it would be nice that "e" tactics should be able to change evar environements (or change of evars on the fly, I don't know).

Note that "e" variants where discussed here #248 (where it was decided that especialize was not needed, but specialize changed since then). And this problem of evar ill-instantiation was discussed somewhere but I can't find where.

[MSoegtropIMC]

@Matafou , thanks for the link to #248 - very interesting - I need to work through this - some interesting ideas.

The problem of illtyped evars should be the same for all e variants - next time I meet these I will do some experiments if using existentials has advantages.

[samuelgruetter]

LibTactics.v by @charguer provides something similar to the especialize being suggested, and it's called specializes, but I think it would be nice to have a built-in especialize with nicer syntax and the ability to say "don't instantiate this".

[MSoegtropIMC]

After going through #248, I would think that specialize is redundant and one should use (e)assert ( H := H .... ) instead. I simply didn't know that it is possible to specialize an existing hypothesis using assert. As far as I understood specialize is older, but assert, at least in its current form, is substantially more general.

I will switch to using assert instead of specialize and see if this has any bad consequences.

The only thing is that specialize is a bit more clear about the intention.

@Zimmi48 : I fully support your comment in #248, that the all combinations of : and := in assert are useful and I don't like the decision to deprecate these either. E.g. if assert is used instead of specialize, the syntax

<assert( H := H <something lengthy)>

is much easier to read than

<pose proof H as H>

In the assert form it is immediately clear that this is a specialization, in the pose proof form maybe not.

Another argument is that it is easier to learn how the various : / := variants of assert are connected than it is to understand how pose proof and assert are connected. I am more in favor of orthogonality (like deprecating specialize in favor of assert) than introducing new names for variants of a tactic (like pose proof).

@Matafou : I will experiment with assert / eassert instead of specialize. In case this looks good I intend to close this request, unless you disagree.

[Matafou]

I also agree that we should have one tactic for all. Whatever the final syntax is it should support the choice of letting some randomly placed arguments uninstantiated (i.e. quantified). Currently assert does not allow that afaiu.

Maybe we just need a short syntax for “random access application” in terms?

(t with `(3:= u)) would mean: instantiate 3rd dep hyp of t and all consequently unified args. But let others quantified.

(t with (3:=u)) would mean what it
means today in apply: everything before dep hyp 3 must be unified otherwise fail.

(t with ?(3:=u)) would mean create evars with non unified args.

[Matafou]

By the way we could have a “as !H” meaning more or less “as foo; clear H; rename foo into H.” So that assert can replace a hypothesis as specialize.

[Matafou]

Last comment. Once assert is general enough to do all that nothing prevents to have specialize as a synonym of assert. Synonyms are not a problem, 4 tactics subtly different and not completely equivalent is a problem.

[MSoegtropIMC]

I did some experiments. I am more into high automation, and there it is more common to specialize argument by argument, for which eassert just works fine - all I wanted. In cases I need to swap hypothesis, because I want to specialize a later but not the first hypothesis, I assert a hypothesis swapping lemma before I assert the then first hypothesis. For automation this is just fine, because doing things step by step gives more insight into what went wrong. But I fully agree that for manual operation specialize including the with syntax you suggest has its value.

I didn't understand your !H comment. What I learned from reading #248 is that assert actually can clear the hypothesis it specializes. Writing assert (H := H term) just works fine and has the same effect as specialize (H term) (as far as I can tell). Was your comment that this should be supported, or did you more mean that there should be an abbreviation for writing assert (H := H term) so that H is not duplicated? Actually I think this behavior of assert should be documented - it is very convenient but rather not so obvious. I would have expected an error for assert (H := H term). Actually I prefer assert over specialize, because it gives me the freedom to keep the original hypothesis or to duplicate it.

So as far as I can tell all which is missing in assert is a way to keep hypothesis generalized without the workaround of applying a swapping lemma.

I fully agree that it would make sense to add the "with" syntax you suggest to assert and then define specialize (H term) to be a shortcut for assert(H := H term) (or pose proof H term as H). A completely separate implementation (as it seems to be the case currently according to #248) doesn't seem to make a lot of sense. The argument swapping shouldn't require complex machinery.

And a physicist question: is there a word for a hypothesis of a hypothesis? I tend to use the term precondition, but this doesn't seem to be common. If there is no word, how about hypohypothesis?

[tchajed]

@MSoegtropIMC when H: P -> Q I like to call P a premise and Q the conclusion of the hypothesis H.