Module Octagons


Require Import Utf8.
Require Import Reals.
Require Import IdealExpr.
Require Import AbIdealNonrel.
Require Import ZArith.
Require Import Coqlib.
Require Import Integers.
Require Import AdomLib.
Require Import AbIdealEnv ShareTree Util TreeAl.
Require Import FloatLib.
Require Import LinearQuery AbLinearize.
Require Import ZIntervals FloatIntervals IdealIntervals.
Require Import FactMsgHelpers.
Require Import ToString.

Local Existing Instance fitv_gamma_oR.
Local Existing Instance fitv_gamma_R.

Inductive ovar :=
| ovPlus (v:var)
| ovMinus (v:var).

Instance ovar_tostring {_:ToString var}: ToString ovar :=
  fun x =>
    match x with
    | ovPlus x => ("+"++to_string x)%string
    | ovMinus x => ("-"++to_string x)%string
    end.

Definition oρ (ρ : var -> ideal_num) (x:ovar) : option R :=
  match x with
  | ovPlus x => rρ ρ x
  | ovMinus x => option_map Ropp (rρ ρ x)
  end.

Definition ovar_opp (x:ovar) : ovar :=
  match x with
  | ovPlus v => ovMinus v
  | ovMinus v => ovPlus v
  end.

Lemma ovar_opp_opp:
  ∀ ρ v x, oρ ρ v = Some (-x) <-> oρ ρ (ovar_opp v) = Some x.
Proof.
  destruct v; simpl.
  - destruct rρ; simpl. 2:intuition congruence.
    split; intros; inv H; rewrite Ropp_involutive; auto.
  - destruct rρ; simpl. 2:intuition congruence.
    split; intros; inv H; f_equal; Psatz.lra.
Qed.

Module ovar_EQ <: TYPE_EQ
    with Definition s := ovar
    with Definition t := (var * (unit + unit))%type.

  Definition s := ovar.
  Definition t := (var * (unit + unit))%type.

  Definition t_of_s (x:s) : t :=
    match x with
    | ovPlus x => (x, inl tt)
    | ovMinus x => (x, inr tt)
    end.

  Definition s_of_t (x:t) : s :=
    match x with
    | (x, inl _) => ovPlus x
    | (x, inr _) => ovMinus x
    end.

  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.
Proof.
intros []; reflexivity. Qed.

  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.
Proof.
intros [? [[]|[]]]; reflexivity. Qed.

  Instance eq : EqDec s.
Proof.
unfold EqDec. decide equality; apply eq_dec. Defined.
End ovar_EQ.

Module SUU := SumShareTree(UnitShareTree)(UnitShareTree).
Module PTSUU := ProdShareTree(T)(SUU).
Module To := BijShareTree(ovar_EQ)(PTSUU).
Module Top := ShareTree_Properties(To).
Module Too := ProdShareTree(To)(To).
Module Toop := ShareTree_Properties(Too).

Instance ovar_eq : EqDec ovar := To.elt_eq.

Definition fin_float := {f:float | is_finite f = true}.

Definition proj_fin_float (f:fin_float) : float := proj1_sig f.
Coercion proj_fin_float : fin_float >-> float.
Lemma proj_fin_float_finite :
  ∀ (f:fin_float), is_finite f = true.
Proof.
intros. apply (proj2_sig f). Qed.
Hint Resolve proj_fin_float_finite.

Instance fin_float_eqdec : EqDec fin_float.
Proof.
  unfold EqDec. intros. destruct (Float.eq_dec x y).
  - left. abstract (destruct x, y; simpl in e; subst; f_equal; apply Axioms.proof_irr).
  - right. abstract (contradict n; congruence).
Defined.

Definition fin_float_of_float (f:float) : option fin_float :=
  match is_finite f with
  | true => fun EQ => Some (exist _ f EQ)
  | false => fun _ => None
  end eq_refl.

Lemma fin_float_of_float_correct:
  ∀ f f',
    fin_float_of_float f = Some f' ->
    is_finite f = true /\ f = f'.
Proof.
  intros f f'. unfold fin_float_of_float.
  destruct f; intro EQ; inv EQ; auto.
Qed.

Ltac destruct_fin_float_of_float :=
  match goal with
  | |- context [fin_float_of_float ?F] =>
    let H := fresh "FFOF" in
    assert (H:=fin_float_of_float_correct F);
    destruct (fin_float_of_float F);
    [specialize (H _ eq_refl)|clear H]
  end.

Definition t := Too.t fin_float.
Definition iter_t := (t * Too.t unit)+⊥.

Instance t_tostring {_:ToString var}: ToString t :=
  fun x =>
    (Too.fold (fun acc xy (b:fin_float) =>
       let '(x, y) := xy in
       acc ++ "[" ++ to_string x ++ to_string (ovar_opp y) ++ "<=" ++ to_string (b:float)++"]")
       x "{" ++ "}")%string.

Instance octitert_tostring {_:ToString var} : ToString iter_t :=
  to_string ∘ (fmap fst).

Instance ogamma: gamma_op t (var -> ideal_num) :=
  fun ab ρ =>
    ∀ x y b, Too.get (x, y) ab = Some b ->
    ∃ xv yv, oρ ρ x = Some xv /\ oρ ρ y = Some yv /\ (xv-yv <= b).

Instance ogamma_it_0: gamma_op (t * Too.t unit) (var -> ideal_num) :=
  γ ∘ fst.


Definition bound_leb (b1 b2:option fin_float) : bool :=
  match b2, b1 with
  | None, _ => true
  | _, None => false
  | Some (exist b2' _), Some (exist b1' _) =>
    if Fleb b1' b2' then true else false
  end.

Definition bound_min (b1 b2:option fin_float) : option fin_float :=
  if bound_leb b1 b2 then b1 else b2.

Lemma bound_min_either:
  ∀ b1 b2 (P:option fin_float -> Prop),
    (P b1) -> (P b2) -> (P (bound_min b1 b2)).
Proof.
  intros. unfold bound_min. destruct bound_leb; auto.
Qed.

Lemma reduct_rule_1:
  ∀ x y z (f1 f2:fin_float),
    (x - y <= f1) -> (y - z <= f2) ->
    let b := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2 in
    is_finite b = true ->
    (x - z <= b).
Proof.
  intros.
  assert (x-z<=f1+f2) by Psatz.lra.
  eapply Rle_trans. eauto.
  eapply Rle_trans.
  { edestruct (round_UP_pt radix2) as (A & B & C).
    apply (fexp_correct 53 1024 eq_refl). apply B. }
  pose proof Bplus_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2.
  Rlt_bool_case H3. simpl in H3.
  - apply Req_le. symmetry; apply H3; auto.
  - destruct H3; auto.
    destruct Bplus; try discriminate. destruct (Bsign f1); discriminate.
    simpl in H3. unfold binary_overflow in H3. simpl in H3.
    destruct (Bsign f1) eqn:SGN1. 2:discriminate.
    assert (f1 <= 0).
    { destruct f1 as [[| | |[]] ?]; try discriminate; simpl. Psatz.lra.
      apply Fcore_float_prop.F2R_le_0_compat. discriminate. }
    assert (f2 <= 0).
    { destruct f2 as [[| | |[]] ?]; try discriminate; simpl. Psatz.lra.
      apply Fcore_float_prop.F2R_le_0_compat. compute. discriminate. }
    rewrite Rabs_left1 in H4.
    2:apply round_le_generic. 2:apply fexp_correct, eq_refl. 2:apply valid_rnd_round_mode.
    2:apply generic_format_0. 2:Psatz.lra.
    apply Ropp_le_contravar in H4. rewrite Ropp_involutive in H4.
    eapply Rle_trans. eauto. apply (Rabs_le_inv b).
    apply Rlt_le, abs_B2R_lt_emax.
Qed.

Definition half : float :=
  match Float.exact_inverse (BofZ 53 1024 eq_refl eq_refl 2) as x
        return match x with Some _ => float | None => True end
  with
  | Some x => x
  | None => I
  end.

Lemma half_half: (half:R) = 1/2.
Proof.
compute. Psatz.lra. Qed.

Opaque Bmult.

Lemma reduct_rule_2:
  ∀ x y (f1 f2:fin_float),
    (2 * x <= f1) -> (- 2 * y <= f2) ->
    let b := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2 in
    let b := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b in
    is_finite b = true ->
    (x - y <= b).
Proof.
  intros.
  assert (x-y<=(1/2)*(f1+f2)) by Psatz.lra.
  eapply Rle_trans. eauto.
  eapply Rle_trans.
  { apply Rmult_le_compat_l. Psatz.lra.
    edestruct (round_UP_pt radix2) as (A & B & C).
    apply (fexp_correct 53 1024 eq_refl). apply B. }
  eapply Rle_trans.
  { edestruct (round_UP_pt radix2) as (A & B & C).
    apply (fexp_correct 53 1024 eq_refl). apply B. }
  pose proof Bplus_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2.
  Rlt_bool_case H3.
  - destruct H3 as (? & ? & ?); auto.
    simpl round_mode in H3. rewrite <- H3. fold b. rewrite <- half_half.
    pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b.
    Rlt_bool_case H7.
    + destruct H7 as (? & ? & ?). simpl round_mode in H7. rewrite <- H7. apply Rle_refl.
    + exfalso. pose proof abs_B2R_lt_emax _ _ b.
      assert (1/2*Rabs (b) < bpow radix2 1024 * /2) by Psatz.lra.
      change (/2) with (bpow radix2 (-1)) in H10. rewrite <- bpow_plus in H10.
      rewrite <- (Rabs_right (1/2)), <- Rabs_mult, <- half_half in H10 by Psatz.lra.
      eapply Rlt_le, Rabs_le_inv in H10. destruct H10.
      eapply round_ge_generic in H10.
      2:apply (fexp_correct 53 1024 eq_refl). 2:apply (valid_rnd_round_mode mode_UP).
      2:apply generic_format_opp, generic_format_bpow; discriminate.
      eapply round_le_generic in H11.
      2:apply (fexp_correct 53 1024 eq_refl). 2:apply (valid_rnd_round_mode mode_UP).
      2:apply generic_format_bpow; discriminate.
      pose proof (Rabs_le _ _ (conj H10 H11)).
      assert (bpow radix2 1024 <= bpow radix2 (1024-1)).
      { eapply Rle_trans; eauto. }
      apply le_bpow in H13. omega.
  - destruct H3; auto.
    destruct Bplus; try discriminate. destruct (Bsign f1); discriminate.
    simpl in H3. unfold binary_overflow in H3. simpl in H3.
    destruct (Bsign f1) eqn:SGN1. 2:discriminate.
    assert (f1 <= 0).
    { destruct f1 as [[| | |[]] ?]; try discriminate; simpl. Psatz.lra.
      apply Fcore_float_prop.F2R_le_0_compat. discriminate. }
    assert (f2 <= 0).
    { destruct f2 as [[| | |[]] ?]; try discriminate; simpl. Psatz.lra.
      apply Fcore_float_prop.F2R_le_0_compat. compute. discriminate. }
    rewrite Rabs_left1 in H4.
    2:apply round_le_generic. 2:apply fexp_correct, eq_refl. 2:apply valid_rnd_round_mode.
    2:apply generic_format_0. 2:Psatz.lra.
    apply Ropp_le_contravar in H4. rewrite Ropp_involutive in H4.
    eapply Rle_trans.
    { apply round_le_generic. apply fexp_correct. reflexivity. apply (valid_rnd_round_mode mode_UP).
      apply generic_format_opp, generic_format_bpow with (e:=(-1+1024)%Z). discriminate.
      eapply Rle_trans. apply Rmult_le_compat_l. Psatz.lra. apply H4.
      compute. Psatz.lra. }
    unfold b0, b. clear b0 b H1. inv H3. Transparent Bmult. compute. Opaque Bmult. Psatz.lra.
Qed.

Definition reduce_diag (x0 x:t) : t+⊥.
refine (
  let handle_bound (f:fin_float) :=
      match Bcompare _ _ f Float.zero with
      | None => None
      | Some Lt => Some false
      | Some Eq => None
      | Some Gt => Some true
      end
  in
  let diffDiag :=
      To.shcombine_diff
        (fun k x0 x =>
           match x0, x with
           | None, None => None
           | Some _, None => None
           | None, Some x =>
             if Top.is_empty x then None
             else
               match To.get k x with
               | None => Some true
               | Some f => handle_bound f
               end
           | Some x0, Some x =>
             if Top.is_empty x then None
             else
               match To.get k x0, To.get k x with
               | None, None => None
               | Some _, None => Some true
               | None, Some f => handle_bound f
               | Some f0, Some f =>
                 if fin_float_eqdec f f0 then None
                 else handle_bound f
               end
           end)
        _ x0 x
  in
  To.fold
    (fun oct k (b:bool) =>
       if b then
         do oct <- oct;
         ret (Too.set (k, k) (exist _ Float.zero eq_refl) oct)
       else Bot)
    diffDiag (NotBot x)).
