inferred match return clause can mask global names used within

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4999 From: @jonleivent Reported version: 8.5 CC: @herbelin

[coqbot]

Comment author: @jonleivent

Some strange interaction between inductively defined Prop constructors and injection is causing Set Injection On Proofs to fail to produce all Prop equalities - but once the Prop constructors are generalized, the problem mysteriously disappears:

Set Injection On Proofs.

Inductive P (A : Set) : Prop := p (a : A).
Variable F : (P nat) -> Set.

Goal forall F (i j : nat)(a : F (p _ i))(b : F (p _ j))(e : existT _ _ a = existT _ _ b), p _ i = p _ j.
Proof.
  intros.
  injection e. (*nothing useful comes out of injection, just a copy of e itself*)
  Fail tauto.
  Restart.
  (*merely generalizing p makes it work:*)
  generalize p.
  intros.
  injection e. (*now useful equalities come out of injection*)
  tauto.
Qed.

In V8.5pl2.

[coqbot]

Comment author: @jonleivent

I think this is a bigger issue than merely a problem with Set Injection On Proofs. Note the following - which doesn't use injection or Set Injection On Proofs at all:

Inductive P (A : Set) : Prop := p (a : A).

Goal forall F (i j : nat)(a : F (p _ i))(b : F (p _ j))(e : existT _ _ a = existT _ _ b), p _ i= p _ j.
Proof.
  intros.
  Fail refine (match e with eq_refl => _ end).
  Restart.
  generalize p.
  intros.
  refine (match e with eq_refl => _ end).
  reflexivity.
Qed.

The error from the first refine is:

Incorrect elimination of "x' in the inductive type 'P':
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort "Prop" is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

But, the following does work:

Goal forall F (i j : nat)(a : F (p _ i))(b : F (p _ j))(e : existT _ _ a = existT _ _ b), p _ i= p _ j.
Proof.
  intros.
  refine (match e in (_ = s) return (let (z, _) := s in p nat i = z) with
          | eq_refl => eq_refl
          end).
Qed.

I think the problem is: whatever mechanism that type inference is using to come up with a return clause for the match in the first case is causing naming problems, as it is apparently using "p" for the let binding, which then makes "p" in the body of that let not work as a constructor name. I guess that injection is relying on this infer-a-return-clause mechanism as well, which is why the original case failed.

The reason why I suspect the name clash in the let-in is by inspecting the proof term of the cases that succeeded - in these cases, Coq used "p" for the let-binding-introduced name in the return clause, and the "generalize" saved the day by changing the ctor's name to p0 instead.

So - I will change the component from Ltac to Main, and rename the bug...

[coqbot]

Comment author: @jonleivent

Another attempt to figure out what is going wrong in the inference of the return clause - this time leaving a hole for the ctor name in the let body in the return clause:

Inductive P (A : Set) : Prop := p (a : A).

Goal forall F (i j : nat)(a : F (p _ i))(b : F (p _ j))(e : existT _ _ a = existT _ _ b), p _ i= p _ j.
Proof.
  intros.
  refine (match e in (_ = s) return (let (p, _) := s in _ nat i = p) with
          | eq_refl => eq_refl
          end).
  intros. constructor.
  exact i.

Fails with "Anomaly: cannot define an evar twice. Please report."

Probably a different bug?

[coqbot]

Comment author: @herbelin

Hi Jonathan,

There are 3 different "bugs".

The first one, on Injection, is not a bug, even though what happens is delicate: option "Injection On Proofs" is working well and injection is going through "p nat i = p nat j". However, because P is in Prop, "p nat i = p nat j" does not imply "i = j" (it is refuted by the proof-irrelevant model of Prop). Technically, there is no projection from "p nat i" to i (consistently with the proof-irrelevant model, non-singleton Prop can only be eliminated to Prop). Compare to:

Set Injection On Proofs.

Inductive P (A : Set) : Prop := p (a : A).
Variable F : (P (True\/True)) -> Set.

Goal forall F (i j : True\/True)(a : F (p _ i))(b : F (p _ j))(e : existT _ _ a = existT _ _ b), p _ i = p _ j.
intros.
injection e.
(* gives i=j *)

Now, you seem to expect in your case that "injection" returns "p nat i = p nat j", which would indeed be a possibility to consider.

Thanks to Maxime, progresses have been made in 8.5 so that equality on subterms of the following forms is preserved:

• "constructor args = constructor' args'" with discrimination not allowed (typically because of a type in Prop)
• "t = u" where at least t or u does not start with a constructor, and t and u are not convertible

Your case is hybrid since it is of the form "constructor args = constructor other-args" (with same constructor) but with non-projectable arguments in Type. I don't know the opinion of others, but I don't see at once a general rule for this case. E.g. if you had say, "p (nat(True\/True)) (a,b) = p (nat(True\/True)) (c,d)", then b=d could be derived but not a=c. Then, would we expect "injection" to return "p (a,b) = p (c,d)" (not injecting on b=d), or returning b=d (as it works now, but with the original information "p (a,b) = p (c,d)" lost because of the absence of a=c), or both?

[One remark in passing: one day, "injection" on dependent equality will have to be reconsidered. It looks wrong to me that it produces the same equation as before. I hope the unfortunately already too busy and too small development team which we form will be able to improve on this issue one day, unifying at the same occasion the behavior of inversion, dependent destruction, etc.]

