Coq: Enable "intros until <non dependent term>" / "intros until <prop>"

[bollu]

Version

v8.7.2

Operating system

Ubuntu 16.04

Description of the problem

Variable A B C: Set.
Lemma foo:
  forall (a: A)
    (EQ: A = B),
    A = C.
Proof.
  Fail intros until EQ.
    (* Ltac call to "intros until (quant_hyp)" failed.
    No quantified hypothesis named EQ in current goal even after head-reduction. *)

  (* WORKAROUND, not nice: *)
  intros a.
  intros. (* named EQ *)
Abort.

What is the correct way to write an intros until EQ?

Workaround 1:

@Zimmi48 explained on gitter that EQ is non-dependent, so not named.
intros until 1 will work, as 1 is the first non-dependent hypothesis.

However, this not very pleasing when one has large proof terms with many hypothesis (counting is annoying).

Workaround 2:

Variable A B C: Set.
Lemma foo (a : A) (EQ : A = B) : A = C.
Proof.

(* state is now:
  A, B, C : Set
  a : A
  EQ : A = B
  ============================
  A = C
*)
Abort.

This is also not ideal, since all the hypothesis are already introduced. If one has a theorem of the form

Theorem manyInductions: forall (a b c d: A), IndProp1 a b 
    -> IndProp2 b c 
    -> IndProp3 c d, Foo. 

It would be annoying if everything has been introduced already, since now one needs to generalize stuff.

Ideally, I would prefer to just have intros until <prop/non-dependent term>.

[bollu]

``` @Zimmi48 do you know what I would need to change to implement this?
coq/coq#7997

Pierre-Marie Pédrot @ppedrot 16:44 @bollu I wouldn't venture too much into that
territory

Siddharth @bollu 16:44 @ppedrot ahaha, why?

Pierre-Marie Pédrot @ppedrot 16:45 the code is already full of quirks to try to
handle properly bound names

Siddharth @bollu 16:45 ah

Pierre-Marie Pédrot @ppedrot 16:45 I am personally convinced that this feature
is not even sound

Siddharth @bollu 16:45 is there some way to clean it up / make it uniform? As
in, is it a theory problem or an engineering problem? OK,why? "this feature"
= one I am asking for?

Pierre-Marie Pédrot @ppedrot 16:45 not in the sense that it proves False, but
that you shouldn't be able to name bound variables no, even the one in the
dependent case it super fragile because bound names are transient they can be
changed with the context I'd rather remove it for the dependent case than the
other way around

Théo Zimmermann @Zimmi48 16:46 I think there is already a mangle-name option
about this @ppedrot ^^

Pierre-Marie Pédrot @ppedrot 16:47 yes yes but it's not about variables that
you already introduced

Siddharth @bollu 16:47 @ppedrot what do you mean "bound named are transient and
can be changed with context"? Is there an example of this?

Pierre-Marie Pédrot @ppedrot 16:47 it's even worse @bollu oh yeah, let's see
Goal forall n : nat, n = n. pose (n := tt). intros_until is performing a
funny dance to determine the name of bound variables it calls the same code as
the printer IIRC I don't think we should encourage the use of this feature

Siddharth @bollu 16:50 @ppedrot the "funny dance" is to determine what n is
referring to in pose (n := tt) (to make sure I'm understanding this correctly)

Pierre-Marie Pédrot @ppedrot 16:50 I'd bet @JasonGross has already misused this
to extract the name of bound variables or something similar

Pierre-Marie Pédrot @ppedrot 16:50 @bollu no, intros_eq needs to know which
bound variable you refer to so essentially, an integer but this information is
not in the term because Coq uses DeBruijn indices

Pierre-Marie Pédrot @ppedrot 16:51 so, it stores forall n : nat, t as (Forall
("n", nat, t)) where "n" is just a hint in particular the goal is internally
unchanged after the call to pose so intros_eq has to guess than when you write
intros_until n0 after the call to pose

Pierre-Marie Pédrot @ppedrot 16:52 you're actually referring to the first
binder, which is just n @ejgallego why #7998 when there is #7984? in
particular coqpp should be exported systemwide at some point so I don't get why
it should not be part of the bin folder

Pierre-Marie Pédrot @ppedrot 16:56 @SkySkimmer I think there is this variant
somewhere but yes this has already been discussed, please open a PR.

Siddharth @bollu 17:17 @ppedrot I see. So, this is some kind of engineering
problem about the way names and tactics interact is my takeaway. Is this
incorrect?

Pierre-Marie Pédrot @ppedrot 17:17 this is probably deeper than mere
engineering

Siddharth @bollu 17:18 Why? That is what I don't understand.

Pierre-Marie Pédrot @ppedrot 17:18 bound variables are bound, and while it is
fine to observe the name hint, it is not to observe what the user is supposed
to read

Siddharth @bollu 17:18 By that definition, intros until is in itself a hack?

Pierre-Marie Pédrot @ppedrot 17:18 indeed

Siddharth @bollu 17:19 Mh This is unfortunate :( So, do I close the issue
citing this chat?

Pierre-Marie Pédrot @ppedrot 17:19 and similarly all tactics like induction and
destruct dunno, that's my personal take

Siddharth @bollu 17:19 OK

Pierre-Marie Pédrot @ppedrot 17:19 other people might disagree

Pierre-Marie Pédrot @ppedrot 17:20 but in any case, expect trouble on the
engineering side (precisely because the notion doesn't make much sense from the
beginning)
```

