substitution.v 4.28 KB
Newer Older
1
From iris.heap_lang Require Export lang.
2
Import heap_lang.
3

4
(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
5 6 7 8 9
can be tuned by declaring [Subst] instances. *)
(** * Substitution *)
Class Subst (x : string) (es : expr) (e : expr) (er : expr) :=
  do_subst : subst x es e = er.
Hint Mode Subst + + + - : typeclass_instances.
10

11
(* Variables *)
12 13 14 15
Lemma do_subst_var_eq x er : Subst x er (Var x) er.
Proof. intros; red; simpl. by case_decide. Qed.
Lemma do_subst_var_neq x y er : bool_decide (x  y)  Subst x er (Var y) (Var y).
Proof. rewrite bool_decide_spec. intros; red; simpl. by case_decide. Qed.
16

17 18 19
Hint Extern 0 (Subst ?x ?v (Var ?y) _) =>
  first [apply do_subst_var_eq
        |apply do_subst_var_neq, I] : typeclass_instances.
20 21

(** Rec *)
22 23 24 25 26 27 28 29 30 31 32
Lemma do_subst_rec_true {x es f y e er} :
  bool_decide (BNamed x  f  BNamed x  y) 
  Subst x es e er  Subst x es (Rec f y e) (Rec f y er).
Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
Lemma do_subst_rec_false {x es f y e} :
  bool_decide (¬(BNamed x  f  BNamed x  y)) 
  Subst x es (Rec f y e) (Rec f y e).
Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.

Local Ltac bool_decide_no_check := vm_cast_no_check I.
Hint Extern 0 (Subst ?x ?v (Rec ?f ?y ?e) _) =>
33
  match eval vm_compute in (bool_decide (BNamed x  f  BNamed x  y)) with
34 35
  | true => eapply (do_subst_rec_true ltac:(bool_decide_no_check))
  | false => eapply (do_subst_rec_false ltac:(bool_decide_no_check))
36 37
  end : typeclass_instances.

38 39 40 41 42
Lemma do_subst_closed x es e : Closed [] e  Subst x es e e.
Proof. apply closed_nil_subst. Qed.
Hint Extern 10 (Subst ?x ?v ?e _) =>
  is_var e; class_apply do_subst_closed : typeclass_instances.

43
(* Values *)
44 45
Instance do_subst_of_val x es v : Subst x es (of_val v) (of_val v) | 0.
Proof. eapply closed_nil_subst, of_val_closed. Qed.
Ralf Jung's avatar
Ralf Jung committed
46

47
(* Boring connectives *)
48 49 50
Section subst.
Context (x : string) (es : expr).
Notation Sub := (Subst x es).
51 52

(* Ground terms *)
53
Global Instance do_subst_lit l : Sub (Lit l) (Lit l).
54
Proof. done. Qed.
55
Global Instance do_subst_app e1 e2 e1r e2r :
56
  Sub e1 e1r  Sub e2 e2r  Sub (App e1 e2) (App e1r e2r).
57 58
Proof. intros; red; f_equal/=; apply: do_subst. Qed.
Global Instance do_subst_unop op e er : Sub e er  Sub (UnOp op e) (UnOp op er).
59
Proof. by intros; red; f_equal/=. Qed.
60
Global Instance do_subst_binop op e1 e2 e1r e2r :
61
  Sub e1 e1r  Sub e2 e2r  Sub (BinOp op e1 e2) (BinOp op e1r e2r).
62
Proof. by intros; red; f_equal/=. Qed.
63
Global Instance do_subst_if e0 e1 e2 e0r e1r e2r :
64
  Sub e0 e0r  Sub e1 e1r  Sub e2 e2r  Sub (If e0 e1 e2) (If e0r e1r e2r).
65
Proof. by intros; red; f_equal/=. Qed.
66
Global Instance do_subst_pair e1 e2 e1r e2r :
67
  Sub e1 e1r  Sub e2 e2r  Sub (Pair e1 e2) (Pair e1r e2r).
68
Proof. by intros ??; red; f_equal/=. Qed.
69
Global Instance do_subst_fst e er : Sub e er  Sub (Fst e) (Fst er).
70
Proof. by intros; red; f_equal/=. Qed.
71
Global Instance do_subst_snd e er : Sub e er  Sub (Snd e) (Snd er).
72
Proof. by intros; red; f_equal/=. Qed.
73
Global Instance do_subst_injL e er : Sub e er  Sub (InjL e) (InjL er).
74
Proof. by intros; red; f_equal/=. Qed.
75
Global Instance do_subst_injR e er : Sub e er  Sub (InjR e) (InjR er).
76
Proof. by intros; red; f_equal/=. Qed.
77
Global Instance do_subst_case e0 e1 e2 e0r e1r e2r :
78
  Sub e0 e0r  Sub e1 e1r  Sub e2 e2r  Sub (Case e0 e1 e2) (Case e0r e1r e2r).
79
Proof. by intros; red; f_equal/=. Qed.
80
Global Instance do_subst_fork e er : Sub e er  Sub (Fork e) (Fork er).
81
Proof. by intros; red; f_equal/=. Qed.
82
Global Instance do_subst_alloc e er : Sub e er  Sub (Alloc e) (Alloc er).
83
Proof. by intros; red; f_equal/=. Qed.
84
Global Instance do_subst_load e er : Sub e er  Sub (Load e) (Load er).
85
Proof. by intros; red; f_equal/=. Qed.
86
Global Instance do_subst_store e1 e2 e1r e2r :
87
  Sub e1 e1r  Sub e2 e2r  Sub (Store e1 e2) (Store e1r e2r).
88
Proof. by intros; red; f_equal/=. Qed.
89
Global Instance do_subst_cas e0 e1 e2 e0r e1r e2r :
90
  Sub e0 e0r  Sub e1 e1r  Sub e2 e2r  Sub (CAS e0 e1 e2) (CAS e0r e1r e2r).
91
Proof. by intros; red; f_equal/=. Qed.
92
End subst.
93 94 95 96

(** * The tactic *)
Ltac simpl_subst :=
  repeat match goal with
97
  | |- context [subst ?x ?es ?e] => progress rewrite (@do_subst x es e)
98 99 100
  | |- _ => progress csimpl
  end.
Arguments subst : simpl never.