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

Require Export Renaming.

Fixpoint lbounds bound (l: list var) : Prop :=
 match l with
 | nil ⇒ True
 | x::l ⇒ (Zpos (vid x)) < Zpos bound ∧ lbounds bound l
 end.

Lemma lbounds_Zle l bound1:
   lbounds bound1 l → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → lbounds bound2 l.
Proof.
  induction l; simpl; intuition eauto with echecker2.
Qed.

Hint Resolve lbounds_Zle: echecker.

Fixpoint lbound (l: list var) (bound: positive): positive :=
 match l with
 | nil ⇒ bound
 | x::l ⇒ lbound l (Pmax ((vid x)+1)%positive bound)
 end.

Lemma lbound_monotonic l: ∀ bound, (Zpos bound) ≤ Zpos (lbound l bound).
Proof.
  induction l; simpl; intros; eauto with checker echecker.
Qed.

Hint Resolve lbound_monotonic: checker.

Lemma lbound_lbounds l: ∀ bound, (lbounds (lbound l bound) l).
Proof.
  induction l; simpl; intuition eauto with checker echecker echecker2.
Qed.

Hint Resolve lbound_lbounds: checker.

Lemma lframeeq_nil_invert bound1 bound2 s s':
  lframeeq nil s s' → frameeq bound1 bound2 s s'.
Proof.
  unfold lframeeq; simpl.
  unfold frameeq; intuition.
Qed.

Lemma lframeeq_cons_invert l x s s':
  lframeeq (x::l) s s' → lframeeq l (add (vid x) (s' (vid x)) s) s'.
Proof.
  unfold lframeeq; simpl.
  intros; unfold add; case (Positive_as_DT.eq_dec (vid x) x0); intuition subst; auto.
Qed.

Fixpoint lfreshx (l:list var) (r:renaming) : renaming :=
  match l with
  | nil ⇒ r
  | x::l ⇒ lfreshx l (fresh x r)
  end.

Lemma lfreshx_rbounds l: ∀ bound r, rbounds bound r → rbounds bound (lfreshx l r).
Proof.
  induction l; simpl; auto with checker.
Qed.

Lemma lfreshx_rbound l: ∀ r, Zpos (rbound r) ≤ Zpos (rbound (lfreshx l r)).
Proof.
  induction l; simpl; intros; auto with checker.
  eapply Zle_trans.
  2: apply IHl.
  simpl; auto with checker echecker.
Qed.

Hint Resolve lfreshx_rbounds lfreshx_rbound: checker.

Definition lfresh l bound := lfreshx l (rempty bound).

Lemma lfresh_rbounds l bound: rbounds bound (lfresh l bound).
Proof.
  unfold lfresh; intros; auto with checker.
Qed.

Lemma lfresh_rbound l: ∀ bound, Zpos bound ≤ Zpos (rbound (lfresh l bound)).
Proof.
  unfold lfresh; intros.
  eapply Zle_trans.
  2: auto with checker.
  simpl; auto with checker.
Qed.

Hint Resolve lfresh_rbound lfresh_rbounds: echecker.

Lemma add_tech1 bound s1 s2 x: frameeq 0 bound s2 s1 → Zpos x < Zpos bound
  → frameeq 0 bound (add x (s1 x) s2) s1.
Proof.
  unfold frameeq; intros H2 H3 y H4.
  intros; rewrite <- H2; intuition.
  autorewrite with rchecker.
  intuition.
Qed.

Hint Resolve add_tech1: checker.


Fixpoint ladd (l:list var) (r: renaming) (s s': state): state :=
  match l with
  | nil ⇒ s'
  | x::l ⇒ ladd l (fresh x r) s (add (rbound r) (s' (vid (rfind x r))) (add (vid x) (s (vid x)) s'))
  end.

Lemma add_tech2 bound s1 s2 x r: rbounds bound r → frameeq 0 bound s2 s1 → Zpos (vid x) < Zpos bound
  → frameeq 0 bound (add (rbound r) (s2 (vid (rfind x r))) (add (vid x) (s1 (vid x)) s2)) s1.
Proof.
  intros H1 H2 H3.
  eapply frameeq_trans.
  eapply add_frameeq_out_2; eauto.
  auto with checker.
  auto with checker.
Qed.

Hint Resolve add_tech2: checker.

Hint Resolve lframeeq_nil_invert:checker.

Lemma ladd_frameeq_1 l: ∀ bound s1 s2 s3 r,
 lframeeq l s3 s1 →
  rbounds bound r →
  lbounds bound l →
  frameeq 0 bound s2 s3 →
     frameeq 0 bound (ladd l r s1 s2) s1.
Proof.
  induction l; simpl; intuition.
  eauto with checker echecker.
  eapply IHl.
  eapply lframeeq_cons_invert; eauto.
  auto with checker.
  auto.
  eapply frameeq_trans; eauto with checker2 checker.
Qed.

Lemma ladd_frameeq_2 l: ∀ bound1 bound2 s1 s2 s3 r,
 Zpos bound1 ≤ Zpos bound2
 → lframeeq l s3 s1
 → lbounds bound1 l
 → rbounds bound2 r
 → frameeq 0 bound1 s2 s3
 → frameeq (Zpos bound1) bound2 (ladd l r s1 s2) s2.
Proof.
  induction l; simpl; intuition.
  eapply frameeq_trans.
  eapply IHl; auto.
  eapply lframeeq_cons_invert; eauto.
  eauto with checker echecker.
  eapply frameeq_trans.
  eapply add_frameeq_out_2; eauto with checker echecker.
  auto with checker.
  clear IHl.
  eapply frameeq_trans.
  eapply add_frameeq_out_2; eauto.
  auto with checker.
  auto with checker2.
Qed.

Lemma eval_rsubst_lfreshx l: ∀ c bound r s s0 s',
  cbounds (rbound r) c
  → lframeeq l s s'
  → rbounds bound r
  → lbounds bound l
  → frameeq 0 bound s0 s
  → eval (rsubst c r) s0
  → eval (rsubst c (lfreshx l r)) (ladd l r s' s0).
Proof.
  induction l; simpl; intuition.
  intros; eapply IHl; clear IHl; simpl.
  eauto with echecker checker.
  intros; eapply lframeeq_cons_invert.
  eapply H0.
  eauto with echecker checker.
  auto.
  eapply frameeq_trans.
  eapply add_frameeq_out_2; eauto with checker.
  eauto with checker.
  erewrite rsubst_fresh_cbounds; eauto.
Qed.

Lemma eval_rsubst l: ∀ c bound1 bound2 s s0 s',
  cbounds bound2 c
  → Zpos bound1 ≤ Zpos bound2
  → lbounds bound1 l
  → frameeq 0 bound1 s0 s
  → eval c s0
  → lframeeq l s s'
  → eval (rsubst c (lfresh l bound2)) (ladd l (rempty bound2) s' s0).
Proof.
  intros; unfold lfresh.
  eapply eval_rsubst_lfreshx; eauto.
  eauto with checker echecker.
  autorewrite with rchecker; auto.
Qed.

Lemma eval_orsubst_lfreshx l: ∀ c bound r s s0 s',
  lframeeq l s s'
  → rbounds bound r
  → lbounds bound l
  → cbounds bound c
  → frameeq 0 bound s0 s
  → oeval c (rlift s0 r) s'
  → eval (orsubst c (lfreshx l r)) (ladd l r s' s0).
Proof.
  induction l; simpl; intuition.
  rewrite orsubst_eval_rlift.
  erewrite frameeq_oeval; eauto with checker.
  eapply frameeq_trans; eauto with checker.
  intros; eapply IHl; clear IHl.
  intros; eapply lframeeq_cons_invert.
  eapply H.
  eauto with echecker checker.
  auto.
  auto.
  eapply frameeq_trans.
  eapply add_frameeq_out_2; eauto with checker.
  eauto with checker.
  erewrite frameeq_oeval; eauto with checker.
  eapply frameeq_Zle.
  eapply rlift_fresh_tech; eauto.
  auto with checker.
Qed.

Lemma eval_orsubst l: ∀ c bound1 bound2 s s0 s',
  Zpos bound1 ≤ Zpos bound2
  → lbounds bound1 l
  → cbounds bound1 c
  → frameeq 0 bound1 s0 s
  → lframeeq l s s'
  → oeval c s s'
  → eval (orsubst c (lfresh l bound2)) (ladd l (rempty bound2) s' s0).
Proof.
  intros; unfold lfresh.
  eapply eval_orsubst_lfreshx; eauto.
  eauto with checker echecker.
  erewrite frameeq_oeval; eauto with checker.
  unfold frameeq in × |- ×.
  intros; autorewrite with rchecker; auto.
Qed.

Lemma guassign_vc: ∀ l (pre post: cond) bound1 bound2 s s0 s',
  cbounds bound2 pre
  → Zpos bound1 ≤ Zpos bound2
  → lbounds bound1 l
  → cbounds bound1 post
  → frameeq 0 bound1 s0 s
  → eval pre s0
  → lframeeq l s s'
  → oeval post s s'
  → extend (bin AND (rsubst pre (lfresh l bound2))
                     (orsubst post (lfresh l bound2)))
                       bound1 bound2 s0 s'.
Proof.
  unfold extend; intuition.
  constructor 1 with (x:=ladd l (rempty bound2) s' s0); simpl; intuition.
  eapply eval_rsubst; eauto.
  eapply eval_orsubst; eauto.
  eapply ladd_frameeq_1; eauto with checker echecker.
  eapply ladd_frameeq_2; eauto with checker echecker.
Qed.