Require Import Atoms.
Require Import Kernel.
Require Export NaiveTermAbstractions.
Require Import MiscUtils.

Record abs_guard := {
  gconc: cond ;
  gabs: kernel ;
  gproof: ∀ s, eval gconc s → Kangel_wlp gabs (eq s) s
}.

Hint Resolve gproof: checker.

Program Definition abs_ensure (c: abs_guard) := {|
  concrete:= ensure (gconc c) ;
  abstract:= gabs c ;
  certif_correctness:= _
|}.
Obligation 1.
  eapply Kangel_wlp_correctness.
  eauto.
  eauto with checker.
Qed.

Program Definition abs_embed (c: cond) := {|
  gconc:= c ;
  gabs := ensure c ;
  gproof := _
|}.
Coercion abs_embed: cond >-> abs_guard.

Program Definition abs_and (c1 c2: abs_guard) := {|
  gconc:=bin AND (gconc c1) (gconc c2) ;
  gabs:= Kseq (gabs c1) (gabs c2) ;
  gproof:= _
|}.
Obligation 1.
  eapply Kangel_wlp_monotonic.
  eauto with checker.
  intros; subst; eauto with checker.
Qed.

Program Definition abs_or (c1 c2: abs_guard) := {|
  gconc:=bin OR (gconc c1) (gconc c2) ;
  gabs:= Kjoin (gabs c1) (gabs c2) ;
  gproof:= _
|}.
Obligation 1.
  case H; eauto with echecker checker.
Qed.

Require Import KernelVCG.
Require Import Coq.Logic.FunctionalExtensionality.

Program Definition abs_atom (oc: bincmp) (tl tr: abs_term) := {|
  gconc:=Conditions.atom oc (tconc tl) (tconc tr) ;
  gabs :=
   let y := mkvar "gy" 1%positive in
   let x := mkvar "gx" (tbound (tconc tr) 2) in
      Kclone x (Kclone y (Kseq (tabs tl x) (Kseq (tabs tr y) (ensure (Conditions.atom oc x y))))) ;
  gproof := _
|}.
Obligation 1.
  eapply Kangel_wlp_monotonic.
  eapply tproof.
  intros; subst.
  eapply Kangel_wlp_monotonic.
  eapply tproof.
  intros; subst.
  simpl.
  constructor 1.
  rewrite add_out2.
  rewrite add_in.
  rewrite add_in.
  erewrite frameeq_teval with (t:=(tconc tr)).
  eapply H.
  eapply tbound_tbounds with (bound:=2%positive).
  eapply add_frameeq_out_2.
  auto with zarith.
  generalize (tbound_monotonic (tconc tr) 2).
  intros H1 H2; rewrite <- H2 in H1.
  omega.
   apply functional_extensionality.
   intros x1. unfold add at 1.
   case (POrderedType.Positive_as_DT.eq_dec (tbound (tconc tr) 2) x1).
   intros; subst. auto.
   unfold add at 1.
   case (POrderedType.Positive_as_DT.eq_dec 1%positive x1).
   intros; subst; auto.
   intros; repeat (rewrite add_out2; auto).
Qed.

Program Definition abs_cut (c1: cond) (c2: abs_guard | ∀ s, eval c1 s → eval (gconc c2) s) := {|
  gconc := c1 ;
  gabs:=gabs c2 ;
  gproof:= _
|}.
Obligation 1.
  auto with checker.
Qed.

Require Export NaiveAbstractionLib.

Program Definition not_LE (tl tr: term) := {|
  gconc:=not (tl ≤ tr) ;
  gabs:=ensure ((tr+1) ≤ tl) ;
  gproof:=_
|}.
Obligation 1.
  hoare_term_simplify.
  case (Z_le_dec (Zof (teval tr s) + 1) (Zof (teval tl s))); auto.
  intros H0; case H.
  hoare_term_simplify.
Qed.

Program Definition not_EQ (tl tr: term) :=
  abs_cut (not (tl=tr)) (abs_or ((tl+1) ≤ tr) ((tr+1) ≤ tl)).
Obligation 1.
  case (Z_le_dec ((Zof (teval tl s))+1) (Zof (teval tr s))).
  intros; constructor 1; hoare_term_simplify; auto.
  intros; constructor 2; hoare_term_simplify.
  assert (Zof (teval tl s) ≠ Zof (teval tr s)).
  intro X; apply H. apply Zof_intro; auto.
  omega.
Qed.

Require Import Classical_Prop.
Program Fixpoint abs_notx (c: cond) : { g: abs_guard | (gconc g = not c)%type } :=
   abs_cut (not c)
      (match c with
      | basic b ⇒ abs_embed (basic (negb b))
      | Conditions.atom LE tl tr ⇒ not_LE tl tr
      | Conditions.atom EQ tl tr ⇒ not_EQ tl tr
      | bin AND cl cr ⇒ abs_or (abs_notx cl) (abs_notx cr)
      | bin OR cl cr ⇒ abs_and (abs_notx cl) (abs_notx cr)
      | not c0 ⇒ abs_embed c0
      end).
Obligation 1.  destruct b; simpl in × |- *; auto.
Qed.
Obligation 4.  abstract (
   rewrite e; rewrite e0; clear e e0; simpl;
   apply not_and_or; auto).
Defined.
Obligation 5.  abstract (rewrite e; rewrite e0; clear e e0; simpl;
 apply not_or_and; auto).
Defined.
Obligation 6.    apply NNPP; auto.
Qed.

Program Definition abs_not (c: cond): abs_guard := abs_notx c.