From iris.heap_lang Require Export lang.
Import heap_lang.

(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
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.

(* Variables *)
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.

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

(** Rec *)
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) _) =>
  match eval vm_compute in (bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y)) with
  | true => eapply (do_subst_rec_true ltac:(bool_decide_no_check))
  | false => eapply (do_subst_rec_false ltac:(bool_decide_no_check))
  end : typeclass_instances.

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.

(* Values *)
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.

(* Boring connectives *)
Section subst.
Context (x : string) (es : expr).
Notation Sub := (Subst x es).

(* Ground terms *)
Global Instance do_subst_lit l : Sub (Lit l) (Lit l).
Proof. done. Qed.
Global Instance do_subst_app e1 e2 e1r e2r :
  Sub e1 e1r → Sub e2 e2r → Sub (App e1 e2) (App e1r e2r).
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).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_binop op e1 e2 e1r e2r :
  Sub e1 e1r → Sub e2 e2r → Sub (BinOp op e1 e2) (BinOp op e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_if e0 e1 e2 e0r e1r e2r :
  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (If e0 e1 e2) (If e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_pair e1 e2 e1r e2r :
  Sub e1 e1r → Sub e2 e2r → Sub (Pair e1 e2) (Pair e1r e2r).
Proof. by intros ??; red; f_equal/=. Qed.
Global Instance do_subst_fst e er : Sub e er → Sub (Fst e) (Fst er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_snd e er : Sub e er → Sub (Snd e) (Snd er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_injL e er : Sub e er → Sub (InjL e) (InjL er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_injR e er : Sub e er → Sub (InjR e) (InjR er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_case e0 e1 e2 e0r e1r e2r :
  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (Case e0 e1 e2) (Case e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_fork e er : Sub e er → Sub (Fork e) (Fork er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_load e er : Sub e er → Sub (Load e) (Load er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_store e1 e2 e1r e2r :
  Sub e1 e1r → Sub e2 e2r → Sub (Store e1 e2) (Store e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_cas e0 e1 e2 e0r e1r e2r :
  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (CAS e0 e1 e2) (CAS e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
End subst.

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