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.
```

If you `cbn`

after `pattern`

the first proof works.

@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 `pattern`

in that it doesn't by itself destroy the proof.)

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`

.

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

please report a bug

Gaëtan Gilbert said:

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

please report a bug

Will do. #14300

Last updated: Jun 18 2024 at 10:02 UTC