Require Import NaiveAbstractionLib.
Require Import LoopsUnrolling.

Notation "'bloop' p 'done'" := (loop p) (at level 95): prog_scope.
Notation "str ! n" := (mkvar str n) (at level 7, no associativity, format "str '!' n"): term_scope.

Bind Scope assertion_scope with assertion.
Delimit Scope assertion_scope with assertion.
Infix "&" := conj (at level 98, left associativity): assertion_scope.
Open Scope assertion_scope.

Ltac quantify x :=
  match goal with
  | |- ?p ⇒ match p with
            | appcontext [x ?n] ⇒ generalize (x n)
            end
  end.

Ltac atom :=
  let n := fresh "x" in
  intro n; repeat (quantify n); intuition subst; zof_simplify.

Ltac splitconj :=
  match goal with
  | |- and ?p1 ?p2 ⇒ constructor 1
  end.

Ltac simplify_vc_eval :=
  vm_compute; (repeat splitconj); (atom || auto).

Section LoopExample.

Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let r := "r"!4.

Let source : prog :=
  ensure (1 ≤ x ∧ x ≤ 10) -;
  join (ensure (x ≤ 5) -; assign y (x+5))
       (ensure (6 ≤ x) -; assign y (x-5)) -;
  assign i 0 -;
  assign r 0 -;
  bloop
     ensure (i ≤ x-1) -;
     assign i (i+1) -;
     assign r (r+y)
  done -;
  ensure (x ≤ i) -;
  require (x ≤ r ∧ r ≤ x×10) -;
  require (1 ≤ r ∧ r ≤ 100).

Open Scope certif_scope.

Let annotated1 : certif :=
  ensure (1 ≤ x ∧ x ≤ 10) -;
  cjoin (ensure (x ≤ 5) -; assign y (x+5))
       (ensure (6 ≤ x) -; assign y (x-5)) -;
  assign i 0 -;
  assign r 0 -;
  stdloop (
     ensure (i ≤ x-1) -;
     assign i (i+1) -;
     assign r (r+y)
  ) (i ≤ x ∧ 1 ≤ x ∧ x ≤ 10 ∧ 1 ≤ y ∧ y ≤ 10 ∧ i ≤ r ∧ r ≤ i×10) -;
  ensure (x ≤ i) -;
  require (x ≤ r ∧ r ≤ x×10) -;
  require (1 ≤ r ∧ r ≤ 100).


Lemma annotated1_proof: is_ok source.
Proof.
  apply vcg_correctness with (cert:=annotated1).
  vm_compute; auto.
  simplify_vc_eval; try omega.
Qed.

Let label := mkjoinlabel 3%positive.

Let annotated2 : certif :=
  ensure (1 ≤ x ∧ x ≤ 10) -;
  cjoin (ensure (x ≤ 5) -; assign y (x+5))
       (ensure (6 ≤ x) -; assign y (x-5)) -;[label]
  assign i 0 -;
  assign r 0 -;
  stdloop (
     ensure (i ≤ x-1) -;
     assign i (i+1) -;
     assign r (r+y)
  ) (inv label & i ≤ x ∧ i ≤ r ∧ r ≤ i×10) -;
  ensure (x ≤ i) -;
  require (x ≤ r ∧ r ≤ x×10) -;
  require (1 ≤ r ∧ r ≤ 100).


Lemma annotated2_proof: is_ok source.
Proof.
  apply vcg_correctness with (cert:=annotated2).
  vm_compute; auto.
  simplify_vc_eval; try omega.
Qed.

Close Scope certif_scope.

End LoopExample.

Section AbstractionExample.

Let x := "x"!1.
Let y := "y"!2.

Let source : prog :=
  ensure (5 ≤ x ∧ 1 ≤ y ∧ y ≤ 3) -;
  assign y ((x×3)*(y+2)) -;
  require (5 ≤ x ∧ x×9 ≤ y ∧ y ≤ x×15).

Open Scope certif_scope.

Let annotated : certif :=
  ensure (5 ≤ x ∧ 1 ≤ y ∧ y ≤ 3) -;
  abs_assign y (mult_pos_interv (x×3) (y+2) (3,5)) -;
  xrequire (5 ≤ x ∧ x×9 ≤ y ∧ y ≤ x×15) "main".


