Require Import Coq.FSets.FMapPositive.
Require Import Coq.Structures.OrderedTypeEx.
Require Import PArith.
Require Import PArith.POrderedType.

Require Export Conditions.

Fixpoint tbounds (bound: positive) (t: term): Prop :=
 match t with
 | tvar x ⇒ Zpos (vid x) < Zpos bound
 | tcte c ⇒ True
 | tbin op tl tr ⇒ tbounds bound tl ∧ tbounds bound tr
 | told t ⇒ tbounds bound t
 | tapp f t ⇒ tbounds bound t
 end.

Lemma tbounds_Zle t bound1:
   tbounds bound1 t → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → tbounds bound2 t.
Proof.
  induction t; simpl; intuition.
Qed.

Hint Resolve tbounds_Zle: echecker.

Definition frameeq (bound1: Z) (bound2: positive) (s s': state) : Prop
 := ∀ x, bound1 ≤ (Zpos x) < Zpos bound2 → (s x)=(s' x).
Hint Unfold frameeq: checker.

Lemma frameeq_Zle bound1 bound2 bound3 s s':
  (frameeq bound1 bound3 s s') → Zpos bound2 ≤ Zpos bound3
   → frameeq bound1 bound2 s s'.
Proof.
  unfold frameeq; intuition.
Qed.

Lemma frameeq_sym bound1 bound2 s1 s2:
  (frameeq bound1 bound2 s1 s2) → (frameeq bound1 bound2 s2 s1).
Proof.
  unfold frameeq; intros; symmetry; auto.
Qed.

Lemma frameeq_trans bound1 bound2 s1 s2 s3:
  (frameeq bound1 bound2 s1 s2) → (frameeq bound1 bound2 s2 s3) → (frameeq bound1 bound2 s1 s3).
Proof.
  unfold frameeq; intros; eapply eq_trans.
  eapply H; eauto.
  auto.
Qed.

Lemma frameeq_glue bound1 bound2 bound3 s1 s2:
  (frameeq bound1 bound2 s1 s2) → (frameeq (Zpos bound2) bound3 s1 s2) → (frameeq bound1 bound3 s1 s2).
Proof.
  unfold frameeq; intros H1 H2 x H3.
  case (Z_le_dec (Zpos bound2) (Zpos x)); intros.
  apply H2; omega.
  apply H1; omega.
Qed.

Lemma frameeq_teval (t: term): ∀ bound s s',
   tbounds bound t →
    frameeq 0 bound s s' →
      teval t s = teval t s'.
Proof.
  unfold frameeq; induction t; simpl; intuition.
  erewrite IHt1; eauto.
  erewrite IHt2; eauto.
  erewrite IHt; eauto.
Qed.

Hint Resolve frameeq_teval frameeq_Zle frameeq_trans frameeq_glue: echecker.

Lemma add_morphism bound1 bound2 x val1 val2 c1 c2:
  val1=val2 → frameeq bound1 bound2 c1 c2 → frameeq bound1 bound2 (add x val1 c1) (add x val2 c2).
Proof.
  unfold frameeq; intros H H0 x0 H1.
  unfold add. case (Positive_as_DT.eq_dec x x0); auto.
Qed.

Hint Resolve add_morphism: checker.

Lemma add_frameeq_out_1 bound1 bound2 s x y : Zpos x < bound1 → frameeq bound1 bound2 (add x y s) s.
Proof.
  unfold frameeq; intros H.
  intros; rewrite add_out; auto.
  omega.
Qed.

Lemma add_frameeq_out_2 bound1 bound2 s x y : Zpos bound2 ≤ Zpos x → frameeq bound1 bound2 (add x y s) s.
Proof.
  unfold frameeq; intros H.
  intros; rewrite add_out; auto.
  omega.
Qed.

Hint Resolve add_frameeq_out_1 add_frameeq_out_2: checker2.

Fixpoint trename (t:term) (x1 x2: positive) : term
  := match t with
     | tvar x ⇒ if Positive_as_DT.eq_dec x1 (vid x) then tvar (mkvar (vtag x) x2) else t
     | tcte c ⇒ t
     | tbin op tl tr ⇒ tbin op (trename tl x1 x2) (trename tr x1 x2)
     | told t ⇒ trename t x1 x2
     | tapp f t ⇒ tapp f (trename t x1 x2)
     end.

Lemma Psucc_lift n: Zpos (n+1)=(Zpos n)+1.
Proof.
  auto.
Qed.
Hint Rewrite Psucc_lift: rchecker.

Lemma Zpos_Psucc_lt n: Zpos n < Zpos (n+1).
Proof.
  autorewrite with rchecker. omega.
Qed.
Hint Resolve Zpos_Psucc_lt: checker.
Hint Resolve Zlt_trans: echecker2.

Lemma Zpos_Psucc_le n: Zpos n ≤ Zpos (n+1).
Proof.
  autorewrite with rchecker. omega.
Qed.
Hint Resolve Zpos_Psucc_le: echecker.

Lemma tbounds_trename t: ∀ x1 x2, tbounds x2 t →
  tbounds (x2+1) (trename t x1 x2).
Proof.
  induction t; simpl; try (intuition; fail).
  unfold trename.
  case x; clear x; intros s x x1 x2; simpl.
  case (Positive_as_DT.eq_dec x1 x); simpl; eauto with checker echecker2.
Qed.
Hint Resolve tbounds_trename: checker.

Lemma trename_tbounds t: ∀ x1 x2 s dummy, tbounds x2 t →
  teval (trename t x1 x2) (add x2 (s x1) (add x1 dummy s)) = teval t s.
Proof.
  unfold teval; induction t; simpl; try (intuition; fail).
  unfold trename.
  case x; clear x; intros s x x1 x2; simpl.
  case (Positive_as_DT.eq_dec x1 x); simpl.
  intros; subst. auto with checker.
  intros; rewrite add_out; auto with checker.
  omega.
  simpl; intuition; rewrite IHt1; auto.
  rewrite IHt2; auto.
  intros; erewrite IHt; auto.
Qed.
Hint Rewrite trename_tbounds: rchecker.

Fixpoint cbounds (bound: positive) (c:cond): Prop :=
 match c with
 | basic b ⇒ True
 | atom oc tl tr ⇒ tbounds bound tl ∧ tbounds bound tr
 | bin og cl cr ⇒ cbounds bound cl ∧ cbounds bound cr
 | not c ⇒ cbounds bound c
 end.

Lemma cbounds_Zle c bound1:
   cbounds bound1 c → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → cbounds bound2 c.
Proof.
  induction c; simpl; intuition eauto with echecker.
Qed.

Hint Resolve cbounds_Zle: echecker.

Lemma frameeq_eval c: ∀ bound s s',
 frameeq 0 bound s s' →
   cbounds bound c →
     eval c s = eval c s'.
Proof.
  induction c; simpl; intuition.
  erewrite frameeq_teval; eauto.
  erewrite frameeq_teval with (s:=s); eauto.
  erewrite IHc1; eauto.
  erewrite IHc2; eauto.
  erewrite IHc; eauto.
Qed.

Lemma frameeq_eval_imp c bound s s':
   cbounds bound c →
     eval c s →
       frameeq 0 bound s s' →
         eval c s'.
Proof.
  intros; erewrite frameeq_eval in × |- ; eauto.
Qed.
Hint Resolve frameeq_eval_imp: echecker.

Lemma frameeq_eval_imp_s c bound s s':
   cbounds bound c →
     eval c s →
      frameeq 0 bound s' s →
         eval c s'.
Proof.
  intros; erewrite frameeq_eval; eauto.
Qed.
Hint Resolve frameeq_eval_imp_s: echecker.

Definition extend (c: cond) (bound1 bound2: positive) (s s': state): Prop :=
  ∃ sf, eval c sf ∧ (frameeq 0 bound1 sf s') ∧ (frameeq (Zpos bound1) bound2 sf s).

Fixpoint rename (c:cond) (x1 x2: positive) : cond
  := match c with
     | atom oc tl tr ⇒ atom oc (trename tl x1 x2) (trename tr x1 x2)
     | bin og cl cr ⇒ bin og (rename cl x1 x2) (rename cr x1 x2)
     | not c ⇒ not (rename c x1 x2)
     | _ ⇒ c
     end.

Lemma rename_cbounds c: ∀ x1 x2 s dummy, cbounds x2 c →
  eval (rename c x1 x2) (add x2 (s x1) (add x1 dummy s)) = eval c s.
Proof.
  induction c; simpl; intuition auto with checker.
  autorewrite with rchecker; auto.
  rewrite IHc1; auto.
  rewrite IHc2; auto.
  rewrite IHc; auto.
Qed.
Hint Rewrite rename_cbounds: rchecker.

Lemma cbounds_rename c: ∀ x1 x2, cbounds x2 c →
  cbounds (x2+1) (rename c x1 x2).
Proof.
  induction c; try (simpl; intuition; fail).
Qed.
Hint Resolve cbounds_rename: checker.

Lemma Zle_Pmax_l n1 n2: (Zpos n1) ≤ Zpos (Pmax n1 n2).
Proof.
  intros; rewrite Zpos_max.
  apply Zle_max_l.
Qed.

Lemma Zle_Pmax_r n1 n2: (Zpos n2) ≤ Zpos (Pmax n1 n2).
Proof.
  intros; rewrite Zpos_max.
  apply Zle_max_r.
Qed.

Hint Resolve Zle_Pmax_r Zle_Pmax_l: echecker.
Hint Resolve Zle_refl: checker.
Hint Resolve Zle_trans: echecker.
Hint Resolve Zlt_le_trans: echecker2.

Fixpoint tbound (t:term) (bound: positive): positive :=
 match t with
 | tvar x ⇒ Pmax bound ((vid x)+1)%positive
 | tcte c ⇒ bound
 | tbin op tl tr ⇒ tbound tl (tbound tr bound)
 | told t ⇒ tbound t bound
 | tapp f t ⇒ tbound t bound
 end.

Lemma tbound_monotonic t: ∀ bound, (Zpos bound) ≤ Zpos (tbound t bound).
Proof.
  induction t; simpl; intros; eauto with checker echecker.
Qed.

Hint Resolve tbound_monotonic: checker.

Lemma tbound_tbounds t: ∀ bound, (tbounds (tbound t bound) t).
Proof.
  induction t; simpl; intros; eauto with checker echecker echecker2.
Qed.

Hint Resolve tbound_tbounds: checker.

Fixpoint cbound (c:cond) (bound: positive): positive :=
 match c with
 | basic b ⇒ bound
 | atom oc tl tr ⇒ tbound tl (tbound tr bound)
 | bin og cl cr ⇒ cbound cl (cbound cr bound)
 | not c ⇒ cbound c bound
 end.

Lemma cbound_monotonic c: ∀ bound, (Zpos bound) ≤ Zpos (cbound c bound).
Proof.
  induction c; simpl; intros; eauto with checker echecker.
Qed.

Hint Resolve cbound_monotonic: checker.

Lemma cbound_cbounds c: ∀ bound, (cbounds (cbound c bound) c).
Proof.
  induction c; simpl; intuition eauto with checker echecker.
Qed.

Hint Resolve cbound_cbounds: checker.

Record renaming := {
  rmap: PositiveMap.t var ;
  rbound: positive
}.

Definition rbounds bound (r: renaming) :=
 Zpos bound ≤ Zpos (rbound r) ∧
 ∀ x, try (PositiveMap.find x (rmap r)) (fun (x:var) ⇒ Zpos bound ≤ Zpos (vid x) < Zpos (rbound r)) True.

Lemma rbounds_rbound bound r : rbounds bound r → Zpos bound ≤ Zpos (rbound r).
Proof.
  unfold rbounds; intuition.
Qed.

Hint Resolve rbounds_rbound: checker.

Lemma rbounds_Zle bound1 bound2 r : rbounds bound2 r → Zpos bound1 ≤ Zpos bound2 → rbounds bound1 r.
Proof.
  unfold rbounds; intuition.
  eapply try_monotonic; eauto.
  simpl; intuition.
Qed.
Hint Resolve rbounds_Zle: echecker.

Definition rfind (x:var) (r: renaming) :=
 match PositiveMap.find (vid x) (rmap r) with
 | Some x ⇒ x
 | None ⇒ x
 end.

Lemma rbounds_rfind_up (x:var) r bound :
  rbounds bound r → Zpos (vid x) < Zpos (rbound r) → Zpos (vid (rfind x r)) < Zpos (rbound r).
Proof.
  unfold rbounds, rfind; intuition.
  generalize (H2 (vid x)).
  case (PositiveMap.find (vid x) (rmap r)); simpl; intuition.
Qed.

Lemma rbounds_rfind_down (x:var) r bound :
  rbounds bound r → Zpos (vid (rfind x r)) < Zpos bound → (rfind x r)=x.
Proof.
  unfold rbounds, rfind; intuition.
  generalize H0 (H2 (vid x)); clear H0 H2.
  case (PositiveMap.find (vid x) (rmap r)); simpl; intuition.
  assert (Zpos (vid x) ≠ Zpos (vid x)).
  omega.
  case H.
  auto.
Qed.

Lemma vid_rfind (x y: var) r: (vid x)=(vid y) → (vid (rfind x r))=(vid (rfind y r)).
Proof.
  unfold rfind. intros H. rewrite H.
  case (PositiveMap.find (vid y) (rmap r)); simpl; auto.
Qed.

Definition rlift (s:state) (r: renaming) : state :=
 fun x ⇒
 match PositiveMap.find x (rmap r) with
 | Some x ⇒ s (vid x)
 | None ⇒ s x
 end.

Lemma rlift_rfind x s r: rlift s r (vid x) = s (vid (rfind x r)).
Proof.
  unfold rlift, rfind. case (PositiveMap.find (vid x) (rmap r)); simpl; auto.
Qed.

Hint Rewrite rlift_rfind: rchecker.

Lemma rlift_frameeq bound s1 s2 r x :
  frameeq 0 bound (rlift s1 r) s2 → Zpos (vid x) < Zpos bound →
   s1 (vid (rfind x r)) = s2 (vid x).
Proof.
  unfold frameeq; intros H H1. rewrite <- H; intuition.
  autorewrite with rchecker.
  auto.
Qed.

Lemma rlift_add_out_2 bound x y s r: rbounds bound r →
  Zpos (rbound r) ≤ Zpos x → frameeq 0 (rbound r) (rlift (add x y s) r) (rlift s r).
Proof.
  unfold rbounds, rlift, frameeq. intuition.
  generalize (H2 x0).
  case (PositiveMap.find x0 (rmap r)); simpl; auto.
  intros; rewrite add_out; auto.
  omega.
  intros; rewrite add_out; auto.
  omega.
Qed.

Definition rempty (bound: positive): renaming :=
 {| rmap:=PositiveMap.empty _ ;
    rbound:=bound
   |}.

Lemma rempty_rbounds bound: rbounds bound (rempty bound).
Proof.
  unfold rbounds. simpl. intuition. rewrite PositiveMap.gempty; simpl; auto.
Qed.

Lemma rempty_rfind x bound : rfind x (rempty bound)=x.
Proof.
  unfold rempty, rfind; simpl.
  rewrite PositiveMap.gempty; simpl; auto.
Qed.

Hint Rewrite rempty_rfind: rchecker.

Lemma rempty_rlift s bound x: rlift s (rempty bound) x = s x.
Proof.
  unfold rempty, rlift; simpl. rewrite PositiveMap.gempty; simpl; auto.
Qed.

Hint Rewrite rempty_rlift: rchecker.

Definition fresh (x:var) (r: renaming): renaming :=
  let bound:=rbound r in
  {| rmap:= PositiveMap.add (vid x) (mkvar (vtag x) bound) (rmap r) ;
     rbound:= (bound+1)%positive
  |}.

Lemma fresh_rbounds bound x r: rbounds bound r → rbounds bound (fresh x r).
Proof.
  unfold rbounds, fresh; simpl; intuition.
  eauto with echecker.
  rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec x0 (vid x)).
  intros; subst; simpl; intuition auto with checker.
  intros; eapply try_monotonic; eauto.
  simpl; intuition eauto with checker echecker2.
Qed.

Hint Resolve rbounds_rfind_up rbounds_rfind_down: echecker.
Hint Resolve rempty_rbounds fresh_rbounds: checker.

Lemma rfind_fresh_in x r: rfind x (fresh x r) = mkvar (vtag x) (rbound r).
Proof.
  unfold rfind, fresh; simpl.
  rewrite PositiveMap.add_1; auto.
  unfold PositiveMap.E.eq; auto.
Qed.

Hint Rewrite rfind_fresh_in: rchecker.

Lemma rfind_fresh r (x x':var): rfind x' (fresh x r) =
  if (PositiveMap.E.eq_dec (vid x') (vid x)) then mkvar (vtag x) (rbound r) else rfind x' r.
Proof.
 unfold rfind, fresh; simpl.
 rewrite PositiveMapAdditionalFacts.gsspec.
 case (PositiveMap.E.eq_dec (vid x') (vid x)); simpl; auto.
Qed.

Lemma rlift_fresh r (x1:var) s x2: rlift s (fresh x1 r) x2 = add (vid x1) (s (rbound r)) (rlift s r) x2.
Proof.
 unfold rlift, fresh; simpl.
 rewrite PositiveMapAdditionalFacts.gsspec.
 case (PositiveMap.E.eq_dec x2 (vid x1)); simpl.
 intros; subst; rewrite add_in; auto.
 intros; rewrite add_out2; auto.
Qed.

Lemma rlift_fresh_tech:
  ∀ bound r x dummy s, (rbounds bound r) →
   Zpos (vid x) < Zpos bound →
   frameeq 0 (rbound r)
    (rlift (add (rbound r) (s (vid (rfind x r))) (add (vid x) dummy s)) (fresh x r))
    (rlift s r).
Proof.
  unfold frameeq; intros.
  rewrite rlift_fresh.
  rewrite add_in.
  case (PositiveMap.E.eq_dec x0 (vid x)).
  intros; subst.
  rewrite add_in.
  autorewrite with rchecker; auto.
  intros; rewrite add_out2; auto.
  eapply eq_trans.
  eapply rlift_add_out_2; eauto with checker.
  unfold rlift, rbounds in × |- ×.
  intuition.
  generalize (H3 x0); clear H3.
  case (PositiveMap.find x0 (rmap r)); simpl.
  intros; rewrite add_out; auto.
  omega.
  intros; rewrite add_out2; auto.
Qed.


Fixpoint trsubst (t:term) r: term :=
  match t with
  | tvar x ⇒ tvar (rfind x r)
  | tcte c ⇒ t
  | tbin op tl tr ⇒ tbin op (trsubst tl r) (trsubst tr r)
  | told t ⇒ trsubst t r
  | tapp f t ⇒ tapp f (trsubst t r)
  end.

Lemma tbounds_trsubst t: ∀ bound r, rbounds bound r → tbounds (rbound r) t →
  tbounds (rbound r) (trsubst t r).
Proof.
  induction t; simpl; intuition eauto with echecker.
Qed.
Hint Resolve tbounds_trsubst: echecker.

Lemma trsubst_teval_rlift t: ∀ r s,
  teval (trsubst t r) s = teval t (rlift s r).
Proof.
  induction t; simpl; auto.
  intros; autorewrite with rchecker; auto.
  intros r s; rewrite IHt1. rewrite IHt2.
  auto.
  intros; rewrite IHt; auto.
Qed.
Hint Rewrite <- trsubst_teval_rlift: rchecker.

Lemma trsubst_rempty t: ∀ s bound,
  teval (trsubst t (rempty bound)) s = teval t s.
Proof.
  induction t; simpl; intuition.
  autorewrite with rchecker; auto.
  rewrite IHt1. rewrite IHt2; auto.
  rewrite IHt; auto.
Qed.
Hint Rewrite trsubst_rempty: rchecker.

Fixpoint rsubst (c:cond) r : cond
  := match c with
     | atom oc tl tr ⇒ atom oc (trsubst tl r) (trsubst tr r)
     | bin og cl cr ⇒ bin og (rsubst cl r) (rsubst cr r)
     | not c ⇒ not (rsubst c r)
     | _ ⇒ c
     end.

Lemma cbounds_rsubst c: ∀ bound r, rbounds bound r → cbounds (rbound r) c →
  cbounds (rbound r) (rsubst c r).
Proof.
  induction c; simpl; intuition; eauto with echecker.
Qed.
Hint Resolve cbounds_rsubst: echecker.

Lemma rsubst_rempty c: ∀ s bound,
  eval (rsubst c (rempty bound)) s = eval c s.
Proof.
  induction c; simpl; intuition.
  autorewrite with rchecker; auto.
  rewrite IHc1. rewrite IHc2; auto.
  rewrite IHc. auto.
Qed.
Hint Rewrite rsubst_rempty: rchecker.

Lemma rsubst_eval_rlift c: ∀ r s,
  eval (rsubst c r) s = eval c (rlift s r).
Proof.
  induction c; simpl; intuition.
  autorewrite with rchecker; auto.
  rewrite IHc1; rewrite IHc2; auto.
  erewrite IHc; auto.
Qed.
Hint Rewrite <- rsubst_eval_rlift: rchecker.

Lemma rsubst_fresh_cbounds c: ∀ bound r (x:var) dummy s, (rbounds bound r) → cbounds (rbound r) c →
  Zpos (vid x) < Zpos bound →
  eval (rsubst c (fresh x r)) (add (rbound r) (s (vid (rfind x r))) (add (vid x) dummy s)) = eval (rsubst c r) s.
Proof.
  intros. rewrite rsubst_eval_rlift. rewrite rsubst_eval_rlift.
  eapply frameeq_eval; eauto.
  eapply rlift_fresh_tech; eauto.
Qed.

Lemma frameeq_oteval (t: term): ∀ bound old new old' new',
   tbounds bound t →
   tbounds bound t →
    frameeq 0 bound old old' →
     frameeq 0 bound new new' →
      oteval t old new = oteval t old' new'.
Proof.
  unfold frameeq; induction t; simpl; intuition.
  erewrite IHt1; eauto.
  erewrite IHt2; eauto.
  eauto with echecker.
  erewrite IHt; eauto.
Qed.

Lemma frameeq_oeval c: ∀ bound old new old' new',
    frameeq 0 bound old old' →
     frameeq 0 bound new new' →
      cbounds bound c →
      cbounds bound c →
       oeval c old new = oeval c old' new'.
Proof.
  induction c; simpl; intuition.
  erewrite frameeq_oteval; eauto.
  erewrite frameeq_oteval with (new:=new); eauto.
  erewrite IHc1; eauto.
  erewrite IHc2; eauto.
  erewrite IHc; eauto.
Qed.

Fixpoint otrsubst (t:term) r: term :=
  match t with
  | tbin op tl tr ⇒ tbin op (otrsubst tl r) (otrsubst tr r)
  | told t ⇒ trsubst t r
  | tapp f t ⇒ tapp f (otrsubst t r)
  | _ ⇒ t
  end.

Lemma tbounds_otrsubst t: ∀ bound r, rbounds bound r → tbounds (rbound r) t →
  tbounds (rbound r) (otrsubst t r).
Proof.
  induction t; simpl; intuition eauto with echecker.
Qed.
Hint Resolve tbounds_otrsubst: echecker.

Lemma otrsubst_rempty t: ∀ s bound,
  teval (otrsubst t (rempty bound)) s = teval t s.
Proof.
  induction t; simpl; intuition.
  rewrite IHt1. rewrite IHt2; auto.
  autorewrite with rchecker; auto.
  rewrite IHt; auto.
Qed.
Hint Rewrite otrsubst_rempty: rchecker.

Lemma otrsubst_eval_rlift t: ∀ r s,
  teval (otrsubst t r) s = oteval t (rlift s r) s.
Proof.
  induction t; simpl; intuition.
  rewrite IHt1; rewrite IHt2; auto.
  autorewrite with rchecker; auto.
  rewrite IHt; auto.
Qed.
Hint Rewrite <- otrsubst_eval_rlift: rchecker.

Fixpoint orsubst (c:cond) r : cond
  := match c with
     | atom oc tl tr ⇒ atom oc (otrsubst tl r) (otrsubst tr r)
     | bin og cl cr ⇒ bin og (orsubst cl r) (orsubst cr r)
     | not c ⇒ not (orsubst c r)
     | _ ⇒ c
     end.

Lemma cbounds_orsubst c: ∀ bound r, rbounds bound r → cbounds (rbound r) c →
  cbounds (rbound r) (orsubst c r).
Proof.
  induction c; simpl; intuition; eauto with echecker.
Qed.
Hint Resolve cbounds_orsubst: echecker.

Lemma orsubst_rempty c: ∀ s bound,
  eval (orsubst c (rempty bound)) s = eval c s.
Proof.
  induction c; simpl; intuition.
  autorewrite with rchecker; auto.
  rewrite IHc1. rewrite IHc2; auto.
  rewrite IHc; auto.
Qed.
Hint Rewrite orsubst_rempty: rchecker.

Lemma orsubst_eval_rlift c: ∀ r s,
  eval (orsubst c r) s = oeval c (rlift s r) s.
Proof.
  induction c; simpl; intuition.
  rewrite otrsubst_eval_rlift; rewrite otrsubst_eval_rlift; auto.
  rewrite IHc1; rewrite IHc2; eauto.
  rewrite IHc; auto.
Qed.

Definition swap (x y: var) bound :renaming :=
  {| rmap:= PositiveMap.add (vid x) y (PositiveMap.add (vid y) x (PositiveMap.empty _));
     rbound:= bound
  |}.

Lemma swap_rbounds bound1 bound2 (x y: var): Zpos bound1 ≤ Zpos (vid x) < Zpos bound2 → Zpos bound1 ≤ Zpos (vid y) < Zpos bound2 → rbounds bound1 (swap x y bound2).
Proof.
  unfold rbounds, swap; simpl; intuition.
  rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec x0 (vid x)); simpl; auto.
  intros; rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec x0 (vid y)); simpl; auto.
  intros; rewrite PositiveMap.gempty; simpl; auto.
Qed.

Lemma swap_rfind x y z bound:
  rfind z (swap x y bound) =
   if PositiveMap.E.eq_dec (vid z) (vid x)
   then y
   else if PositiveMap.E.eq_dec (vid z) (vid y)
   then x
   else z.
Proof.
  unfold swap, rfind; simpl.
  rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec (vid z) (vid x)); auto.
  rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec (vid z) (vid y)); auto.
  intros; rewrite PositiveMap.gempty; intuition.
Qed.

Lemma swap_rfind_1 x y bound: rfind x (swap x y bound)=y.
Proof.
  unfold swap, rfind; simpl.
  rewrite PositiveMap.add_1; intuition.
Qed.

Lemma swap_rfind_2 x y bound: (vid y)<>(vid x) → rfind y (swap x y bound)=x.
Proof.
  intros H; rewrite swap_rfind.
  case (PositiveMap.E.eq_dec (vid y) (vid x)).
  intros; case H; auto.
  case (PositiveMap.E.eq_dec (vid y) (vid y)); auto.
  intros H0; case H0; auto.
Qed.

Hint Rewrite swap_rfind_1 swap_rfind_2: rchecker.

Lemma swap_rfind_3 x y bound z: (vid z)<>(vid x) → (vid z)<>(vid y) → rfind z (swap x y bound)=z.
Proof.
  intros H H0; rewrite swap_rfind.
  case (PositiveMap.E.eq_dec (vid z) (vid x)).
  intros; case H; auto.
  case (PositiveMap.E.eq_dec (vid z) (vid y)).
  intros; case H0; auto.
  auto.
Qed.

Lemma swap_rlift s x y z bound: rlift s (swap x y bound) z = add (vid x) (s (vid y)) (add (vid y) (s (vid x)) s) z.
Proof.
  unfold rlift, swap; simpl.
 rewrite PositiveMapAdditionalFacts.gsspec.
 case (PositiveMap.E.eq_dec z (vid x)).
 intros; subst; rewrite add_in; auto.
 intros; rewrite add_out2; auto.
 rewrite PositiveMapAdditionalFacts.gsspec.
 case (PositiveMap.E.eq_dec z (vid y)).
 intros; subst; rewrite add_in; auto.
 intros; rewrite add_out2; auto.
 rewrite PositiveMap.gempty; simpl; auto.
Qed.