surprising behavior of `intros` when names are given in unexpected way.

[gasche]

intros <name>* is not documented in the reference manual. It would be helpful to know what the intended semantics is. I don't know whether any of the following are bugs, but they look strange anyway.

Starting from:

Theorem foo : true -> true -> true.

I can do either intros or intros HA HB, which work as expected: intros makes up a fresh hypothesis name, and intros HA HB uses the names I gave. But the following are strange:

Conflicting names (I guess that's ok):

  intros A A.
(*
A : true
A1 : true
============================
 true
*)

Too many names (I guess that's ok, although for script robustness I would rather have a failure here):

  intros A B C.
(*
A : true
B : true
============================
 true
*)

Giving "not enough names" works fine (later names are picked by the system), except if the name given are H1, H2...:

  intros H1.
(*
H1 : true
H1 : true
============================
 true
*)

(notice that two hypotheses now have the same name)

[gasche]

In fact, explicitly giving intros H1 H2. works badly even if the correct number of variables are given, because it disturbs the fresh-name generation later in the script to reuse H1 and H2 again. This means that given a script that uses intros., rewriting it to use intros H1 ... Hn explicitly will in general break the rest of the proof script as it will change the generated variable names.

I guess the fix is: whenever the user chooses a variable name, checks if it coincides with the "next fresh name", and in that case increment the fresh name counter (do as if it had been generated by the system).

[chaudhuri]

I've committed a quick fix but it has a performance impact. Not sure how measurable. Also it may break some existing proofs because the numbering is different in some corner cases. Will need to revisit this.

On Mon, Jan 8, 2018 at 12:19 PM, Gabriel Scherer notifications@github.com wrote:

In fact, explicitly giving intros H1 H2. works badly even if the correct number of variables are given, because it disturbs the fresh-name generation later in the script to reuse H1 and H2 again. This means that given a script that uses intros., rewriting it to use intros H1 ... Hn explicitly will in general break the rest of the proof script as it will change the generated variable names.

I guess the fix is: whenever the user chooses a variable name, checks if it coincides with the "next fresh name", and in that case increment the fresh name counter (do as if it had been generated by the system).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/abella-prover/abella/issues/97#issuecomment-355940711, or mute the thread https://github.com/notifications/unsubscribe-auth/AAjB6JASK-9HMLtoRKsRk9uAJgT7N5v-ks5tIfnGgaJpZM4RWOtE .

[chaudhuri]

This breaks too many existing proofs. More testing is needed.