Goal is_ok source.
Proof.
  apply vcg_correctness with (cert:=annotated).
  vm_compute; auto.
  simplify_vc_eval; try omega.
Qed.

Close Scope certif_scope.

End AbstractionExample.

Section UnroolBasicExample.

Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let r := "r"!4.

Let source : prog :=
  ensure (x ≤ 3) -;
  ensure (0 ≤ y) -;
  assign i 1 -;
  assign r 0 -;
  bloop
     ensure (i ≤ x) -;
     assign i (i+1) -;
     assign r (r+y)
  done -;
  ensure (x+1 ≤ i) -;
  require (0 ≤ r ∧ r ≤ y×3).

Open Scope certif_scope.

Let annotated : certif :=
  ensure (x ≤ 3) -;
  ensure (0 ≤ y) -;
  assign i 1 -;
  assign r 0 -;
  unroll_all 3%nat None (
    ensure (i ≤ x) -;
    assign i (i+1) -;
    assign r (r+y)
  ) (ensure (x+1≤i)) -;
  require (0 ≤ r ∧ r ≤ y×3).


Goal is_ok source.
Proof.
  apply vcg_correctness with (cert:=annotated).
  vm_compute; auto.
  simplify_vc_eval; try omega.
Qed.

Close Scope certif_scope.

End UnroolBasicExample.

Section GuassignExample.

Let x := "x"!1.
Let y := "y"!2.
Let z := "z"!3.
Let t := "t"!4.
Let u := "u"!5.
Let v := "v"!6.

Open Scope certif_scope.

Let essai: certif :=
  assign u 100 -;
  assign v 200 -;
  assign t 250 -;
  assign z 30 -;
  guassign [u;x;y;t] (u = (told t) ∧ t = (told u) ∧ (told (u+v)) = x ∧ x+v = y) -;
  require (250 = u) -;
  require (t=100) -;
  require (v=200) -;
  require (z=30) -;
  require (300=x) -;
  require (y=500).

Let list := vcg essai.


Goal vc_eval list.
Proof.
  simplify_vc_eval; auto; try omega.
Qed.

Close Scope certif_scope.

End GuassignExample.

Section LetTerm.

Let x := "x"!1.

Let y := "y"!2.

Let source : prog :=
  ensure (1 ≤ x ∧ x ≤ 4 ∧ 0 ≤ y) -;
  assign x ((x-1)*((x+y-1)*x)) -;
  require (0 ≤ x ∧ x ≤ y×12+36).

Open Scope certif_scope.

Let z := "z"!3.

Let annotated : certif :=
  ensure (1 ≤ x ∧ x ≤ 4 ∧ 0 ≤ y) -;
  abs_assign x
    (let_term z := mult_pos_interv (x+y-1) x (1,4) in
                   mult_interv_pos (x-1) z (0,3)) -;
  require (0 ≤ x ∧ x ≤ y×12+36).

Eval vm_compute in abstract annotated.

Goal is_ok source.
Proof.
   apply vcg_correctness with (cert:=annotated).
   vm_compute; auto.
   simplify_vc_eval; try omega.
Qed.


Let annotatedy : certif :=
  ensure (1 ≤ x ∧ x ≤ 4 ∧ 0 ≤ y) -;
  abs_assign x
    (let_term y := mult_pos_interv (x+y-1) x (1,4) in
                   mult_interv_pos (x-1) y (0,3)) -;
  require (0 ≤ x ∧ x ≤ y×12+36).


Goal is_ok source.
Proof.
   apply vcg_correctness with (cert:=annotatedy).
   vm_compute; auto.
   simplify_vc_eval; try omega.
Qed.

Close Scope certif_scope.

End LetTerm.

Section Misc1.

Let x := "x"!1.
Let y := "y"!2.
Let r := "r"!3.

Open Scope certif_scope.

Let annotated : certif :=
  ensure (6 ≤ r ∧ r ≤ 50 ∧ 7 ≤ x+y ∧ x+y ≤ 15) -;
  assign r (r+x+y) -;
  require (13 ≤ r ∧ r ≤ 65).

Close Scope certif_scope.

Goal vc_eval (vcg annotated).
Proof.
  simplify_vc_eval; auto; try omega.
Qed.

End Misc1.