Proof.
  clear.
  abstract
    (destruct v; [|reflexivity]; destruct Top.is_empty; [reflexivity|];
     destruct To.get; [|reflexivity]; destruct fin_float_eqdec; congruence).
Defined.

Lemma reduce_diag_correct:
  ∀ x0 x ρ, ρ ∈ γ x -> ρ ∈ γ (reduce_diag x0 x).
Proof.
  intros. unfold reduce_diag.
  match goal with
  | |- ρ ∈ γ (To.fold _ ?diffDiag _) =>
    assert (HDIFF:∀ k,
               match To.get k diffDiag with
               | None => True
               | Some true => oρ ρ k <> None
               | Some false => False
               end);
    [|revert HDIFF; generalize diffDiag; intros]
  end.
  { intros. rewrite To.gshcombine_diff. pose proof (H k k). specialize (H k).
    unfold Too.get in H, H0. fold To.t.
    destruct (To.get k x). 2:destruct To.get; exact I.
    pose proof Top.is_empty_correct _ t0. destruct (Top.is_empty t0).
    destruct (To.get k x0); exact I.
    assert (oρ ρ kNone). {
      intro. destruct H1. lapply H3. discriminate.
      intros. specialize (H i). destruct (To.get i t0). 2:auto.
      edestruct H as (xv & _ & Hxv & _ & _). eauto. congruence. }
    destruct (To.get k t0). 2:destruct (To.get k x0); [destruct (To.get k t1)|]; now auto.
    edestruct H0 as (xv & yv & Hxv & Hyv & Hxyb). reflexivity. clear H H0 H1.
    rewrite Hxv in Hyv. inv Hyv. replace (yv-yv) with 0 in Hxyb by ring.
    rewrite Bcompare_correct; auto.
    apply Rcompare_not_Lt in Hxyb. change (B2R Float.zero) with 0.
    destruct To.get. 2:destruct Rcompare; try easy; congruence.
    destruct To.get. 2:destruct Rcompare; try easy; congruence.
    destruct fin_float_eqdec. now auto. destruct Rcompare; try easy; congruence. }
  rewrite To.fold_spec.
  assert (∀ k b, List.In (k, b) (To.elements t0) -> b = true /\ oρ ρ k <> None).
  { intros. apply To.elements_complete in H0. specialize (HDIFF k).
    rewrite H0 in HDIFF. destruct b; now intuition. }
  clear HDIFF.
  assert (γ (NotBot x) ρ) by auto. clear H.
  revert H1 H0. generalize (NotBot x). induction (To.elements t0). auto.
  intros. apply IHl.
  - destruct a as [k []]; destruct (H0 _ _ (or_introl eq_refl)); clear H0.
    2:discriminate.
    eapply botbind_spec; eauto.
    repeat intro. rewrite Too.gsspec in H3. destruct Too.elt_eq. inv e. inv H3.
    + destruct oρ. 2:congruence. eexists. eexists. split. eauto. split. eauto.
      simpl. change (B2R Float.zero) with 0. Psatz.lra.
    + apply H0. auto.
  - intros. apply H0. right. auto.
Qed.


Definition otop (c:query_chan): (t * messages_chan)+⊥ :=
  NotBot (Too.empty _, List.nil).

Lemma otop_correct:
  ∀ c ρ, ρ ∈ γ c -> ρ ∈ γ (otop c).
Proof.
  split. repeat intro. rewrite Too.gempty in H0. discriminate. constructor.
Qed.


