| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle bug_7825.v Sprache: Coq |
|||||||||
|
Record T (x : nat) := { t : x = x }.
Goal exists x, T x. refine (ex_intro _ _ _). Show Existentials. simple refine {| t := _ |}. reflexivity. Unshelve. exact 0. Qed. (** Fine if the new evar is defined as the originally shelved evar: we do nothing. In the other direction we promote the non-shelved new goal to a shelved one: shelved status has priority over goal status. *) Goal forall a : nat, exists x, T x. evar (x : nat). subst x. Show Existentials. intros a. simple refine (ex_intro ?[x0] _ _). shelve. simpl. (** Here ?x := ?x0 which is shelved, so ?x becomes shelved even if it would not be by default (refine ?x and _ produce non-shelved evars by default)*) simple refine (Build_T ?x _). reflexivity. Unshelve. exact 0. Qed. Goal { A : _ & { P : _ & @sigT A P } }. epose _ as A; epose _ as P; exists A, P. (* Regardless of which evars are in the goals vs the hypotheses, [simple refine (existT _ _ _)] should leave over two goals. This should be true even when chained with epose. *) assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); subst P; assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); subst A; assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2). (* fails *) Abort. Goal { A : _ & { P : _ & @sigT A P } }. epose _ as A; epose _ as P; exists A, P; (* In this example we chain everything *) assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); subst P; assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); subst A; assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2). (* fails *) Abort. ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28