Require Export Certificate.
Require Import Kernel.

Fixpoint iter (n:nat) (body: prog) : prog :=
  match n with
  | O ⇒ skip
  | (S n) ⇒ body -; iter n body
  end.

Fixpoint le_iter (n:nat) (body: prog): prog :=
  match n with
  | O ⇒ skip
  | (S n) ⇒ join (le_iter n body) (iter (S n) body)
  end.

Lemma le_iter_stop body n: ∀ s, sem (le_iter n body) s (Some s).
Proof.
  induction n; simpl; eauto with sem.
Qed.
Hint Resolve le_iter_stop: sem.

Lemma le_iter_continue body n: ∀ s s', sem (body -; le_iter n body) s s' → sem (le_iter (S n) body) s s'.
Proof.
  induction n; simpl.
  intros s s' H; inversion_clear H; eauto with sem.
  intros s s' H; inversion_clear H.
  inversion_clear H1; eauto with sem.
  eauto with sem.
Qed.

Lemma unroll_fwd_sem body n: ∀ s s',
   sem (loop body) s s' →
   sem (join (le_iter n body) ((iter (S n) body) -; (loop body))) s s'.
Proof.
  induction n; simpl.
  intros s s' H; inversion_clear H; eauto with sem.
  intros s s' H; inversion_clear H; eauto with sem.
  generalize (IHn _ _ H1); simpl; clear H1 IHn.
  intro H1; inversion_clear H1.
  eapply sem_join_l.
  eapply le_iter_continue.
  eauto with sem.
  inversion_clear H; eauto with sem.
Qed.

Lemma wlp_unroll_fwd_correctness n body post s:
   wlp (join (le_iter n body) ((iter (S n) body) -; (loop body))) post s
  → wlp (loop body) post s.
Proof.
  intro H; eapply wlp_complete.
  intros s' H0; eapply wlp_correctness.
  apply unroll_fwd_sem; eauto.
  eauto.
Qed.

Lemma wlp_succ_iter body (n:nat): ∀ post s, wlp (iter n body -; body) post s → wlp (iter (S n) body) post s.
Proof.
  induction n; simpl; eauto with echecker.
  intros; eapply wlp_monotonic.
  eauto.
  intros; eapply IHn.
  simpl; auto.
Qed.

Lemma iter_Kwlp (p: certif) (n: nat): ∀ post s, Kwlp_iter n (Kwlp (abstract p)) post s → wlp (iter n (concrete p)) post s.
Proof.
  induction n; simpl; auto.
  intros; eapply wlp_succ_iter.
  simpl; eauto with checker echecker.
Qed.
Hint Resolve iter_Kwlp: checker.

Lemma le_iter_Kwlp (p: certif) (n: nat): ∀ post s, Kwlp_le_iter n (Kwlp (abstract p)) post s → wlp (le_iter n (concrete p)) post s.
Proof.
  induction n; simpl; intuition eauto with checker echecker.
  eapply wlp_succ_iter.
  simpl; eauto with checker echecker.
Qed.

Program Definition unrollfwd (n:nat) (label: option alabel) (body: certif) (inv: assertion) (next: certif) :=
{|
  concrete := loop (concrete body) -; (concrete next) ;
  abstract :=
     Kle_iter n label (abstract body) (Kseq (Kloop (abstract body) inv) (abstract next) ) (abstract next) ;
  certif_correctness:= _
|}.
Obligation 1.
  apply wlp_unroll_fwd_correctness with (n:=n).
  constructor 1.
  eapply le_iter_Kwlp.
  eauto with checker echecker.
  eapply iter_Kwlp with (n:=S n).
  change (Kwlp_iter (S n) (Kwlp (abstract body)) (wlp (loop (concrete body) -; (concrete next)) R) s).
  apply Kiter_monotonic with (n:=S n) (P:=Kwlp (Kseq (Kloop (abstract body) inv) (abstract next)) R); eauto with echecker.
  clear H0 H.
  simpl.
  firstorder (auto with checker).
Qed.

Notation "'bloop' body 'fwd' n 'invariant' inv 'then' next 'done'" :=
  (unrollfwd (pred n) None body inv next)
  (at level 95): certif_scope.

Program Definition unroll_all (n:nat) (label: option alabel) (body: certif) (next: certif) := {|
  concrete := (loop (concrete body)) -; (concrete next) ;
  abstract := Kle_iter n label (abstract body) (xrequire absurd "dead code") (abstract next) ;
  certif_correctness:= _
|}.
Obligation 1.
  apply wlp_unroll_fwd_correctness with (n:=n).
  constructor 1.
  eapply le_iter_Kwlp.
  eauto with checker echecker.
  eapply iter_Kwlp.
  simpl; eapply Kiter_monotonic; eauto with echecker.
  intros; eapply Kwlp_monotonic; eauto.
  simpl; intuition.
Qed.

Notation "'bloop' 'split' label body 'all' n 'then' next 'done'" :=
  (unroll_all n (Some label) body next)
  (at level 95, label at level 0): certif_scope.