Definition join0 (x y:t) : t.
refine (Too.shcombine
          (fun vab (xb yb:option fin_float) =>
             let lt (xb':fin_float) xb yb (y:t) :=
               let '(va, vb) := vab in
               let yb' : option fin_float :=
                 do bndA <- Too.get (va, ovar_opp va) y;
                 do bndB <- Too.get (ovar_opp vb, vb) y;
                 let bnd:float := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                  (bndA:fin_float) (bndB:fin_float) in
                 let bnd:float := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                        half bnd in
                 fin_float_of_float bnd
               in
               if bound_leb yb yb' then yb
               else match yb' with
                    | None => None
                    | Some yb' => if Fleb yb' xb' then xb else Some yb'
                    end
             in
             match xb, yb with
             | None, None => None
             | Some xb', None => lt xb' xb yb y
             | None, Some yb' => lt yb' yb xb x
             | Some xb', Some yb' =>
               match Bcompare _ _ xb' yb' with
               | None => None
               | Some Eq => xb
               | Some Lt => lt xb' xb yb y
               | Some Gt => lt yb' yb xb x
               end
             end)
          _ x y).
Proof.
abstract (intros; simpl; destruct v;
          [rewrite Bcompare_refl|]; auto using is_finite_not_is_nan).
Defined.

Definition join0_correct :
  ∀ x y, (γ x ∪ γ y) ⊆ γ (join0 x y).
Proof.
  intros x y ρ Hρ. unfold join0.
  intros va vb b Hb. rewrite Too.gshcombine in Hb.
  destruct (Too.get (va, vb) x) eqn:EQx, (Too.get (va, vb) y) eqn:EQy.
  - rewrite Bcompare_correct in Hb by auto.
    assert (∃ xa xb, oρ ρ va = Some xa /\ oρ ρ vb = Some xb /\
                     (γ x ρ /\ xa - xb <= f \/ γ y ρ /\ xa - xb <= f0)).
    { destruct Hρ as [Hρ|Hρ];
      edestruct Hρ as (xa & xb & Hxa & Hxb & Hxaxb); now eauto 10. }
    destruct H as (xa & xb & Hxa & Hxb & Hxaxb). clear Hρ.
    eexists. eexists. split. eauto. split. eauto.
    destruct (Rcompare_spec f f0).
    + revert Hb. destruct bound_leb. intro. inv Hb. Psatz.lra.
      destruct (Too.get (va, ovar_opp va) y) eqn:EQa, (Too.get (ovar_opp vb, vb) y) eqn:EQb;
        try discriminate.
      destruct Hxaxb as [[]|[]].
      * simpl. destruct fin_float_of_float. 2:discriminate.
        rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb. Psatz.lra.
        eapply Rle_trans. eauto. apply Rlt_le, H2.
      * apply H0 in EQa. destruct EQa as (? & ? & Hxa' & Hxa'' & Hxaa).
        rewrite <- ovar_opp_opp, Hxa in Hxa''. inv Hxa''. rewrite Hxa in Hxa'. inv Hxa'.
        apply H0 in EQb. destruct EQb as (? & ? & Hxb' & Hxb'' & Hxbb).
        rewrite <- ovar_opp_opp, Hxb in Hxb'. inv Hxb'. rewrite Hxb in Hxb''. inv Hxb''.
        simpl. destruct_fin_float_of_float. 2:discriminate. destruct FFOF.
        rewrite Fleb_Rle, <- H3 by auto.
        intro. Rle_bool_case Hb; inv Hb.
        eapply Rle_trans, H4. eapply reduct_rule_2.
        Psatz.lra. Psatz.lra. auto.
        rewrite <- H3. eapply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
    + inv Hb. Psatz.lra.
    + revert Hb. destruct bound_leb. intro. inv Hb. Psatz.lra.
      destruct (Too.get (va, ovar_opp va) x) eqn:EQa, (Too.get (ovar_opp vb, vb) x) eqn:EQb;
        try discriminate.
      destruct Hxaxb as [[]|[]].
      * apply H0 in EQa. destruct EQa as (? & ? & Hxa' & Hxa'' & Hxaa).
        rewrite <- ovar_opp_opp, Hxa in Hxa''. inv Hxa''. rewrite Hxa in Hxa'. inv Hxa'.
        apply H0 in EQb. destruct EQb as (? & ? & Hxb' & Hxb'' & Hxbb).
        rewrite <- ovar_opp_opp, Hxb in Hxb'. inv Hxb'. rewrite Hxb in Hxb''. inv Hxb''.
        simpl. destruct_fin_float_of_float. 2:discriminate. destruct FFOF.
        rewrite Fleb_Rle, <- H3 by auto. intro. Rle_bool_case Hb; inv Hb.
        eapply Rle_trans, H4. eapply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
        rewrite <- H3. eapply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
      * simpl. destruct_fin_float_of_float. 2:discriminate.
        rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb. Psatz.lra.
        eapply Rle_trans. eauto. apply Rlt_le, H2.
  - clear EQy. destruct bound_leb. discriminate. unfold snd.
    destruct (Too.get (va, ovar_opp va) y) eqn:EQa, (Too.get (ovar_opp vb, vb) y) eqn:EQb;
      try discriminate.
    destruct Hρ as [Hρ|Hρ].
    + apply Hρ in EQx. destruct EQx as (xa & xb & Hxa & Hxb & Hxaxb).
      eexists. eexists. split. eauto. split. eauto.
      destruct Too.get. 2:discriminate. destruct Too.get. 2:discriminate.
      revert Hb. simpl. destruct_fin_float_of_float. 2:discriminate.
      rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb.
      auto. eapply Rle_trans. eauto. apply Rlt_le, H.
    + apply Hρ in EQa. destruct EQa as (? & ? & Hxa & Hxa' & Hxaa).
      rewrite <- ovar_opp_opp, Hxa in Hxa'. inv Hxa'.
      apply Hρ in EQb. destruct EQb as (? & ? & Hxb & Hxb' & Hxbb).
      rewrite <- ovar_opp_opp, Hxb' in Hxb. inv Hxb.
      eexists. eexists. split. eauto. split. eauto.
      revert Hb. simpl. destruct_fin_float_of_float. 2:discriminate. destruct FFOF.
      rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb.
      eapply Rle_trans, H1. rewrite <- H0. apply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
      rewrite <- H0. apply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
  - clear EQx. destruct bound_leb. discriminate. unfold snd.
    destruct (Too.get (va, ovar_opp va) x) eqn:EQa, (Too.get (ovar_opp vb, vb) x) eqn:EQb;
      try discriminate.
    destruct Hρ as [Hρ|Hρ].
    + apply Hρ in EQa. destruct EQa as (? & ? & Hxa & Hxa' & Hxaa).
      rewrite <- ovar_opp_opp, Hxa in Hxa'. inv Hxa'.
      apply Hρ in EQb. destruct EQb as (? & ? & Hxb & Hxb' & Hxbb).
      rewrite <- ovar_opp_opp, Hxb' in Hxb. inv Hxb.
      eexists. eexists. split. eauto. split. eauto.
      revert Hb. simpl. destruct_fin_float_of_float. 2:discriminate. destruct FFOF.
      rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb.
      eapply Rle_trans, H1. rewrite <- H0. apply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
      rewrite <- H0. apply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
    + apply Hρ in EQy. destruct EQy as (xa & xb & Hxa & Hxb & Hxaxb).
      eexists. eexists. split. eauto. split. eauto.
      destruct Too.get. 2:discriminate. destruct Too.get. 2:discriminate.
      revert Hb. simpl. destruct_fin_float_of_float. 2:discriminate.
      rewrite Fleb_Rle by auto. intro. Rle_bool_case Hb; inv Hb.
      auto. eapply Rle_trans. eauto. apply Rlt_le, H.
  - discriminate.
Qed.

Definition get_join_diffs (x y:t) : list (ovar * fin_float * fin_float) *
                                    list (ovar * fin_float * fin_float).
refine(
    let m := To.shcombine_diff (fun v x' y' =>
      do x' <- x'; do x' <- To.get (ovar_opp v) x';
      do y' <- y'; do y' <- To.get (ovar_opp v) y';
      match Bcompare _ _ (x':fin_float) (y':fin_float) with
      | Some Lt => ret (true, x', y')
      | Some Gt => ret (false, x', y')
      | _ => None
      end) _ x y
    in
    To.fold (fun l v t =>
       let '(lt, gt) := l in
       let '(cmp, x', y') := t in
       if cmp:bool then ((v, x', y')::lt, gt) else (lt, (v, x', y')::gt))
      m (nil, nil)).
Proof.
  abstract (intros; destruct v; simpl;
            [destruct To.get; simpl;
             [rewrite Bcompare_refl|]|]; auto using is_finite_not_is_nan).
Defined.

Lemma get_join_diffs_correct:
  ∀ x y llt lgt v bndx bndy,
    get_join_diffs x y = (llt, lgt) ->
    In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
  ∀ ρ,
    (ρ ∈ γ x -> ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) /\
    (ρ ∈ γ y -> ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndy).
Proof.
  unfold get_join_diffs. intros.
  rewrite To.fold_spec, <- fold_left_rev_right in H.
  match type of H with
  | context [To.elements ?X] =>
    generalize (To.elements_complete X);
    revert H; setoid_rewrite To.gshcombine_diff; setoid_rewrite in_rev;
    revert llt lgt H0;
    induction (rev (To.elements X)) as [|[v' [[[] x']y']]]; simpl; intros
  end.
  - inv H. destruct H0 as [[]|[]].
  - destruct (fold_right (A:=_*_)). inv H. specialize (fun H => IHl _ _ H eq_refl).
    destruct H0 as [[]|]; auto. clear IHl. inv H. specialize (H1 _ _ (or_introl eq_refl)).
    revert H1.
    destruct (To.get v x) eqn:EQx; try discriminate. simpl.
    destruct (To.get (ovar_opp v) t0) eqn:EQx'; try discriminate. simpl.
    destruct (To.get v y) eqn:EQy; try discriminate. simpl.
    destruct (To.get (ovar_opp v) t1) eqn:EQy'; try discriminate. simpl.
    destruct Bcompare; try discriminate. intro. destruct c; inv H1.
    split; intro H; specialize (H v (ovar_opp v)); unfold Too.get in H.
    + rewrite EQx, EQx' in H. edestruct H as (xv & xv' & Hxv & Hxv' & Hxxv). eauto.
      apply ovar_opp_opp in Hxv'. rewrite Hxv in Hxv'. inv Hxv'.
      eexists. split. eauto. Psatz.lra.
    + rewrite EQy, EQy' in H. edestruct H as (xv & xv' & Hxv & Hxv' & Hxxv). eauto.
      apply ovar_opp_opp in Hxv'. rewrite Hxv in Hxv'. inv Hxv'.
      eexists. split. eauto. Psatz.lra.
  - destruct (fold_right (A:=_*_)). inv H. specialize (fun H => IHl _ _ H eq_refl).
    destruct H0 as [|[]]; auto. clear IHl. inv H. specialize (H1 _ _ (or_introl eq_refl)).
    revert H1.
    destruct (To.get v x) eqn:EQx; try discriminate. simpl.
    destruct (To.get (ovar_opp v) t0) eqn:EQx'; try discriminate. simpl.
    destruct (To.get v y) eqn:EQy; try discriminate. simpl.
    destruct (To.get (ovar_opp v) t1) eqn:EQy'; try discriminate. simpl.
    destruct Bcompare; try discriminate. intro. destruct c; inv H1.
    split; intro H; specialize (H v (ovar_opp v)); unfold Too.get in H.
    + rewrite EQx, EQx' in H. edestruct H as (xv & xv' & Hxv & Hxv' & Hxxv). eauto.
      apply ovar_opp_opp in Hxv'. rewrite Hxv in Hxv'. inv Hxv'.
      eexists. split. eauto. Psatz.lra.
    + rewrite EQy, EQy' in H. edestruct H as (xv & xv' & Hxv & Hxv' & Hxxv). eauto.
      apply ovar_opp_opp in Hxv'. rewrite Hxv in Hxv'. inv Hxv'.
      eexists. split. eauto. Psatz.lra.
Qed.

Definition finish_join (r:t)
           (l:list (ovar * fin_float * fin_float) * list (ovar * fin_float * fin_float)) : t :=
  let '(llt, lgt) := l in
  List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
    let '(a, bndxa, bndya) := x in
    List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
      let '(b, bndxb, bndyb) := x in
      let bndx := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndxa bndxb in
      let bndx := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndx in
      let bndx := fin_float_of_float bndx in
      let bndy := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndya bndyb in
      let bndy := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndy in
      let bndy := fin_float_of_float bndy in
      let bnd := if bound_leb bndx bndy then bndy else bndx in
      let '(bnd0, setter) := Too.get_set (a, ovar_opp b) r in
      if bound_leb bnd0 bnd then r
      else match bnd with
           | None => r
           | Some bnd =>
             let r := setter bnd in
             Too.set (b, ovar_opp a) bnd r
           end)
     llt r)
    lgt r.

Lemma finish_join_correct:
  ∀ lgt llt r ρ,
  ((∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
      ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) \/
   (∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
      ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndy)) ->
  ρ ∈ γ r ->
  ρ ∈ γ (finish_join r (llt, lgt)).
Proof.
  Opaque Too.get_set Too.set Too.get.
  unfold finish_join.
  induction lgt as [|[[a bndxa]bndya]]; simpl fold_left. auto.
  intros. apply IHlgt.
  { destruct H.
    - left. intros. apply H with (bndy:=bndy). simpl. tauto.
    - right. intros. apply H with (bndx:=bndx). simpl. tauto. }
  clear IHlgt. revert r ρ H H0.
  induction llt as [|[[b bndxb]bndyb]]; simpl fold_left. auto.
  intros. apply IHllt.
  { destruct H.
    - left. intros. apply H with (bndy:=bndy). simpl. tauto.
    - right. intros. apply H with (bndx:=bndx). simpl. tauto. }
  destruct (Too.get_set_spec (a, ovar_opp b) r).
  destruct Too.get_set as [? setter]. simpl in H1. subst.
  destruct bound_leb. now auto.
  repeat (destruct_fin_float_of_float; try destruct FFOF); auto; destruct f; auto.
  destruct f0. simpl. rewrite Fleb_Rle by auto.
  simpl in H, H3, H5. subst. clear IHllt. repeat intro. destruct H.
  - edestruct H as (av & Hav & Haav). right. auto.
    edestruct H as (bv & Hbv & Hbbv). left. auto.
    apply reduct_rule_2 with (x:=av) (y:=(-bv)) in H1.
    2:now auto. 2:now Psatz.lra.
    Rle_bool_case H3; rewrite H2, !Too.gsspec in H3;
    (destruct Too.elt_eq; [|destruct Too.elt_eq]).
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto.
      eapply Rle_trans, H5. eapply Rle_trans, H1. Psatz.lra.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto.
      eapply Rle_trans, H5. auto.
    + apply H0, H3.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto.
      eapply Rle_trans, H1. Psatz.lra.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto. auto.
    + apply H0, H3.
  - edestruct H as (av & Hav & Haav). right. auto.
    edestruct H as (bv & Hbv & Hbbv). left. auto.
    apply reduct_rule_2 with (x:=av) (y:=(-bv)) in H4.
    2:now auto. 2:now Psatz.lra.
    Rle_bool_case H3; rewrite H2, !Too.gsspec in H3;
    (destruct Too.elt_eq; [|destruct Too.elt_eq]).
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto.
      eapply Rle_trans, H4. Psatz.lra.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto. auto.
    + apply H0, H3.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto. simpl.
      eapply Rle_trans, Rlt_le, H5. eapply Rle_trans, H4. Psatz.lra.
    + inv H3. inv e1. eexists. eexists. split. eauto. split.
      apply -> ovar_opp_opp. rewrite Ropp_involutive. eauto.
      eapply Rle_trans, Rlt_le, H5. auto.
    + apply H0, H3.
      Transparent Too.get_set Too.set Too.get.
Qed.

Definition ojoin (x:t * query_chan) (y:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥ :=
  let r := join0 (fst x) (fst y) in
  let l := get_join_diffs (fst x) (fst y) in
  let r := finish_join r l in
  NotBot (r, List.nil).

Lemma ojoin_correct :
  forall x y c ρ,
    ρ ∈ γ x \/ ρ ∈ γ y -> ρ ∈ γ c ->
    ρ ∈ γ (ojoin x y c).
Proof.
  split. 2:constructor. simpl.
  pose proof get_join_diffs_correct (fst x) (fst y). destruct get_join_diffs.
  apply finish_join_correct, join0_correct. 2:destruct H as [[]|[]]; now auto.
  destruct H.
  - left. intros. specialize (H1 _ _ _ _ _ eq_refl H2 ρ). apply H1, H.
  - right. intros. specialize (H1 _ _ _ _ _ eq_refl H2 ρ). apply H1, H.
Qed.


Definition oinit_iter (m:t+⊥) : iter_t :=
  do m <- m;
  let m :=
    Toop.filter (fun xy (b:fin_float) =>
                   let '(x, y) := xy in
                   if eq_dec x (ovar_opp y) then true
                   else
                     match Too.get (x, ovar_opp x) m, Too.get (ovar_opp y, y) m with
                     | None, _ | _, None => true
                     | Some f1, Some f2 =>
                       let b' := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                       (f1:fin_float) (f2:fin_float) in
                       let b' := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b' in
                       negb (Fleb b' b)
                     end
                ) m
  in
  NotBot (m, Too.empty _).

Lemma oinit_iter_sound:
  ∀ m, γ m ⊆ γ (oinit_iter m).
Proof.
  intros. eapply botbind_spec, H.
  intros. repeat intro. unfold fst in H1. rewrite Toop.gfilter in H1.
  destruct (Too.get (x, y) a0) eqn:EQxy. 2:discriminate. destruct @eq_dec.
  - inv H1. apply H0. auto.
  - destruct (Too.get (x, ovar_opp x) a0), (Too.get (ovar_opp y, y) a0).
    destruct @Fleb in H1. discriminate.
    inv H1. apply H0. auto. inv H1. apply H0. auto.
    inv H1. apply H0. auto. inv H1. apply H0. auto.
Qed.

Definition widen0 (it:t*Too.t unit) (m:t) : t.
refine (Too.shcombine
          (fun vab (itb mb:option fin_float) =>
             let '(va, vb) := vab in
             match itb, mb with
             | None, None => None
             | None, Some mb =>
               match Too.get vab (snd it) with
               | Some _ => None
               | None =>
                 match Too.get (va, ovar_opp va) (fst it), Too.get (ovar_opp vb, vb) (fst it) with
                 | None, _ | _, None => None
                 | Some bndA, Some bndB =>
                   let bnd := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndA bndB in
                   let bnd := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bnd in
                   if Fleb mb bnd then
                     if bound_leb (Too.get (va, ovar_opp va) m) (Some bndA) &&
                        bound_leb (Too.get (ovar_opp vb, vb) m) (Some bndB) then
                       None
                     else fin_float_of_float bnd
                   else None
                 end
               end
             | Some _, _ =>
               if bound_leb mb itb then itb
               else
                 do bndA <- Too.get (va, ovar_opp va) m;
                 do bndB <- Too.get (ovar_opp vb, vb) m;
                 let bnd := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                  (bndA:fin_float) (bndB:fin_float) in
                 let bnd := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bnd in
                 let b := fin_float_of_float bnd in
                 if bound_leb b itb then itb else None
             end)
          _ (fst it) m).
Proof.
  abstract
    (intros; destruct x as [va vb], v as [[]|]; auto;
     unfold bound_leb; rewrite Fleb_refl; auto using is_finite_not_is_nan).
Defined.

Lemma widen0_incr:
  ∀ it m, γ it ⊆ γ (widen0 it m).
Proof.
  intros. unfold widen0. repeat intro. rewrite Too.gshcombine in H0.
  destruct (Too.get (x, y) (fst it)) eqn:EQit.
  - apply H. rewrite EQit.
    destruct bound_leb. now auto.
    destruct (Too.get (x, ovar_opp x)). 2:discriminate.
    destruct (Too.get (ovar_opp y, y)). 2:discriminate.
    unfold bind, option_monad in H0. destruct bound_leb. now auto. discriminate.
  - destruct (Too.get (x, y) m) eqn:EQm. 2:discriminate.
    destruct (Too.get (x, y) (snd it)). discriminate.
    destruct (Too.get (x, ovar_opp x) (fst it)) eqn:EQitx. 2:discriminate.
    destruct (Too.get (ovar_opp y, y) (fst it)) eqn:EQity. 2:discriminate.
    destruct @Fleb. 2:discriminate. destruct andb. discriminate.
    destruct (H _ _ _ EQitx) as (vx & vx' & Hvx & Hvx' & Hvxvx').
    rewrite <- ovar_opp_opp, Hvx in Hvx'. inv Hvx'.
    destruct (H _ _ _ EQity) as (vy' & vy & Hvy' & Hvy & Hvyvy').
    rewrite <- ovar_opp_opp, Hvy in Hvy'. inv Hvy'.
    eexists. eexists. split. eauto. split. eauto.
    revert H0. destruct_fin_float_of_float. 2:discriminate. intro EQ. inv EQ.
    destruct FFOF as [? <-]. eapply reduct_rule_2. Psatz.lra. Psatz.lra. auto.
Qed.

Definition record_widen_diffs (it:t*Too.t unit) (itnew:t) : Too.t unit.
refine(let diffs :=
           Too.shcombine_diff
             (fun v old new =>
                match old, new with
                | Some _, None => Some tt
                | _, _ => None
                end)
             _ (fst it) itnew
       in
       Too.fold (fun w v _ => Too.set v tt w) diffs (snd it)).
Proof.
abstract (destruct v; auto). Defined.

Definition finish_widen
           (r:t)
           (l:list (ovar * fin_float * fin_float) *
              list (ovar * fin_float * fin_float))
           (w:Too.t unit) : t :=
  let '(llt, lgt) := l in
  List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
    let '(a, bndita, bndma) := x in
    List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
      let '(b, bnditb, bndmb) := x in
      match Too.get (a, ovar_opp b) w with
      | Some _ => r
      | None =>
        match Too.get_set (a, ovar_opp b) r with
        | (Some _, _) => r
        | (None, setter) =>
          let bndit := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndita bnditb in
          let bndit := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndit in
          let bndit := fin_float_of_float bndit in
          let bndm := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndma bndmb in
          let bndm := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndm in
          let bndm := fin_float_of_float bndm in
          if bound_leb bndm bndit then
            match bndit with
            | Some bndit =>
              let r := setter bndit in
              Too.set (b, ovar_opp a) bndit r
            | None => r
            end
          else r
        end
      end)
     llt r)
  lgt r.

Lemma finish_widen_correct:
  ∀ lgt llt r w ρ,
  (∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
   ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) ->
  ρ ∈ γ r ->
  ρ ∈ γ (finish_widen r (llt, lgt) w).
Proof.
  Opaque Too.get_set Too.set Too.get.
  unfold finish_widen.
  induction lgt as [|[[a bndxa]bndya]]; simpl fold_left. auto.
  intros. apply IHlgt.
  { intros. eapply H. destruct H1. eauto. simpl. eauto. }
  clear IHlgt. revert r ρ H H0.
  induction llt as [|[[b bndxb]bndyb]]; simpl fold_left. auto.
  intros. apply IHllt.
  { intros. eapply H. destruct H1; simpl; eauto. }
  destruct (Too.get (a, ovar_opp b) w). auto.
  destruct (Too.get_set_spec (a, ovar_opp b) r).
  destruct Too.get_set as [? setter]. simpl in H1. subst. destruct Too.get. now auto.
  destruct bound_leb. 2:now auto.
  destruct_fin_float_of_float. 2:now auto.
  destruct FFOF; eauto. rewrite H2. clear H2. repeat intro.
  simpl in H, H3. subst.
  edestruct H as (av & Hav & Haav). right. auto.
  edestruct H as (bv & Hbv & Hbbv). left. auto.
  rewrite !Too.gsspec in H2. destruct Too.elt_eq; [|destruct Too.elt_eq].
  - inv H2. inv e. rewrite <- H3.
    eexists. eexists. split. eauto. split. rewrite <- ovar_opp_opp, Hav, Ropp_involutive. eauto.
    eapply Rle_trans, reduct_rule_2; eauto. 2:rewrite Rmult_opp_opp; eauto. Psatz.lra.
  - inv H2. inv e. rewrite <- H3.
    eexists. eexists. split. eauto. split. rewrite <- ovar_opp_opp, Hbv, Ropp_involutive. eauto.
    apply reduct_rule_2; auto. Psatz.lra.
  - apply H0. auto.
  Transparent Too.get_set Too.set Too.get.
Qed.

Definition widen_reduce_1 (y0 y:t) : t :=
  (To.fold
     (fun (y:t) c _ =>
        match To.get (ovar_opp c) y, To.get c y with
        | None, _ | _, None => y
        | Some aa, Some bb =>
          Toop.map_changed fin_float_eqdec
             (fun ab yb =>
                let '(a, b) := ab in
                let bound :=
                  do f1 <- To.get (ovar_opp a) aa;
                  do f2 <- To.get b bb;
                  fin_float_of_float (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                            (f1:fin_float) (f2:fin_float))
                in
                bound_min yb bound)
             y0 y
        end
     ) y y).

Lemma widen_reduce_1_correct:
  ∀ y0 y ρ, ρ ∈ γ y -> ρ ∈ γ (widen_reduce_1 y0 y).
Proof.
  intros y0 y ρ. unfold widen_reduce_1. rewrite To.fold_spec.
  generalize y at 1 3. induction (To.elements y) as [|[c ?]]. now auto.
  intros. apply IHl. unfold fst at 1 2.
  destruct (To.get (ovar_opp c) y1) as [aa|] eqn:EQaa. 2:now auto.
  destruct (To.get c y1) as [bb|] eqn:EQbb. 2:now auto.
  intros a b bd Hbd.
  edestruct Toop.map_changed_correct as [[]|[]];
    (eapply eq_trans in Hbd; [|symmetry; apply H1]).
  eapply H; now eauto.
  revert bd Hbd. eapply bound_min_either. now apply H.
  destruct (To.get (ovar_opp a) aa) as [aa'|] eqn:EQaa'. 2:discriminate.
  destruct (To.get b bb) as [bb'|] eqn:EQbb'. 2:discriminate.
  intros. simpl in Hbd. apply fin_float_of_float_correct in Hbd. destruct Hbd.
  assert (Too.get (ovar_opp c, ovar_opp a) y1 = Some aa').
  { unfold Too.get. rewrite EQaa, EQaa'; auto. }
  eapply H in H4; eauto using ovar_opp_opp.
  destruct H4 as (xc & xa & Hxc & Hxa & Baa'). rewrite <- ovar_opp_opp in Hxc, Hxa.
  assert (Too.get (c, b) y1 = Some bb').
  { unfold Too.get. rewrite EQbb, EQbb'; auto. }
  eapply H in H4; eauto using ovar_opp_opp.
  destruct H4 as (xc' & xb & Hxc' & Hxb & Bbb').
  eexists. eexists. split. eauto. split. eauto. rewrite <- H3.
  apply reduct_rule_1 with (y:=xc'). rewrite Hxc in Hxc'. inv Hxc'. Psatz.lra. Psatz.lra. auto.
Qed.

Definition owiden (it:iter_t) (y:(t * query_chan)+⊥) (c:query_chan+⊥) :
  iter_t * ((t * messages_chan) +⊥) :=
  match it, y with
  | Bot, Bot => (oinit_iter Bot, Bot)
  | Bot, NotBot (y, _) => (oinit_iter (NotBot y), NotBot (y, nil))
  | NotBot it, Bot =>
    let w := widen_reduce_1 (Too.empty _) (fst it) in
    (NotBot it, do w <- reduce_diag (Too.empty _) w; ret (w, List.nil))
  | NotBot it, NotBot (y, _) =>
    let r := widen0 it y in
    let w := record_widen_diffs it r in
    let l := get_join_diffs (fst it) y in
    let r := finish_widen r l w in
    (NotBot (r,w),
     let r := widen_reduce_1 y r in
     do r <- reduce_diag y r; ret (r, nil))
  end.

Lemma owiden_incr:
  forall x y c ρ,
    ρ ∈ γ x -> ρ ∈ γ c ->
    ρ ∈ γ (owiden x y c).
Proof.
  unfold owiden. intros. destruct x, y as [|[]]; try contradiction.
  - split. auto. eapply botbind_spec, reduce_diag_correct, widen_reduce_1_correct, H.
    split. auto. constructor.
  - pose proof get_join_diffs_correct (fst x) t0. destruct get_join_diffs.
    split.
    + apply finish_widen_correct, widen0_incr, H.
      intros. apply H1 with (ρ:=ρ) in H2. 2:auto. clear H1. destruct H2. auto.
    + eapply botbind_spec, reduce_diag_correct, widen_reduce_1_correct,
             finish_widen_correct, widen0_incr, H.
      split. auto. constructor.
      intros. apply H1 with (ρ:=ρ) in H2. 2:auto. clear H1. destruct H2. auto.
Qed.


Definition oleb (x:t * query_chan) (y:t) : bool.
refine (
  let x := fst x in
  Too.shforall2 (fun k (xff yff:option fin_float) =>
    match yff with
    | None => true
    | Some fy =>
      match xff with
      | None => false
      | Some fx => Fleb fx fy
      end ||
      let x' : option fin_float :=
        let '(A, B) := k in
        do bndA <- Too.get (A, ovar_opp A) x;
        do bndB <- Too.get (ovar_opp B, B) x;
        let b : float := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                               (bndA:fin_float) (bndB:fin_float) in
        let b : float := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                               half b in
        fin_float_of_float b
      in
      match x' with
      | None => false
      | Some fx' => Fleb fx' fy
      end
    end)
    _ x y).
Proof.
  clear.
  abstract (
      destruct v; [rewrite Fleb_refl; destruct f as [[] ?];
                   try discriminate; reflexivity
                  |reflexivity]).
Defined.

Lemma oleb_correct:
  forall x y ρ,
    oleb x y = true ->
    ρ ∈ γ x ->
    ρ ∈ γ y.
Proof.
  repeat intro.
  unfold oleb in H. eapply Too.shforall2_correct with (x:=(x0, y0)) in H.
  rewrite H1 in H. destruct H0. apply Bool.orb_true_iff in H. destruct H.
  - specialize (H0 x0 y0).
    destruct Too.get. 2:discriminate.
    edestruct H0 as (xb & yb & Hxb & Hyb & Hxyb). eauto.
    exists xb, yb. split. auto. split. auto.
    eapply Rle_trans. eauto. rewrite Fleb_Rle in H by auto.
    Rle_bool_case H. auto. discriminate.
  - destruct (Too.get (x0, ovar_opp x0) (fst x)) eqn:EQx. 2:discriminate.
    destruct (Too.get (ovar_opp y0, y0) (fst x)) eqn:EQy. 2:discriminate.
    apply H0 in EQx. destruct EQx as (xv & mxv & Hxv & Hmxv & Hxmxb).
    apply H0 in EQy. destruct EQy as (myv & yv & Hmyv & Hyv & Hmyyb).
    eexists. eexists. split. eauto. split. eauto.
    revert H. simpl. destruct_fin_float_of_float. 2:discriminate.
    rewrite Fleb_Rle by auto. intro.
    Rle_bool_case H. 2:discriminate. eapply Rle_trans, H3. clear H3 b H1 H y.
    edestruct FFOF as [? <-]. apply reduct_rule_2, H.
    rewrite <- ovar_opp_opp, Hxv in Hmxv. inv Hmxv. Psatz.lra.
    rewrite <- ovar_opp_opp, Hyv in Hmyv. inv Hmyv. Psatz.lra.
Qed.


Definition oforget0 (x:var) (ab:t) : t :=
  let ab := To.remove (ovPlus x) ab in
  let ab := To.remove (ovMinus x) ab in
  To.map1
    (fun ab =>
       let ab := To.remove (ovPlus x) ab in
       To.remove (ovMinus x) ab)
    ab.

Lemma oforget0_incl:
  ∀ x ab, γ ab ⊆ γ (oforget0 x ab).
Proof.
  repeat intro. unfold oforget0, Too.get in H0.
  rewrite To.gmap1, !To.grspec in H0.
  destruct To.elt_eq. discriminate.
  destruct To.elt_eq. discriminate.
  destruct (To.get x0 ab) eqn:EQ. 2:discriminate.
  simpl in H0. rewrite !To.grspec in H0.
  destruct To.elt_eq. discriminate.
  destruct To.elt_eq. discriminate.
  apply H. simpl. rewrite EQ. auto.
Qed.

Lemma oforget0_forget:
  ∀ x ab ρ n,
    ρ ∈ γ (oforget0 x ab) ->
    ρ+[x => n] ∈ γ (oforget0 x ab).
Proof.
  repeat intro. specialize (H _ _ _ H0).
  destruct H as (xb & yb & Hxb & Hyb & Hxyb).
  exists xb, yb. split. 2:split. 3:now auto.
  - unfold oρ, rρ.
    destruct x0; simpl; rewrite upd_o; auto; unfold oforget0, Too.get in H0; intro; subst;
    rewrite To.gmap1 in H0; [rewrite To.gro in H0 by discriminate|]; rewrite To.grs in H0;
    discriminate.
  - unfold oρ, rρ.
    destruct y; simpl; rewrite upd_o; auto; unfold oforget0, Too.get in H0; intro; subst;
    rewrite To.gmap1 in H0; destruct To.get; try discriminate; simpl in H0;
    [rewrite To.gro in H0 by discriminate|]; rewrite To.grs in H0; discriminate.
Qed.

Definition oforget (x:var) (ab:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥ :=
  NotBot (oforget0 x (fst ab), List.nil).

Lemma oforget_correct:
  forall x ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    (ρ+[x => n]) ∈ γ (oforget x ab chan).
Proof.
  intros. split. 2:constructor. apply oforget0_forget, oforget0_incl, H.
Qed.


Definition add_zerocycle (x:ovar) (ab:t) : t :=
  match Too.get_set (x, x) ab with
  | (None, setter) => setter (exist _ Float.zero eq_refl)
  | (Some v, setter) =>
    if Fleb Float.zero v then setter (exist _ Float.zero eq_refl)
    else ab
  end.

Lemma add_zerocycle_correct:
  ∀ x ab ρ xv,
    ρ ∈ γ ab ->
    oρ ρ x = Some xv ->
    ρ ∈ γ (add_zerocycle x ab).
Proof.
  repeat intro. unfold add_zerocycle in H1.
  destruct (Too.get_set_spec (x, x) ab). destruct Too.get_set.
  unfold fst, snd in H2, H3. subst o. rewrite H3 in H1. clear H3.
  destruct (Too.get (x, x) ab); [destruct @Fleb|]; rewrite ?Too.gsspec in H1;
  try (destruct Too.elt_eq; [inv e|]); inv H1; auto; simpl; change (B2R Float.zero) with 0.
  - eexists. eexists. split. eauto. split. eauto. Psatz.lra.
  - eexists. eexists. split. eauto. split. eauto. Psatz.lra.
Qed.

Definition constraint_row := To.t fin_float.

Instance cr_tostring {_:ToString var} : ToString constraint_row :=
  fun x =>
    (To.fold (fun acc y (b:fin_float) =>
       acc ++ "[_" ++ to_string (ovar_opp y) ++ "<=" ++ to_string (b:float) ++"]")
       x "{" ++ "}")%string.

Definition constraints_row_valid (row:constraint_row) (ρ:var -> ideal_num) : ℘ R :=
  fun v =>
  ∀ x b, To.get x row = Some b ->
  ∃ xv, oρ ρ x = Some xv /\ (v-xv <= b).

Definition trim_constraints_row (a:ovar) (row:constraint_row) (ab:t) : constraint_row :=
  let mapa :=
      match To.get a ab with
      | None => To.empty _
      | Some mapa => mapa
      end
  in
  To.combine (fun old new => if bound_leb old new then None else new)
    mapa row.

Lemma trim_constraints_row_correct:
  ∀ a row ab ρ av,
    ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    constraints_row_valid (trim_constraints_row a row ab) ρ av.
Proof.
  unfold constraints_row_valid, trim_constraints_row. intros.
  rewrite To.gcombine in H1 by auto. revert H1.
  destruct bound_leb; simpl. discriminate. auto.
Qed.

Definition reduce_constraints_row_step (row:constraint_row) (x:ovar) (ax:fin_float) (ab:t):
  constraint_row :=
  match To.get x ab with
  | None => row
  | Some mapx =>
    To.combine
      (fun (ay xy:option fin_float) =>
         let ay' :=
             match xy with
             | None => None
             | Some xy =>
               fin_float_of_float (
                   Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ax xy)
             end
         in
         bound_min ay ay')
      row mapx
  end.

Lemma reduce_constraints_row_step_correct:
  ∀ row x (ax:fin_float) ab ρ v,
    ρ ∈ γ ab ->
    (∀ xv, oρ ρ x = Some xv -> (v - xv <= ax)) ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row_step row x ax ab) ρ v.
Proof.
  unfold constraints_row_valid, reduce_constraints_row_step.
  intros. specialize (H x x0). unfold Too.get in H.
  destruct (To.get x ab). 2:now auto.
  rewrite To.gcombine in H2 by auto. revert H2. apply bound_min_either.
  - intros. edestruct H1 as (xv0 & Hxv0 & Hxv0'). eauto. eauto.
  - intros. destruct To.get. 2:discriminate. edestruct H as (? & ? & ? & ? & ?). now eauto.
    apply fin_float_of_float_correct in H2. destruct H2 as (? & <-).
    eauto using reduct_rule_1.
Qed.

Definition reduce_constraints_row_final (row:constraint_row) (a:ovar) (ab:t):
  constraint_row:=
  let best_aa' :=
    T.fold (fun bnd z (azaz':option fin_float * option fin_float) =>
              match azaz' with
              | (Some az, Some az') =>
                bound_min bnd (
                  fin_float_of_float (
                      Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP az az'))
              | _ => bnd
              end)
    row (To.get (ovar_opp a) row)
  in
  match best_aa' with
  | None => row
  | Some best_aa' =>
    let row := To.set (ovar_opp a) best_aa' row in
    reduce_constraints_row_step row (ovar_opp a) best_aa' ab
  end.

Lemma reduce_constraints_row_final_correct:
  ∀ row a ab ρ av,
    ρ ∈ γ ab ->
    oρ ρ a = Some av ->
    constraints_row_valid row ρ av ->
    constraints_row_valid (reduce_constraints_row_final row a ab) ρ av.
Proof.
  unfold constraints_row_valid, reduce_constraints_row_final. intros.
  match type of H2 with
  | To.get x match ?BESTAA' with _ => _ end = _ =>
    assert (∀ best_aa', BESTAA' = Some best_aa' -> av+av <= best_aa');
      [|destruct BESTAA']
  end.
  { clear H2. rewrite T.fold_spec with (A:=SUU.t fin_float).
    pose proof T.elements_complete row.
    revert H2. pose proof (H1 (ovar_opp a)). revert H2.
    generalize (To.get (ovar_opp a) row).
    induction (T.elements row) as [|[?[]] ?]; simpl; intros.
    - subst. destruct (H2 _ eq_refl) as (? & ? & ?).
      apply ovar_opp_opp in H4. rewrite H0 in H4. inv H4. Psatz.lra.
    - eapply IHl, H4. 2:now eauto.
      intros. destruct t0, t1; try now (subst; eauto).
      revert H5. apply bound_min_either; simpl; intro. now (subst; eauto).
      apply fin_float_of_float_correct in H5. destruct H5 as (? & <-).
      specialize (H3 _ _ (or_introl eq_refl)).
      pose proof (H1 (ovMinus e)). specialize (H1 (ovPlus e)).
      unfold To.get in H1, H6. simpl in H1, H6.
      rewrite H3 in H1, H6. edestruct H1 as (? & ? & ?), H6 as (? & ? & ?); try reflexivity.
      rewrite H7 in H9. inv H9.
      eexists. split. apply -> ovar_opp_opp. rewrite Ropp_involutive. now eauto.
      eapply reduct_rule_1; eauto. Psatz.lra. }
  2:now auto.
  specialize (H3 _ eq_refl).
  eapply reduce_constraints_row_step_correct. now eauto. 3:now eauto.
  - intros. rewrite <- ovar_opp_opp, H0 in H4. inv H4. now auto.
  - repeat intro. rewrite To.gsspec in H4. destruct To.elt_eq. 2:now auto.
    inv H4. eexists. rewrite <- ovar_opp_opp, H0, Ropp_involutive. split. eauto. Psatz.lra.
Qed.

Definition reduce_constraints_row (row:constraint_row) (a:ovar) (ab:t) : constraint_row :=
  let row :=
    To.fold (fun (acc:constraint_row) (x:ovar) (ax:fin_float) =>
               reduce_constraints_row_step acc x ax ab)
      row row
  in
  reduce_constraints_row_final row a ab.

Lemma reduce_constraints_row_correct:
  ∀ row a ab ρ v,
    ρ ∈ γ ab ->
    oρ ρ a = Some v ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row row a ab) ρ v.
Proof.
  intros. apply reduce_constraints_row_final_correct; auto.
  rewrite To.fold_spec.
  generalize H1. generalize row at 1 3.
  specialize (fun i v H => H1 _ _ (To.elements_complete _ i v H)).
  induction To.elements as [|[x ax]]. now auto.
  intros. eapply IHl. intros. apply H1. right. now auto.
  edestruct H1 as (? & ? & ?). left. reflexivity.
  eapply reduce_constraints_row_step_correct; eauto.
  simpl. intros. assert (xv=x0) by congruence. subst. now auto.
Qed.

Definition add_constraints_row_noreduce (a:ovar) (row:constraint_row) (ab:t) : t :=
  let ab := add_zerocycle a ab in
  let ab := add_zerocycle (ovar_opp a) ab in
  match To.get (ovar_opp a) ab with
  | None => ab
  | Some map_ya =>
    let ab :=
      To.fold (fun acc yopp (ya:fin_float) =>
        match To.get_set (ovar_opp yopp) acc with
        | (None, _) => acc
        | (Some map_yx, setter_yx) =>
          let '(map_yx, chgt) :=
            To.fold (fun (acc':To.t fin_float * bool) x (ax:fin_float) =>
              let '(map_yx, chgt) := acc' in
              let new :=
                fin_float_of_float (
                  Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ya ax)
              in
              let (old, setter) := To.get_set x map_yx in
              if bound_leb old new then acc'
              else match new with
                   | None => acc'
                   | Some new => (setter new, true)
                   end) row (map_yx, false)
          in
          if chgt then (setter_yx map_yx) else acc
        end) map_ya ab
    in
    match To.get (ovar_opp a) ab with
    | None => ab
    | Some map_ya =>
      To.fold (fun acc x (ax:fin_float) =>
        match To.get_set (ovar_opp x) acc with
        | (None, _) => acc
        | (Some map_xoppyopp, setter_xoppyopp) =>
          let '(map_xoppyopp, chgt) :=
            To.fold (fun (acc':To.t fin_float * bool) yopp (ya:fin_float) =>
              let '(map_xoppyopp, chgt) := acc' in
              let new :=
                fin_float_of_float (
                  Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ya ax)
              in
              let (old, setter) := To.get_set yopp map_xoppyopp in
              if bound_leb old new then acc'
              else match new with
                   | None => acc'
                   | Some new => (setter new, true)
                   end) map_ya (map_xoppyopp, false)
          in
          if chgt then (setter_xoppyopp map_xoppyopp) else acc
        end) row ab
    end
  end.

Lemma add_constraints_row_noreduce_correct:
  ∀ a row ab ρ av,
    oρ ρ a = Some av -> ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    ρ ∈ γ (add_constraints_row_noreduce a row ab).
Proof.
  intros.
  unfold constraints_row_valid in H1. unfold add_constraints_row_noreduce.
  eapply add_zerocycle_correct in H0. 2:now eauto.
  eapply add_zerocycle_correct in H0.
  2:apply -> ovar_opp_opp; etransitivity; [apply H|]. 2:f_equal; symmetry; apply Ropp_involutive.
  revert H0 H1. generalize (add_zerocycle (ovar_opp a) (add_zerocycle a ab)) as ab'. clear ab. intros.
  destruct (To.get (ovar_opp a) ab') as [map_ya|] eqn:EQmap_ya. 2:now auto.
  assert (∀ yopp ya, List.In (yopp, ya) (To.elements map_ya) ->
          ∃ yv, oρ ρ yopp = Some yv ∧ (- yv - av <= ya)).
  { intros. specialize (H0 (ovar_opp a)). unfold Too.get in H0.
    rewrite EQmap_ya in H0. specialize (H0 _ _ (To.elements_complete _ _ _ H2)).
    destruct H0 as (? & ? & ? & ? & ?). eexists.
    split. eauto. rewrite <- ovar_opp_opp, H in H0. inv H0. Psatz.lra. }
  specialize (fun x ax H => H1 _ _ (To.elements_complete _ x ax H)). clear EQmap_ya.
  match goal with
  | |- context [To.fold ?F map_ya ab'] =>
    set (ab'':=To.fold F map_ya ab'); assert (ρ ∈ γ ab'')
  end.
  { clear H. subst ab''. rewrite To.fold_spec. revert ab' H0.
    induction (To.elements map_ya) as [|[]]; simpl; intros. now auto.
    apply IHl. intros. apply H2. right. auto. clear IHl.
    destruct (To.get_set_spec (ovar_opp e) ab'), To.get_set.
    destruct o. 2:now auto.
    pose proof (H0 (ovar_opp e)). unfold Too.get in H4.
    rewrite <- H in H4. clear H. simpl in H4. rewrite To.fold_spec.
    pattern t1 in H4.
    match goal with
    | H4 : ?F t1 |- γ match ?FOLD with _ => _ end ρ =>
      assert (F (fst FOLD)); [|destruct FOLD as [?[]]]
    end.
    { clear H3. change t1 with (fst (t1, false)) in H4. revert H4 H1.
      generalize (t1, false).
      induction (To.elements row) as [|[]]; simpl; intros. now auto.
      apply IHl0 in H. now auto. 2:now auto. clear IHl0. destruct p. intros.
      destruct (To.get_set_spec e0 t2), To.get_set.
      revert H3. destruct bound_leb; simpl; intros. now auto.
      match type of H3 with
      | context [match ?F with _ => _ end] => destruct F eqn:EQ
      end. 2:now auto.
      simpl in H3, H6. rewrite H6, To.gsspec in H3. destruct To.elt_eq. inv H3. 2:now auto.
      apply fin_float_of_float_correct in EQ. destruct EQ as [? <-].
      edestruct H1 as (? & ? & ?). now eauto.
      edestruct H2 as (? & ? & ?). left. now eauto.
      eexists. eexists. split. rewrite <- ovar_opp_opp, H9, Ropp_involutive. reflexivity.
      split. eauto. eapply reduct_rule_1; eauto. }
    2:now auto.
    rewrite H3. repeat intro. unfold Too.get in H5. rewrite To.gsspec in H5.
    destruct To.elt_eq. subst. now auto. apply H0, H5. }
  revert H3. generalize ab''. clear ab'' ab' H0. intros.
  destruct (To.get (ovar_opp a) ab'') eqn:EQ. 2:now auto.
  pose proof H3 (ovar_opp a). unfold Too.get in H0. rewrite EQ in H0. clear EQ.
  rewrite To.fold_spec. revert H1 ab'' H3.
  induction (To.elements row) as [|[]]; simpl; intros. now auto.
  apply IHl. now auto. destruct (To.get_set_spec (ovar_opp e) ab''), To.get_set as [[]?].
  clear IHl. 2:now auto.
  pose proof H3 (ovar_opp e). unfold Too.get in H6. rewrite <- H4 in H6. clear H4. simpl in H6.
  pattern t1 in H6.
  match goal with
  | H6 : ?F t1 |- γ match ?FOLD with _ => _ end ρ =>
    assert (F (fst FOLD)); [|destruct FOLD as [?[]]]
  end.
  { change t1 with (fst (t1, false)) in H6. rewrite To.fold_spec.
    specialize (fun y b H => H0 _ _ (To.elements_complete _ y b H)). revert H0.
    revert H6. generalize (t1, false).
    induction (To.elements t0) as [|[]]; simpl; intros. now auto. destruct p.
    eapply IHl0, H4. 2:now auto. intros y0 b1.
    destruct (To.get_set_spec e0 t3), To.get_set, bound_leb. now auto.
    simpl. intro.
    match type of H9 with
    | context [match ?F with _ => _ end] => destruct F eqn:EQ
    end. 2:now auto. simpl in H9. rewrite H8, To.gsspec in H9.
    destruct To.elt_eq. 2:now auto. inv H9.
    apply fin_float_of_float_correct in EQ. destruct EQ as [? <-].
    edestruct H1 as (? & ? & ?). eauto.
    edestruct H0 as (? & ? & ? & ? & ?). eauto.
    eexists. eexists. split. rewrite <- ovar_opp_opp, H10, Ropp_involutive. reflexivity.
    split. now eauto. replace (-x-x1) with (-x1-x) by ring.
    rewrite <- ovar_opp_opp, H in H12. inv H12.
    eapply reduct_rule_1; eauto. Psatz.lra. }
  2:now auto. rewrite H5.
  repeat intro. unfold Too.get in H7. rewrite To.gsspec in H7.
  destruct To.elt_eq. 2:now auto. subst. now auto.
Qed.

Definition add_constraints_row (a:ovar) (row:constraint_row) (ab:t) : t :=
  let row := trim_constraints_row a row ab in
  let row := reduce_constraints_row row a ab in
  let row := trim_constraints_row a row ab in
  add_constraints_row_noreduce a row ab.

Lemma add_constraints_row_correct :
  ∀ a row ab ρ av,
    oρ ρ a = Some av -> ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    ρ ∈ γ (add_constraints_row a row ab).
Proof.
  intros. eapply add_constraints_row_noreduce_correct; eauto.
  apply trim_constraints_row_correct,
        reduce_constraints_row_correct, trim_constraints_row_correct; eauto.
Qed.

Definition add_constraint_to_row (r:constraint_row) (y:ovar) (b:float) : constraint_row :=
  match fin_float_of_float b with
  | None => r
  | Some b => To.set y b r
  end.

Lemma add_constraint_to_row_correct:
  ∀ row b ρ y yv v,
    oρ ρ y = Some yv ->
    (RF_le (v - yv) b) ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (add_constraint_to_row row y b) ρ v.
Proof.
  intros. unfold add_constraint_to_row. repeat intro.
  pose proof fin_float_of_float_correct b.
  destruct fin_float_of_float. 2:now auto. edestruct H3. now eauto.
  rewrite To.gsspec in H2. destruct To.elt_eq. 2:now auto. inv H2.
  unfold RF_le in H0. rewrite H4 in H0. now eauto.
Qed.

Fixpoint constraints_row_of_linear_expr (i:fitv) (terms:list (var * (fitv * fitv))) :
  constraint_row * constraint_row * fitv :=
  match terms with
  | nil => (To.empty _, To.empty _, FITV Float.zero Float.zero)
  | (y, (itvα, itvy)) :: q =>
    let iαy := mult_itv itvα itvy in
    let '(constr_p, constr_m, iq) :=
        constraints_row_of_linear_expr (add_itv iαy i) q
    in
    let i := add_itv iq i in
    let 'FITV xpy_a xpy_b :=
        add_itv (mult_itv (add_itv itvα (FITV one one)) itvy) i in
    let mone := Float.neg one in
    let 'FITV xmy_a xmy_b :=
        add_itv (mult_itv (add_itv itvα (FITV mone mone)) itvy) i in
    let constr_p := add_constraint_to_row constr_p (ovPlus y) xmy_b in
    let constr_m := add_constraint_to_row constr_m (ovMinus y) (Float.neg xmy_a) in
    let constr_p := add_constraint_to_row constr_p (ovMinus y) xpy_b in
    let constr_m := add_constraint_to_row constr_m (ovPlus y) (Float.neg xpy_a) in
    (constr_p, constr_m, add_itv iαy iq)
  end.

Transparent Float.zero Float.neg.

Lemma constraints_row_of_linear_expr_correct:
  ∀ terms x i constr_p constr_m iterms ρ,
    eval_linear_expr ρ (i, terms) x ->
    constraints_row_of_linear_expr i terms = (constr_p, constr_m, iterms) ->
    constraints_row_valid constr_p ρ x /\
    constraints_row_valid constr_m ρ (-x) /\
    eval_linear_expr ρ (FITV Float.zero Float.zero, terms) ⊆ γ iterms.
Proof.
  induction terms as [|[y [itvα itvy]]]; simpl; intros.
  - inv H0. split. 2:split.
    repeat intro. rewrite To.gempty in H0. discriminate.
    repeat intro. rewrite To.gempty in H0. discriminate.
    now eauto.
  - specialize (IHterms x (add_itv (mult_itv itvα itvy) i)).
    destruct constraints_row_of_linear_expr as [[constr_p0 constr_m0] iq].
    specialize (IHterms constr_p0 constr_m0 iq ρ).
    unfold eval_linear_expr in H. simpl in H.
    destruct (rρ ρ y) eqn:EQy; destruct H. destruct H as (α & Hα & FOLD).
    assert (eval_linear_expr ρ (add_itv (mult_itv itvα itvy) i, terms) x).
    { apply eval_linear_expr_change_cst in FOLD. destruct FOLD as (? & ? & ?).
      replace x with (x - α * r + (α * r + x0) - x0) by ring. apply H2.
      apply add_itv_correct. apply mult_itv_correct; now auto. now auto. }
    edestruct IHterms as (? & ? & ?). now auto. now auto. clear IHterms.
    assert (∃ x', x' ∈ γ i /\
                  eval_linear_expr ρ (FITV Float.zero Float.zero, terms) (x-x'-α*r)).
    { apply eval_linear_expr_change_cst in FOLD. destruct FOLD as (? & ? & ?).
      eexists. split. now eauto. replace (x - x0 - α * r) with (x - α * r + 0 - x0) by ring.
      apply H6. compute; Psatz.lra. }
    clear FOLD.
    destruct H5 as (? & ? & ?). pose proof (H4 _ H6).
    match type of H0 with
    | (let 'FITV _ _ := ?X in _) = _ =>
      refine ((fun H:(_ ∈ γ X) => _) _); [destruct X|]
    end.
    2:apply add_itv_correct; [apply mult_itv_correct;
      [apply add_itv_correct|]|apply add_itv_correct]; eauto.
    2:instantiate (1:=R1); compute; Psatz.lra.
    match type of H0 with
    | (let 'FITV _ _ := ?X in _) = _ =>
      refine ((fun H:(_ ∈ γ X) => _) _); [destruct X|]
    end.
    2:apply add_itv_correct; [apply mult_itv_correct;
      [apply add_itv_correct|]|apply add_itv_correct]; eauto.
    2:instantiate (1:=(-1)); compute; Psatz.lra.
    inv H0.
    replace ((α + 1) * r + (x - x0 - α * r + x0)) with (x+r) in H8 by ring.
    replace ((α + - 1) * r + (x - x0 - α * r + x0)) with (x-r) in H9 by ring.
    destruct H8, H9.
    split. 2:split.
    + eapply add_constraint_to_row_correct. simpl. rewrite EQy. reflexivity.
      replace (x- -r) with (x+r) by ring. auto.
      eapply add_constraint_to_row_correct; eauto.
    + eapply add_constraint_to_row_correct. eauto.
      replace (-x -r) with (-(x+r)) by ring. auto.
      eapply add_constraint_to_row_correct. simpl. rewrite EQy. reflexivity.
      replace (-x - - r) with (-(x-r)) by ring. auto. auto.
    + intros. red in H11. simpl in H11. rewrite EQy in H11.
      destruct H11 as [(? & ? & ?) ?].
      replace a with (x1*r+(a-x1*r)) by ring.
      apply add_itv_correct; auto. apply mult_itv_correct; auto.
Qed.

Definition meet_constraints_row (x y:constraint_row) : constraint_row :=
  To.combine bound_min x y.

Lemma meet_constraints_row_correct:
  ∀ x a b ρ,
    constraints_row_valid a ρ x ->
    constraints_row_valid b ρ x ->
    constraints_row_valid (meet_constraints_row a b) ρ x.
Proof.
  repeat intro. revert H1.
  unfold meet_constraints_row. rewrite To.gcombine by auto.
  apply bound_min_either; now auto.
Qed.

Fixpoint assume_linear_constraint (i:fitv) (terms:list (var * (fitv * fitv))) (ab:t) : t :=
  match terms with
  | nil => ab
  | (x, (itvα, itvx)) :: q =>
    if fitv_is_top i then ab
    else
      let ip := add_itv (mult_itv (add_itv itvα (FITV one one)) itvx) i in
      let '(constr_p0, constr_m0, iq) := constraints_row_of_linear_expr ip q in
      let ipq := add_itv ip iq in
      let 'FITV lx2 ux2 := add_itv ipq ipq in
      let constr_p0 := add_constraint_to_row constr_p0 (ovMinus x) ux2 in
      let constr_m0 := add_constraint_to_row constr_m0 (ovPlus x) (Float.neg lx2) in

      let im := add_itv (mult_itv (add_itv (opp_itv itvα) (FITV one one)) itvx)
                        (opp_itv i)
      in
      let qm := List.map (fun t =>
        let '(k, (itvα, itvk)) := t in (k, (opp_itv itvα, itvk))) q
      in
      let '(constr_p1, constr_m1, iq) := constraints_row_of_linear_expr im qm in
      let imq := add_itv im iq in
      let 'FITV lx2 ux2 := add_itv imq imq in
      let constr_p1 := add_constraint_to_row constr_p1 (ovMinus x) ux2 in
      let constr_m1 := add_constraint_to_row constr_m1 (ovPlus x) (Float.neg lx2) in

      let constr_p := meet_constraints_row constr_p0 constr_p1 in
      let ab := add_constraints_row (ovPlus x) constr_p ab in
      let constr_m := meet_constraints_row constr_m0 constr_m1 in
      let ab := add_constraints_row (ovMinus x) constr_m ab in

      let i := add_itv (mult_itv itvα itvx) i in
      assume_linear_constraint i q ab
  end.

Lemma assume_linear_constraint_correct:
  ∀ terms i ab ρ,
    ρ ∈ γ ab ->
    eval_linear_expr ρ (i, terms) 0 ->
    ρ ∈ γ (assume_linear_constraint i terms ab).
Proof.
  induction terms as [|[x [itvα itvx]]]. now auto.
  intros. simpl. destruct fitv_is_top. auto.
  unfold eval_linear_expr in H0. simpl in H0. destruct (rρ ρ x) eqn:EQx, H0.
  destruct H0 as (α & Hα & Hr).
  pose proof constraints_row_of_linear_expr_correct terms r
               (add_itv (mult_itv (add_itv itvα (FITV one one)) itvx) i).
  destruct constraints_row_of_linear_expr as [[constr_p0 constr_m0] ?].
  refine (let HH := H0 _ _ _ ρ _ eq_refl in _); clear H0.
  { apply eval_linear_expr_change_cst in Hr. destruct Hr as (? & ? & ?).
    replace r with (0-(α*r)+((α+1)*r+x0)-x0) by ring.
    apply H2, add_itv_correct, H0. apply mult_itv_correct, H1.
    apply add_itv_correct. apply Hα. compute; Psatz.lra. }
  destruct HH as (? & ? & ?).
  pose proof constraints_row_of_linear_expr_correct
       (map (fun t1 => let '(k, (itvα0, itvk)) := t1 in
                       (k, (opp_itv itvα0, itvk))) terms) r
       (add_itv
          (mult_itv (add_itv (opp_itv itvα) (FITV one one)) itvx)
          (opp_itv i)).
  destruct constraints_row_of_linear_expr as [[constr_p1 constr_m1] ?].
  refine (let HH := H4 _ _ _ ρ _ eq_refl in _); clear H4.
  { edestruct eval_linear_expr_change_cst as (? & ? & ?).
    2:replace r with (-(0-α*r)+((-α+1)*r+x0)-x0) by ring;
      apply H5, add_itv_correct, H4; apply mult_itv_correct, H1;
      apply add_itv_correct; [apply opp_itv_correct, Hα|compute; Psatz.lra].
    revert Hr. unfold eval_linear_expr. simpl. generalize (0-α*r). clear.
    induction terms as [|[y [itvβ itvy]]]; simpl; intros. apply opp_itv_correct, Hr.
    destruct (rρ ρ y), Hr. split. 2:now auto.
    destruct H as (β & Hβ & Hr0). eexists. split. now apply opp_itv_correct, Hβ.
    apply IHterms in Hr0.
    replace (- r - - β * r0) with (- (r - β * r0)) by ring. now auto. }
  destruct HH as (? & ? & ?).
  assert (∃ iv, iv ∈ γ i /\
                eval_linear_expr ρ (FITV Float.zero Float.zero, terms) (-α*r-iv)).
  { apply eval_linear_expr_change_cst in Hr. destruct Hr as (? & ? & ?). eexists. split. now eauto.
    replace (- α * r - x0) with (0 - α * r + 0 - x0) by ring. apply H8.
    compute; Psatz.lra. }
  destruct H7 as (iv & Hiv & EVAL).
  repeat match goal with
  | |- _ (let 'FITV lx2 ux2 := add_itv ?I ?I in _) _ =>
    assert (r ∈ γ I); [|destruct (add_itv I I) eqn:?]
  end.
  { replace r with ((α+1)*r + iv + (-α*r-iv)) by ring.
    apply add_itv_correct. apply add_itv_correct. apply mult_itv_correct.
    apply add_itv_correct. now auto. compute; Psatz.lra. now auto. now auto. now auto. }
  { replace r with ((-α+1)*r - iv + (α*r+iv)) by ring.
    apply add_itv_correct. apply add_itv_correct. apply mult_itv_correct.
    apply add_itv_correct. apply opp_itv_correct. now auto. compute; Psatz.lra.
    now auto. apply opp_itv_correct. now auto. apply H6. clear -EVAL.
    replace (-α*r-iv) with (-(α*r+iv)) in EVAL by ring.
    revert EVAL. unfold eval_linear_expr. simpl. generalize (α * r + iv).
    induction terms as [|[k[itvβ itvk]]]; simpl. compute; intros; Psatz.lra.
    destruct (rρ ρ k); intros ? []; intros. split. 2:now auto.
    destruct H as (α0 & Hα0 & FOLD). eexists. split. apply opp_itv_correct, Hα0.
    apply IHterms. replace (-(r1 - - α0 * r0)) with (- r1 - α0 * r0) by ring. now auto. }
  assert ((r + r) ∈ γ (FITV f1 f2)).
  { rewrite <- Heqf1. apply add_itv_correct; auto. }
  assert ((r + r) ∈ γ (FITV f3 f4)).
  { rewrite <- Heqf3. apply add_itv_correct; auto. }
  assert (eval_linear_expr ρ (add_itv (mult_itv itvα itvx) i, terms) 0).
  { apply eval_linear_expr_change_cst in Hr. destruct Hr as (? & ? & ?).
    replace 0 with (0 - α * r + (α*r+x0) - x0) by ring.
    auto using add_itv_correct, mult_itv_correct. }
  apply IHterms, H11.
  eapply add_constraints_row_correct, meet_constraints_row_correct; eauto.
  simpl. rewrite EQx. reflexivity.
  eapply add_constraints_row_correct, meet_constraints_row_correct; eauto.
  - eapply add_constraint_to_row_correct. simpl. rewrite EQx. reflexivity.
    replace (r - - r) with (r + r) by ring. apply H9. now auto.
  - eapply add_constraint_to_row_correct. simpl. rewrite EQx. reflexivity.
    replace (r - - r) with (r + r) by ring. apply H10. now auto.
  - eapply add_constraint_to_row_correct. apply EQx.
    replace (- r - r) with (-(r + r)) by ring. apply H9. now auto.
  - eapply add_constraint_to_row_correct. apply EQx.
    replace (- r - r) with (-(r + r)) by ring. apply H10. now auto.
Qed.

Definition msg_of_bnds
           (a b:option fin_float) (x:var)
           (ty:ideal_num_ty) (itv:iitv+⊤+⊥) : message+⊤+⊥ :=
  let a :=
    match a with
    | None => B754_infinity true
    | Some a => Float.neg (Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half a)
    end
  in
  let b :=
    match b with
    | None => B754_infinity false
    | Some b => Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b
    end
  in
  do itv' <- fitv_of_iitv itvJust (FITV a b);
  let itv' := NotBot (bind itv' (iitv_of_fitv ty)) in
  if itvitv' return message+⊤+⊥ then NotBot All
  else match itv' ⊓ itv with
       | NotBot All => NotBot All
       | Bot => Bot
       | NotBot (Just itv') =>
         NotBot (Just (Broadcasted_msg (
           match IdealIntervals.singleton itv' with
           | Some v => Known_value_msg x v
           | None => Itv_msg x itv'
           end)))
       end.

Lemma msg_of_bnds_correct:
  ∀ (a b:option fin_float) x ty itv ρ xv,
    ρ x ∈ γ ty ->
    ρ x ∈ γ itv ->
    rρ ρ x = Some xv ->
    (∀ a', a = Some a' -> -2*xv <= a') ->
    (∀ b', b = Some b' -> 2*xv <= b') ->
    ρ ∈ γ (msg_of_bnds a b x ty itv).
Proof.
  intros. unfold msg_of_bnds. eapply botbind_spec with (rρ ρ x), @meet_correct.
  2:exact _.
  - intros. destruct (leb itv). constructor.
    match goal with
    | |- γ match ?X with _ => _ end _ => assertx ∈ γ X); [|destruct X as [|[]]; auto]
    end.
    { apply meet_correct. split. 2:now auto. apply toplift_bind_spec with (rρ ρ x), H4.
      intros. apply iitv_of_fitv_correct; auto. }
    pose proof (fun x => IdealIntervals.singleton_correct _ _ x H5).
    destruct IdealIntervals.singleton. 2:now auto. apply H6, eq_refl.
  - split. eapply fitv_of_iitv_correct, H0. rewrite H1. split.
    + destruct b. 2:now auto. specialize (H3 _ eq_refl). clear - H3. unfold RF_le.
      match goal with
      | |- context [Bmult ?a ?b ?c ?d ?e ?f ?g ?h] =>
        pose proof Bmult_correct a b c d e f g h
      end.
      rewrite Rlt_bool_true in H.
      * destruct H as (-> & -> & _). rewrite proj_fin_float_finite.
        apply Rle_trans with (half*f), round_UP_pt, fexp_correct, eq_refl.
        rewrite half_half. Psatz.lra.
      * clear H. eapply Rle_lt_trans, bpow_lt with (e1:=(-1+1024)%Z), eq_refl.
        apply abs_round_le_generic. apply fexp_correct, eq_refl. apply valid_rnd_round_mode.
        apply generic_format_bpow. discriminate.
        rewrite bpow_plus, Rabs_mult. apply Rmult_le_compat.
        apply Rabs_pos. apply Rabs_pos.
        rewrite <- !B2R_Babs with (abs_nan:=Float.abs_pl). compute. Psatz.lra.
        apply Rlt_le, abs_B2R_lt_emax.
    + destruct a. 2:now auto. specialize (H2 _ eq_refl). clear - H2. unfold RF_le.
      unfold Float.neg. rewrite !B2R_Bopp, !is_finite_Bopp, Ropp_involutive.
      match goal with
      | |- context [Bmult ?a ?b ?c ?d ?e ?f ?g ?h] =>
        pose proof Bmult_correct a b c d e f g h
      end.
      rewrite Rlt_bool_true in H.
      * destruct H as (-> & -> & _). rewrite proj_fin_float_finite.
        apply Rle_trans with (half*f), round_UP_pt, fexp_correct, eq_refl.
        rewrite half_half. Psatz.lra.
      * clear H. eapply Rle_lt_trans, bpow_lt with (e1:=(-1+1024)%Z), eq_refl.
        apply abs_round_le_generic. apply fexp_correct, eq_refl. apply valid_rnd_round_mode.
        apply generic_format_bpow. discriminate.
        rewrite bpow_plus, Rabs_mult. apply Rmult_le_compat.
        apply Rabs_pos. apply Rabs_pos.
        rewrite <- !B2R_Babs with (abs_nan:=Float.abs_pl). compute. Psatz.lra.
        apply Rlt_le, abs_B2R_lt_emax.
Qed.

Definition oprocess_msg (m:message) (ab0:t * query_chan) : (t * messages_chan)+⊥.
refine
  (match m with
  | Linear_zero_msg e =>
    let '(ab0, c) := ab0 in
    let ab := assume_linear_constraint (fst e) (T.elements (snd e)) ab0 in
    do ab <- reduce_diag ab0 ab;
    let diff :=
      To.shcombine_diff (fun x mapxy0 mapxy =>
        let a0 := do mapxy0 <- mapxy0; To.get (ovar_opp x) mapxy0 in
        let a := do mapxy <- mapxy; To.get (ovar_opp x) mapxy in
        match a0, a with
        | None, Some _ => a
        | Some a0', Some a' => if Fleb (a0':fin_float) (a':fin_float) then None else a
        | _, _ => None
        end) _
        ab0 ab
    in
    do msgs <-
      T.fold (fun acc x bnds =>
        match bnds with
        | (None, None) => acc
        | (a, b) =>
          match c.(get_var_ty) x with
          | Just ty =>
            let ichan := c.(get_itv) (IEvar ty x) in
            do m <- msg_of_bnds b a x ty ichan;
            match m with
            | All => acc
            | Just m => do acc <- acc; ret (m::acc)
            end
          | All => acc
          end
        end) diff (NotBot nil);
    ret (ab, m::msgs)
  | _ => NotBot (fst ab0, m::nil)
  end).
Proof.
  destruct v. 2:reflexivity. simpl. destruct To.get. 2:reflexivity.
  simpl. rewrite Fleb_refl; auto using is_finite_not_is_nan.
Defined.

Lemma oprocess_msg_correct:
  ∀ m ρ ab,
    ρ ∈ γ ab -> ρ ∈ γ m ->
    ρ ∈ γ (oprocess_msg m ab).
Proof.
  intros [] ρ [ab chan] [Hab Hchan] Hmsg; simpl;
    try (split; [auto|constructor;[eauto|constructor]]).
  eapply botbind_spec, reduce_diag_correct, assume_linear_constraint_correct, Hmsg.
  2:now auto. intros.
  eapply botbind_spec.
  repeat constructor; eauto.
  rewrite T.fold_spec.
  assert (ρ ∈ γ (NotBot List.nil)) by constructor.
  revert H0. generalize (NotBot (@List.nil message)).
  match goal with
  | |- context [@T.elements ?A ?X] =>
    generalize (@T.elements_complete A X); induction (@T.elements A X) as [|[?[]]]
  end. now auto.
  simpl. intros. apply IHl. now auto. clear IHl. specialize (H0 _ _ (or_introl eq_refl)).
  match type of H0 with
  | @T.get ?A e ?M = Some ?X =>
    pose proof (eq_refl:To.get (ovPlus e) M = do m <- @T.get A e M; fst m);
    pose proof (eq_refl:To.get (ovMinus e) M = do m <- @T.get A e M; snd m)
  end.
  rewrite H0 in H3, H2. rewrite To.gshcombine_diff in H2, H3. clear H0. simpl in H3, H2.
  unfold fst in H2, Hab. unfold snd in H3, Hchan. subst o o0.
  pose proof Hab (ovPlus e) (ovMinus e). pose proof Hab (ovMinus e) (ovPlus e).
  pose proof H (ovPlus e) (ovMinus e). pose proof H (ovMinus e) (ovPlus e).
  unfold Too.get in H0, H2, H3, H4. unfold ovar_opp.
  pose proof @get_var_ty_correct _ ρ Hchan e.
  destruct get_var_ty;
  repeat match goal with
  | H : context [@To.get ?A ?B ?C] |- context [@To.get ?A' ?B' ?C'] =>
    change A' with A; change B' with B; change C' with C;
    destruct (@To.get A B C); simpl
  | H: ∀ b, Some _ = Some b -> _ |- _ =>
    edestruct H as (? & ? & ? & ? & ?); [reflexivity|clear H]
  | H: ?A = ?B, H': ?A = ?C |- _ => rewrite H in H'; inv H'
  | |- context [Fleb ?f ?f'] => destruct (Fleb f f')
  | |- context [do x <- _; _] => eapply botbind_spec; [intros|]
  | |- context [msg_of_bnds _ _ _ _ _] => eapply msg_of_bnds_correct
  | |- context [get_itv _ _] => eapply get_itv_correct
  | H:oρ ρ (ovMinus ?e) = Some ?xm,
    H':oρ ρ (ovPlus ?e) = Some ?xp |- _ =>
    simpl in H, H'; rewrite H' in H; inv H
  | |- context [match ?A with _ => _ end] => destruct A
  | |- context [NotBot (_ :: _)] => constructor
  end; eauto; intros ff eq; inv eq;
  match goal with
  | H : (?A <= ?B) |- (?C <= ?D) => eapply Rle_trans, H; Psatz.lra
  end.
Qed.


Definition reduce_constraints_row_step_self (row:constraint_row) (x:ovar) (ab:t):
  constraint_row :=
  match To.get x row with
  | None => row
  | Some ax => reduce_constraints_row_step row x ax ab
  end.

Lemma reduce_constraints_row_step_self_correct:
  ∀ row x ab ρ v,
    ρ ∈ γ ab ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row_step_self row x ab) ρ v.
Proof.
  unfold reduce_constraints_row_step_self. intros.
  pose proof (H0 x). destruct (To.get x row). 2:now auto.
  edestruct H1 as (? & ? & ?). now eauto.
  eapply reduce_constraints_row_step_correct; eauto.
  intros. assert (xv=x0) by congruence. subst. now auto.
Qed.

Definition oassign (x:var) (e0:iexpr) (ab0:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥:=
  let e := (snd ab0).(linearize_expr) e0 in
  let ty := iexpr_ty e0 in
  match e with
  | None => oforget x ab0 c
  | Some e =>
    let ab0 := fst ab0 in
    let ab := oforget0 x ab0 in
    let '(constr_p, constr_m, i) :=
        constraints_row_of_linear_expr (fst e) (T.elements (snd e))
    in
    let i := add_itv (fst e) i in
    let ichan := c.(get_itv) (IEvar (iexpr_ty e0) x) in
    do i <-
      match fitv_of_iitv ichan with
      | All => NotBot i
      | Just i' => i' ⊓ i
      end;
    let 'FITV a b := add_itv i i in

    let constr_p := reduce_constraints_row_step_self constr_p (ovPlus x) ab0 in
    let constr_p := reduce_constraints_row_step_self constr_p (ovMinus x) ab0 in
    let x'mx : option fin_float := To.get (ovPlus x) constr_p in
    let x'px : option fin_float := To.get (ovMinus x) constr_p in
    let b' :=
      do x'mx <- x'mx;
      do x'px <- x'px;
      fin_float_of_float (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                (x'mx:fin_float) (x'px:fin_float))
    in
    let constr_p := T.remove x constr_p in
    let constr_p :=
      match bound_min (fin_float_of_float b) b' with
      | Some b => To.set (ovMinus x) b constr_p
      | _ => constr_p
      end
    in

    let ab := add_constraints_row (ovPlus x) constr_p ab in

    let constr_m := reduce_constraints_row_step_self constr_m (ovPlus x) ab0 in
    let constr_m := reduce_constraints_row_step_self constr_m (ovMinus x) ab0 in
    let mx'mx : option fin_float := To.get (ovPlus x) constr_m in
    let mx'px : option fin_float := To.get (ovMinus x) constr_m in
    let a' :=
      do mx'mx <- mx'mx;
      do mx'px <- mx'px;
      fin_float_of_float
        (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP (mx'mx:fin_float) (mx'px:fin_float))
    in
    let constr_m := T.remove x constr_m in
    let constr_m :=
      match bound_min (fin_float_of_float (Float.neg a)) a' with
      | Some a => To.set (ovPlus x) a constr_m
      | _ => constr_m
      end
    in

    let ab := add_constraints_row (ovMinus x) constr_m ab in

    do ab <- reduce_diag ab0 ab;

    let a := Too.get (ovMinus x, ovPlus x) ab in
    let b := Too.get (ovPlus x, ovMinus x) ab in
    do msg <- msg_of_bnds a b x ty ichan;
    let msgs :=
      match msg with
      | All => nil
      | Just m => m::nil
      end
    in
    ret (ab, msgs)
  end.

Lemma oassign_correct:
  forall x e ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    neval_iexpr ρ e ->
    (ρ+[x => n]) ∈ γ (oassign x e ab chan).
Proof.
  unfold oassign. intros.
  pose proof linearize_expr_correct (snd ab) e.
  destruct ((snd ab).(linearize_expr) e). 2:now auto using oforget_correct.
  edestruct H2 as (y & Hy & EVAL). now eauto. now apply H. now apply H1. clear H2.
  destruct (constraints_row_of_linear_expr (fst t0) (T.elements (snd t0)))
    as [[constr_p constr_m] i] eqn:CONSTR.
  eapply constraints_row_of_linear_expr_correct in CONSTR. 2:now apply EVAL.
  destruct CONSTR as (CONSTRp & CONSTRm & HITV).
  assert (∃ xx,
    eval_linear_expr ρ (FITV Float.zero Float.zero, T.elements (snd t0)) (y-xx) /\
    xx ∈ γ (fst t0)).
  { unfold eval_T_linear_expr in EVAL. apply eval_linear_expr_change_cst in EVAL.
    destruct EVAL as (? & ? & ?). eexists. split. 2:now eauto.
    replace (y - x0) with (y+0-x0) by ring. apply H3. compute; Psatz.lra. }
  destruct H2 as (xx & Hxx1 & Hxx2). apply HITV in Hxx1.
  match goal with
  | |- γ (do i0 <- ?I0; _) _ => assert (y ∈ γ I0)
  end.
  { assert (eval_iexpr (ρ+[x=>n]) (IEvar (iexpr_ty e) x) n).
    { repeat constructor. unfold upd; rewrite eq_dec_true; auto.
      eapply iexpr_ty_correct, H1. }
    eapply get_itv_correct in H2. 2:now eauto.
    apply fitv_of_iitv_correct in H2.
    assert (y ∈ γ (add_itv (fst t0) i)).
    { replace y with (xx+(y-xx)) by ring. apply add_itv_correct; auto. }
    destruct fitv_of_iitv. auto. apply meet_correct. rewrite Hy in H2. auto. }
  eapply botbind_spec. 2:now eauto. clear H2. intros.
  assert ((y + y) ∈ γ (add_itv a a)) by eauto using add_itv_correct.
  destruct add_itv.
  eapply botbind_spec, reduce_diag_correct.
  { intros. eapply botbind_spec, msg_of_bnds_correct. intros.
    split. eauto. destruct a1; constructor. eauto. constructor.
    eapply iexpr_ty_correct. rewrite upd_s. eauto.
    eapply get_itv_correct; eauto. constructor. auto.
    rewrite upd_s. eapply iexpr_ty_correct; eauto.
    unfold rρ. rewrite upd_s. eauto.
    intros. apply H4 in H5. unfold oρ, rρ in H5. rewrite upd_s, Hy in H5.
    destruct H5 as (? & ? & ? & ? & ?). inv H5. inv H6. eapply Rle_trans, H7. Psatz.lra.
    intros. apply H4 in H5. unfold oρ, rρ in H5. rewrite upd_s, Hy in H5.
    destruct H5 as (? & ? & ? & ? & ?). inv H5. inv H6. eapply Rle_trans, H7. Psatz.lra. }
  match goal with
  | |- context [add_constraints_row (ovMinus x) _ ?AB] =>
    assert ((ρ +[ x => n]) ∈ γ AB)
  end.
  { eapply add_constraints_row_correct.
    { unfold upd, oρ, rρ. rewrite eq_dec_true, Hy. reflexivity. }
    apply oforget0_forget, oforget0_incl, H.
    eapply reduce_constraints_row_step_self_correct with (x:=ovPlus x) in CONSTRp. 2:apply H.
    eapply reduce_constraints_row_step_self_correct with (x:=ovMinus x) in CONSTRp. 2:apply H.
    match type of CONSTRp with
    | constraints_row_valid ?X _ _ =>
      assert (constraints_row_valid (T.remove x X) (ρ+[x=>n]) y)
    end.
    { repeat intro. specialize (CONSTRp x0 b). unfold To.get in CONSTRp, H4.
      unfold upd, oρ, rρ.
      destruct x0; simpl in CONSTRp, H4; rewrite T.grspec in H4;
      destruct (T.elt_eq v x); try discriminate;
      (destruct CONSTRp as (xv & Hxv1 & Hxv2); [now auto|]); exists xv; split; auto;
      destruct (eq_dec v x); auto; congruence. }
    match goal with
    | |- constraints_row_valid (match ?BND with _ => _ end) _ _ =>
      assert (∀ bnd, BND = Some bnd -> y+y <= bnd); [|destruct BND]
    end.
    { intro. apply bound_min_either; intro.
      - apply fin_float_of_float_correct in H5. destruct H3, H5 as [? ->].
        unfold RF_le in H3. rewrite H5 in H3. apply H3.
      - pose proof (CONSTRp (ovPlus x)). pose proof (CONSTRp (ovMinus x)).
        destruct To.get, To.get; try discriminate.
        edestruct H6 as (? & ? & ?), H7 as (? & ? & ?). now eauto. now eauto. now eauto.
        simpl in H8, H10. rewrite H8 in H10. inv H10. simpl in H5.
        apply fin_float_of_float_correct in H5. destruct H5 as [? <-].
        replace (y+y) with (y- -y) by ring. eapply reduct_rule_1; eauto. Psatz.lra. }
    2:now auto. specialize (H5 _ eq_refl). repeat intro.
    rewrite To.gsspec in H6. destruct To.elt_eq. inv H6.
    eexists. split. unfold upd, oρ, rρ. rewrite eq_dec_true, Hy. reflexivity. Psatz.lra.
    unfold To.get, PTSUU.get in H6. destruct (ovar_EQ.t_of_s x0) eqn:EQ. rewrite T.grspec in H6.
    destruct T.elt_eq. discriminate.
    specialize (CONSTRp x0). unfold To.get in CONSTRp. rewrite EQ in CONSTRp.
    apply CONSTRp in H6. unfold upd, oρ, rρ. destruct x0; inv EQ.
    destruct (eq_dec v x). congruence. now auto.
    destruct (eq_dec v x). congruence. now auto. }
  eapply add_constraints_row_correct.
  { unfold upd, oρ, rρ. rewrite eq_dec_true, Hy. reflexivity. }
  now apply H4. clear H4.
  eapply reduce_constraints_row_step_self_correct with (x:=ovPlus x) in CONSTRm. 2:apply H.
  eapply reduce_constraints_row_step_self_correct with (x:=ovMinus x) in CONSTRm. 2:apply H.
  match type of CONSTRm with
  | constraints_row_valid ?X _ _ =>
    assert (constraints_row_valid (T.remove x X) (ρ+[x=>n]) (-y))
  end.
  { repeat intro. specialize (CONSTRm x0 b). unfold To.get in CONSTRm, H4.
    unfold upd, oρ, rρ.
    destruct x0; simpl in CONSTRm, H4; rewrite T.grspec in H4;
    destruct (T.elt_eq v x); try discriminate;
    (destruct CONSTRm as (xv & Hxv1 & Hxv2); [now auto|]); exists xv; split; auto;
    destruct (eq_dec v x); auto; congruence. }
    match goal with
    | |- constraints_row_valid (match ?BND with _ => _ end) _ _ =>
      assert (∀ bnd, BND = Some bnd -> -y-y <= bnd); [|destruct BND]
    end.
    { intro. apply bound_min_either; intro.
      - apply fin_float_of_float_correct in H5. destruct H3, H5 as [? <-].
        unfold RF_le in H6. rewrite H5 in H6. Psatz.lra.
      - pose proof (CONSTRm (ovPlus x)). pose proof (CONSTRm (ovMinus x)).
        destruct To.get, To.get; try discriminate.
        edestruct H6 as (? & ? & ?), H7 as (? & ? & ?). now eauto. now eauto. now eauto.
        simpl in H8, H10. rewrite H8 in H10. inv H10. simpl in H5.
        apply fin_float_of_float_correct in H5. destruct H5 as [? <-].
        eapply reduct_rule_1; eauto. Psatz.lra. }
    2:now auto. specialize (H5 _ eq_refl). repeat intro.
    rewrite To.gsspec in H6. destruct To.elt_eq. inv H6.
    eexists. split. unfold upd, oρ, rρ. rewrite eq_dec_true, Hy. reflexivity. Psatz.lra.
    unfold To.get, PTSUU.get in H6. destruct (ovar_EQ.t_of_s x0) eqn:EQ. rewrite T.grspec in H6.
    destruct T.elt_eq. discriminate.
    specialize (CONSTRm x0). unfold To.get in CONSTRm. rewrite EQ in CONSTRm.
    apply CONSTRm in H6. unfold upd, oρ, rρ. destruct x0; inv EQ.
    destruct (eq_dec v x). congruence. now auto.
    destruct (eq_dec v x). congruence. now auto.
Qed.

Program Instance oct_idenv : ab_ideal_env t iter_t :=
  {| id_leb := oleb;
     id_top := otop;
     id_join := ojoin;
     id_init_iter := oinit_iter;
     id_widen := owiden;
     assign := oassign;
     forget := oforget;
     enrich_query_chan ab c := c;
     process_msg := oprocess_msg |}.
Next Obligation.
eapply otop_correct; eauto. Qed.
Next Obligation.
eapply oleb_correct; eauto. Qed.
Next Obligation.
eapply ojoin_correct; eauto. Qed.
Next Obligation.
apply oinit_iter_sound; auto. Qed.
Next Obligation.
apply owiden_incr; auto. Qed.
Next Obligation.
apply oassign_correct; auto. Qed.
Next Obligation.
eapply oforget_correct; eauto. Qed.
Next Obligation.
apply oprocess_msg_correct; auto. Qed.