coq

coq copied to clipboard

Description of the problem

Don't know if this is a real bug or a feature. In the latter case I would like to ask for a workaround.

specialize does not allow the following anymore, due to some scope error that IMHO should not happen.

This is a simplified version of the especialize tactic I frequently use and is currently broken:

Lemma lem: (forall n m:nat, (forall x, x<n) -> m = n) -> Prop.
Proof.
  intros H. 
  evar (n':nat).
  evar (foo: forall x, x < ?n').
  specialize H with (1:=foo).

H : forall n m : nat, (forall x : nat, x < n) -> m = n
n' := ?n' : nat
foo := ?foo : forall x : nat, x < ?n'
n : nat
Unable to unify "?n'" with "n" (cannot instantiate "?n'" because "n" is not in its scope: available arguments are "H").

Indeed n is not in the scope of ?n' but IMHO there is no reason for ?n' to be instantiated by n, it should remain uninstantiated.

Note that this works fine (but the whole goal of the e-tactics is to avoid giving the non-dependent hyps by hand):

  specialize H with (n:=0) (1:=foo).

The comment here: https://github.com/coq/coq/blame/3c5387245ab14d1520967184c8fab49b3676a2b4/tactics/tactics.ml#L2929 my be involved in the problem.

Pinging @ppedrot

Coq Version

8.18