blob: 0d0f2eed44c2279e8e67290acb80b7f867c8c75d (
plain)
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(* Check that resolved status of evars follows "restrict" *)
Axiom H : forall (v : nat), Some 0 = Some v -> True.
Lemma L : True.
eapply H with _;
match goal with
| |- Some 0 = Some ?v => change (Some (0+0) = Some v)
end.
Abort.
(* The original example *)
Set Default Proof Using "Type".
Module heap_lang.
Inductive expr :=
| InjR (e : expr).
Inductive val :=
| InjRV (v : val).
Bind Scope val_scope with val.
Fixpoint of_val (v : val) : expr :=
match v with
| InjRV v => InjR (of_val v)
end.
Fixpoint to_val (e : expr) : option val := None.
End heap_lang.
Export heap_lang.
Module W.
Inductive expr :=
| Val (v : val)
(* Sums *)
| InjR (e : expr).
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
| Val v => of_val v
| InjR e => heap_lang.InjR (to_expr e)
end.
End W.
Section Tests.
Context (iProp: Type).
Context (WPre: expr -> Prop).
Context (tac_wp_alloc :
forall (e : expr) (v : val),
to_val e = Some v -> WPre e).
Lemma push_atomic_spec (x: val) :
WPre (InjR (of_val x)).
Proof.
(* This works. *)
eapply tac_wp_alloc with _.
match goal with
| |- to_val ?e = Some ?v =>
change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
end.
Undo. Undo.
(* This is fixed *)
eapply tac_wp_alloc with _;
match goal with
| |- to_val ?e = Some ?v =>
change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
end.
Abort.
|
