Universe for `pattern` · Coq users

Stream: Coq users

Topic: Universe for `pattern`

Andrej Dudenhefner (May 10 2021 at 11:35):

Is the following the expected behavior of pattern to fail on Qed whereas the previously printed proof works fine? This is confusing:

Goal Prop = (True : Type) -> Prop.
Proof.
  intro H.
  pattern Prop.
  rewrite H.
  exact I. (* No more subgoals. *)
  Show Proof.
Fail Qed.

Restart.
  (* use the previous Show Proof output (no universe constraints) *)
  exact (fun H : Prop = (True : Type) => eq_rect_r (fun T : Type => T) I H).
Qed.

Ali Caglayan (May 10 2021 at 13:28):

If you cbn after pattern the first proof works.

Michael Soegtrop (May 10 2021 at 13:35):

@Ali Caglayan : the cbv just undoes the effect of pattern. E.g. this also works:

Goal Prop = (True : Type) -> Prop.
Proof.
  intro H.
  rewrite H.
  exact I.
Qed.

I guess this was not the question.

IMHO it is always a bug when one ends up via tactic application with "No more sugoals" and Qed fails, so I would suggest to file a bug for this.

I can't help but wonder if the problem isn't with both pattern and rewrite. Given that the proof works modulo universes and that the universes look alright before rewrite I suspect that rewrite has problems with Type@{Set+1} which appears as the type of Prop after pattern. Interestingly, ssrpattern also produces this type in the let-binding it introduces and here rewrite fails immediately. (A manual proof via eq_rect_r succeeds after ssrpattern so I think it is very comparable to patternin that it doesn't by itself destroy the proof.)

Janno (May 10 2021 at 13:49):

Oh, I forgot the second part: I can't find an easy way to introduce Type@{Set+1} into the goal outside of pattern and ssrpattern which is why I suspect that they are buggy in that way. Other tactics create fresh universes in place of Set+1.

Gaëtan Gilbert (May 10 2021 at 13:51):

Set+1 is probably the problem, I guess pattern is missing a refresh somewhere
please report a bug

Andrej Dudenhefner (May 10 2021 at 14:05):

Gaëtan Gilbert said: