Require Import MiscUtils.
Require Export Renaming.
Require Import BoundedIteration.
Require Import Coq.FSets.FMapPositive.
Require Import Coq.Structures.OrderedTypeEx.
Require Import ZArith.
Open Scope Z_scope.

Record aentry : Set := {
  acond: cond ;

  abranch: Z

}.

Record alabel : Set := mklabel {
  labmin: Z ;
  labmax: Z ;
  labid: positive
}.

Definition mkseqlabel id := mklabel 0 0 id.
Definition mkjoinlabel id := mklabel 0 1 id.

Definition adefault := {| acond := absurd ; abranch := 0 |}.

Definition aenvironment := PositiveMap.t aentry.

Definition aempty : aenvironment := PositiveMap.empty _.

Definition aadd (x: positive) (val: aentry) (aenv: aenvironment): aenvironment := PositiveMap.add x val aenv.

Definition oadd (ox: option alabel) (acond:cond) (abranch:Z) (aenv: aenvironment): aenvironment :=
  match ox with
  | Some x ⇒ aadd (labid x) {| acond := acond ; abranch := abranch |} aenv
  | None ⇒ aenv
  end.

Definition afind x (aenv: aenvironment) :=
 match PositiveMap.find x aenv with
 | Some val ⇒ val
 | None ⇒ adefault
 end.

Definition aebounds (bound: positive) aenv :=
  ∀ x, cbounds bound (acond (afind x aenv)).

Lemma aempty_aebounds bound: aebounds bound aempty.
Proof.
  intros x; case x; simpl; auto.
Qed.

Lemma aadd_aebounds bound x val aenv : aebounds bound aenv → cbounds bound (acond val) →
  aebounds bound (aadd x val aenv).
Proof.
  unfold aebounds, aadd, afind.
  intros H H0 y. rewrite PositiveMapAdditionalFacts.gsspec.
  case (PositiveMap.E.eq_dec y x); intros; subst; simpl; intuition auto with checker.
Qed.

Hint Resolve aempty_aebounds: checker.
Hint Resolve aadd_aebounds: echecker.

Lemma oadd_aebounds bound ox acond abranch aenv : aebounds bound aenv → cbounds bound acond →
  aebounds bound (oadd ox acond abranch aenv).
Proof.
  case ox; simpl; auto with echecker.
Qed.

Hint Resolve oadd_aebounds: echecker.

Lemma aebounds_Zle aenv bound1:
   aebounds bound1 aenv → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → aebounds bound2 aenv.
Proof.
  unfold aebounds; intuition eauto with echecker.
Qed.

Hint Resolve aebounds_Zle: echecker.

Inductive assertion : Set :=
  | simple (c: cond)
  | conj (a1 a2: assertion)
  | inv (label: alabel)
  | branch2 (label: alabel) (a1 a2: assertion)
  | branch (label: alabel) (a: Z → assertion).

Coercion simple: cond >-> assertion.

Definition safe_branch {A} (l: alabel) aenv (f: Z → A) (default:A) :=
  let x:=(abranch (afind (labid l) aenv)) in
  if Zle_bool (labmin l) x &&& Zle_bool x (labmax l) then f x else default.

Lemma safe_branch_ind {A} l aenv f default (P: A → Prop): P default → (∀ z, (labmin l) ≤ z ≤ (labmax l) → P (f z)) → P (safe_branch l aenv f default).
Proof.
  unfold safe_branch. generalize (Zle_cases (labmin l) (abranch (afind (labid l) aenv))) (Zle_cases (abranch (afind (labid l) aenv)) (labmax l)).
  case (Zle_bool (labmin l) (abranch (afind (labid l) aenv))); simpl; auto.
  case (Zle_bool (abranch (afind (labid l) aenv)) (labmax l)); simpl; auto.
Qed.

Ltac branch_ind :=
   match goal with
   | |- appcontext [safe_branch ?l ?aenv ?f ?default] ⇒
         pattern (safe_branch l aenv f default);
         apply (safe_branch_ind l aenv f default);
         try (simpl; intuition; fail)
   | |- _ ⇒ fail 1 "not found any safe_branch application in the current goal"
   end.

Fixpoint aeval (a: assertion) aenv: cond :=
  match a with
  | simple c ⇒ c
  | conj a1 a2 ⇒ bin AND (aeval a1 aenv) (aeval a2 aenv)
  | inv l ⇒ acond (afind (labid l) aenv)
  | branch2 l a1 a2 ⇒ if Zeq_bool (abranch (afind (labid l) aenv)) (labmin l) then (aeval a1 aenv) else (aeval a2 aenv)
  | branch l a ⇒ safe_branch l aenv (fun z ⇒ aeval (a z) aenv) absurd
  end.

Fixpoint abounds (bound: positive) (a: assertion): Prop :=
  match a with
  | simple c ⇒ cbounds bound c
  | conj a1 a2 ⇒ abounds bound a1 ∧ abounds bound a2
  | inv l ⇒ True
  | branch2 l a1 a2 ⇒ abounds bound a1 ∧ abounds bound a2
  | branch l a ⇒ ∀ z, (labmin l) ≤ z ≤ (labmax l) → abounds bound (a z)
  end.

Lemma abounds_Zle a bound1:
   abounds bound1 a → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → abounds bound2 a.
Proof.
  induction a; simpl; intuition eauto with echecker.
Qed.

Hint Resolve abounds_Zle: echecker.

Lemma aeval_bounds (bound: positive) (a: assertion) (aenv: aenvironment) :
  abounds bound a → aebounds bound aenv → cbounds bound (aeval a aenv).
Proof.
  induction a; simpl; intuition eauto with echecker.
  case (Zeq_bool (abranch (afind (labid label) aenv)) (labmin label)); eauto with echecker.
  branch_ind.
Qed.

Hint Resolve aeval_bounds: echecker.

Fixpoint abound (a:assertion) (bound: positive): positive :=
  match a with
  | simple c ⇒ cbound c bound
  | conj a1 a2 ⇒ abound a1 (abound a2 bound)
  | inv l ⇒ bound
  | branch2 l a1 a2 ⇒ abound a1 (abound a2 bound)
  | branch l a ⇒ biter (labmin l) (labmax l) (fun z ⇒ abound (a z)) bound
  end.

Ltac do_except_on f tac :=
   match goal with
   | |- appcontext [f] ⇒ idtac
   | |- _ ⇒ tac
   end.

Lemma abound_monotonic a: ∀ bound, (Zpos bound) ≤ Zpos (abound a bound).
Proof.
  induction a; simpl; intros; do_except_on @biter ltac:(eauto with checker echecker).
  biter_ind; auto with zarith.
  intros; eapply Zle_trans.
  2: apply H.
  auto.
Qed.

Hint Resolve abound_monotonic: checker.

Lemma abound_abounds a: ∀ bound, (abounds (abound a bound) a).
Proof.
  induction a; simpl; do_except_on @biter ltac:(intuition eauto with checker echecker).
  intros bound z; biter_ind.
  intros n x H0 H1 H2.
  biter_split_le H2.
  intros; eapply abounds_Zle.
  eapply H1.
  omega.
  auto with checker.
Qed.

Hint Resolve abound_abounds: checker.