aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5757.v
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.