1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
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.
|