Chat log describing why @ppedrot thinks this feature is a bad idea.

[herbelin]

As an extra comment, let's say that tactics like intros until were designed at a time where proving was done interactively in a terminal. The name you had used to state the theorem was not anymore visible on the screen, so, you were using the only name effectively available and this was the name that the printer was showing to you (or the absence of name in the case of your EQ).

With the arrival of GUIs working on a editable document, reasoning on the possibly fluctuating printed name started to make lesser sense than relying on the name that you had written in your document and that was still in your field of vision.

Additionally, the need for some minimal requirement of robustness to small changes in a proof also led to progressively spread the methodology of enforcing some binding structure in proof scripts (as was e.g. advocated by the math-comp developers). This means for instance, avoiding intro; apply H but preferring intro H; apply H, etc.

Your example is interesting because it is actually consistent with this "new" vision of being able to statically define what is a binding variable, what is a bound variable, and what is an ill-scoped variable in a document.

In particular, since what you are seeing is:

Lemma foo: forall (a: A) (EQ: A = B), A = C.

you expect that a and EQ are usable in the "natural" scope of the statement of the lemma, and in particular that the next tactic to be issued is aware of this scope and thus able to refer to a and EQ.

As of now, Coq is not able to ensure that the EQ you wrote is still available as a variable, thus, the answer is that we cannot fulfill your request.

But, maybe, what is wrong is to want to maintain the "old" view which dates back to the time of interactive sessions in the terminal.

Maybe, what would be right would be to instead forbid to do thinks like Goal forall n : nat, n = n. pose (n := tt). or thinks like Goal forall x, x=0 -> forall x, x=0, or like Inductive foo A A : Type := ..., as was discussed somewhere in an issue started by @jashug if I remember correctly.

Maybe, what would be right would be to give priority to being able to formally assign a binding structure to the names used in a script and to progressively deprecate any kind of feature which is liable to break this binding structure.

What I'm saying is at the current time just an informal idea. To make it concrete, we would have to do it properly, and that is not clear that it would be easy to precisely define the scope of a variable written in a document, but I feel that we can at least try to make progresses in this direction, typically progressively accompanying the "funny dances" that Coq is currently doing by deprecation warnings, so that one day, one can trust names explicitly written in a document, such as EQ in your case.

[bollu]

@herbelin do you have some vision of how this could be done? I don't understand anything in the Coq theory, but I would be interested in learning and trying.

[herbelin]

@bollu: I don't think this question of binding names in a document needs to understand Coq theory. It is more about the question of putting structure in proof scripts.

I don't know the opinion of others, but a first step could typically be to prevent standard tactics to declare an hypothesis of name foo when the quantified variables of the goal that are "in scope" already include a foo.

Another step would be to forbid declarations such as Lemma foo : forall x x :nat, x = 0. which a user shall anyway not write spontaneously.

For the record, note that a typical source of mandatory renaming to be aware of is the following:

Definition P x := forall y, x + y = 0.
Lemma L : forall y, P y.
unfold P.

but this remains compatible with the "natural intuition" that the y which appears in the statement of L is the name which should be preserved after unfolding (as it is already the case actually).

[jashug]

@herbelin references issue https://github.com/coq/coq/issues/6785#issuecomment-380836468
Concerning the workaround in your original post, do note that intros might decide to use a different name if EQ is already taken:

Variable A B C: Set.
Lemma foo:
  forall (a: A)
    (EQ: A = B),
    A = C.
Proof.
set (EQ := tt).
intro a.
intros.
(*
1 subgoal
EQ := tt : unit
a : A
EQ0 : A = B
______________________________________(1/1)
A = C
*)
Abort.

Set Mangle Names.
Lemma foo:
  forall (a: A)
    (EQ: A = B),
    A = C.
Proof.
intro a.
intros.
(*
1 subgoal
a : A
_0 : A = B
______________________________________(1/1)
A = C
*)

Below is a more theoretical take on why this feature is difficult. Note that I'm not a core Coq developer, and the opinions below are strictly my own.

Internally, Coq uses DeBruijn indices to represent variables, and only keeps the user-given names around for printing. And those names which are printed can change arbitrarily to avoid shadowing. Other features which rely on user-provided names (for example intros until and default implicit argument names (c.f. #6785)) also use the same arbitrary names generated for printing. For example:

Lemma foo : forall (a a : nat), a = a.
intros until a0.
(*
1 subgoal
a, a0 : nat
______________________________________(1/1)
a0 = a0
*)

That is why features which rely on the names of bound variables are currently rather fragile.
Coming up with a description of terms which preserves the names of bound variables, doesn't allow shadowing, and also supports capture-avoiding substitution and expansion of definitions, sounds like an ambitious research project to me.

[jashug]

@herbelin Your example of mandatory renaming only follows the status quo by chance:

Definition P T := forall x : nat, x = x -> T.
Lemma foo : P (forall x : bool, x = x).
unfold P.
(*
1 subgoal
______________________________________(1/1)
forall x : nat,
x = x -> forall x0 : bool, x0 = x0
*)

Though perhaps this is "cheating" in that it is not clear before unfolding P that (forall x : bool, x = x) will be part of the top-level spine of binders.