The cause of the second problem is similar though in code unrelated to the code of the "injection' tactic: the inference of the return clause indeed tries to do some "injection" on the fly and, here, it notices too late that injection i out of "p _ i" is not allowed. So, we could consider this as a request for enhancement.

The anomaly produced in the third situation is not very elegant. It is related to "refine" leaving constraints which are here not shown (I thought we decided we shall write them eventually in 8.5 but I'm not sure). For the purpose of diagnosis, let's mention that it is failing in 8.6 with no anomaly but instead with an "Incorrect number of goals" error (I don't know why though).

[coqbot]

Comment author: @jonleivent

Hugo,

I am perhaps not understanding your diagnosis. Ignoring the 3rd anomaly case - why does a generalize on the constructor name in the first two cases cause success?

My point is: whatever the reason for this trivial generalize changing the behavior of both injection and match-return-clause inference, shouldn't they both not require this generalize to succeed?

As for projecting out of props - you do note that I didn't attempt any such projection when the goal wasn't itself in Prop. Indeed, I would expect an error if I attempted that. So, I don't understand why this is being brought up.

I have experimented some more with inference of parts of match return clauses, and have found other unusual behaviors that may help explain the bug. Note, for instance that the following refine does not fail in the second case (prior to the generalize) - although it doesn't prove very useful:

refine (match e return _ with eqrefl => end).

This is why I think the error produced by the original refine for the second case:

refine (match e with eqrefl => end).

about incorrect elimination of sort Prop when the return type is of sort Type is itself incorrect and a red herring. Why did the "return _" part, which should perhaps have made no difference at all, at least convince Coq that the elimination was taking place properly?

-- Jonathan

[coqbot]

Comment author: @herbelin

why does a generalize on the constructor name in the first two cases cause success?

The generalization turns the constructor into a variable and injection stops trying to project when it sees a variable.

When p is a constructor, injection tries to use the injectivity of p to extract an equality on the contents of p, here i=j, but i and j are in nat, so their projection is not allowed and injection renounces to project them.

Similarly for the inference of the return clause: it stops trying injecting when finding a non-constructor (only injectivity of constructor is taken into account).

As for projecting out of props - you do note that I didn't attempt any such projection when the goal wasn't itself in Prop. Indeed, I would expect an error if I attempted that. So, I don't understand why this is being brought up.

What matters to project is not the type of the goal, it is the type of the elements which are projected. Here i and j are in nat, so they cannot be projected out of a P which has no elimination to Set/Type.

I have experimented some more with inference of parts of match return clauses, and have found other unusual behaviors that may help explain the bug. Note, for instance that the following refine does not fail in the second case (prior to the generalize) - although it doesn't prove very useful:

refine (match e return _ with eqrefl => end).

Yes, using _ for the return predicate stops the algorithm for inferring the return clause to try injection.

Is that clearer?

[coqbot]

Comment author: @herbelin

For reference: extra comments on injection (coming from a discussion with Jonathan Leivent):

Desirable properties for injection:

• Reversibility: the conjunction of hypotheses produced by injection should be equivalent to the initial hypothesis.

• Idempotency: calling injection on an hypothesis produced by injection is the identity. (On dependent equalities using existT, this seems to hold - with the as clause of injection -; on non projectable equalities in Type arguments of a constructor in Prop, I don't know how to ensure it in the general case.)

• Generalization of injection so that it works not only on constructors but also on functions of a type class of injective functions.

[coqbot]

Comment author: @jonleivent

Until this is fixed, I have come up with the following workaround. It temporarily factors all Prop constructors out of the injecting hypothesis. It uses the new is_constructor predicate available in 8.6 (I have a way to do that in 8.5, but it's slow and kludgey). It also addresses somewhat the nagging issue where injection sometimes just returns a copy of the injecting hypothesis - instead failing in this case to prevent infinite loops:

(*Do an intro only if it is unique, else remove it:*)
Ltac uintro :=
  lazymatch goal with
  | _ : ?T |- ?T -> _ => intros _
  | _ => intros ? (*not "intro" to avoid head reduction*)
  end.

Ltac is_prop_ctor sym :=
  is_constructor sym;
  let tsym := type of sym in
  let ttsym := type of tsym in
  constr_eq ttsym Prop.

Ltac with_factored_prop_ctors H tac :=
  match type of H with
  | context[?C] =>
    is_prop_ctor C;
    let C' := fresh "ctor_alias" in
    remember C as C';
    with_factored_prop_ctors H tac;
    subst C'
  | _ => tac
  end.

Ltac fixed_injection H :=
  progress (with_factored_prop_ctors H ltac:(injection H); repeat uintro; subst).

[coqbot]

Comment author: @jonleivent

Since 4890 looks similar, perhaps it is best to workaround this by factoring out any factorable non-top-level constructors (again, 8.6 needed for is_constructor):

(*Do an intro only if it is unique, else remove it:*)
Ltac uintro :=
  lazymatch goal with
  | _ : ?T |- ?T -> _ => intros _
  | _ => intros ? (*not "intro" to avoid head reduction*)
  end.

Ltac careful_injection H :=
  let rec factout p :=
      (lazymatch p with
       | (?F ?A, ?G ?B) =>
         (tryif (is_constructor A; is_constructor B)
           then try (remember A; remember B)
           else factout (A, B));
         factout (F, G)
       | _ => idtac
       end) in
  lazymatch type of H with
  | ?A = ?B =>
    factout (A, B); injection H; repeat uintro; subst
  end.

[coqbot]

Comment author: @jonleivent

No - that's obviously broken....