# Module IdealIntervals

Require Import Utf8 Util FastArith.
Require Import ShareTree.
Require Import ZArith.
Require Import Coqlib ToString.
Require Import ZIntervals FloatIntervals.
Require Import IdealExpr.

Inductive iitv :=
| Az : zitv -> iitv
| Af : fitv -> iitv.

Instance iditv_leb : leb_op iitv := fun x y =>
match x, y return _ with
| Az x, Az y => xy
| Af x, Af y => xy
| Af _, Az _ | Az _, Af _ => false
end.

Program Instance iditv_join : join_op iitv (iitv+⊤) := fun x y =>
match x, y with
| Az x', Az y' =>
let res := x' ⊔ y' in
Just (ifeq x' == res then x else
ifeq y' == res then y else Az res)
| Af x', Af y' =>
let res := x' ⊔ y' in
Just (ifeq x' == res then x else
ifeq y' == res then y else Af res)
| Af _, Az _ | Az _, Af _ => All
end.
Next Obligation.
congruence. Qed.
Next Obligation.
unfold physEq. congruence. Qed.
Next Obligation.
congruence. Qed.
Next Obligation.
unfold physEq. congruence. Qed.

Instance iditv_meet : meet_op iitv (iitv+⊥) := fun x y =>
match x, y with
| Az x, Az y => fmap Az (xy)
| Af x, Af y => fmap Af (xy)
| Af _, Az _ | Az _, Af _ => Bot
end.

Program Definition iditv_widen x y :=
match x, y with
| Az x', Az y' =>
do res <- widen_zitv x' y';
ret (ifeq x' == res then x else
ifeq y' == res then y else Az res)
| Af x', Af y' =>
let res := fitv_widen x' y' in
ret (ifeq x' == res then x else
ifeq y' == res then y else Af res)
| Af _, Az _ | Az _, Af _ => All
end.
Next Obligation.
congruence. Qed.
Next Obligation.
unfold physEq. congruence. Qed.

Instance itv_num_gamma : gamma_op iitv ideal_num := fun v x =>
match v, x with
| Az v, INz x => (x:Z) ∈ γ v
| Af v, INf x => x ∈ γ v
| _, _ => False
end.

Instance iditv_leb_correct : leb_op_correct iitv ideal_num.
Proof.
repeat intro. destruct a1, a2, a; try easy; simpl in *.
eapply leb_correct; eauto.
eapply leb_correct; eauto.
Qed.

Instance iditv_join_correct : join_op_correct iitv (iitv+⊤) ideal_num.
Proof.
repeat intro. destruct x, y, a; try easy; simpl in *; try now intuition; apply join_correct; auto.
Qed.

Instance iditv_meet_correct : meet_op_correct iitv (iitv+⊥) ideal_num.
Proof.
intros [|[]] [|[]] []; intuition (try easy).
eapply botbind_spec. intros. apply H. apply meet_correct; auto.
eapply botbind_spec. intros. apply H. apply meet_correct; auto.
Qed.

Lemma widen_incr:
∀ ab1 ab2, γ ab1 ⊆ γ (iditv_widen ab1 ab2).
Proof.
unfold iditv_widen, physEq. intros. destruct ab1, ab2; try constructor.
- destruct a. contradiction. pose proof ZIntervals.widen_incr z z0 _ H.
destruct widen_zitv; auto.
- destruct a. 2:contradiction. pose proof FloatIntervals.widen_incr f f0 _ H.
destruct fitv_widen; auto.
Qed.

Definition in_z v : zitv+⊤+⊥ :=
match v with
| Just (Az v) => NotBot (Just v)
| Just (Af v) => Bot
| All => NotBot All
end.

Lemma in_z_correct:
∀ ab x, INz x ∈ γ ab -> (x:Z) ∈ γ (in_z ab).
Proof.
destruct ab as [|[]]; simpl; auto.
Qed.

Hint Resolve in_z_correct.

Definition in_f v : fitv+⊤+⊥ :=
match v with
| Just (Af v) => NotBot (Just v)
| Just (Az v) => Bot
| All => NotBot All
end.

Lemma in_f_correct:
∀ ab x, INf x ∈ γ ab -> x ∈ γ (in_f ab).
Proof.
destruct ab as [|[]]; simpl; auto.
Qed.

Hint Resolve in_f_correct.

Definition singleton (itv:iitv) : option ideal_num :=
match itv with
| Az (ZITV a b) => if Zfastleb b a then Some (INz a) else None
| Af (FITV a b) =>
if FloatLib.Fleb b a then
match a with
| Fappli_IEEE.B754_zero _ => None
| _ => Some (INf a)
end
else None
end.

Lemma singleton_correct:
∀ itv x r, x ∈ γ itv -> singleton itv = Some r -> x = r.
Proof.
unfold singleton. intros [[[] []]|[]] [|[]] r [] Hr.
- fastunwrap. destruct (Z.leb_spec x0 x); inv Hr. f_equal. f_equal. Psatz.lia.
- destruct (FloatLib.Fleb f0 f) eqn:?. 2:discriminate.
destruct f as [|[]| |[]], f0 as [|[]| |[]], f1 as [|[]| |[]];
inv Hr; try discriminate; auto; f_equal; apply Fappli_IEEE.B2R_inj; auto;
rewrite FloatLib.Fleb_Rle in * by auto;
FloatLib.Rle_bool_case H; FloatLib.Rle_bool_case H0; FloatLib.Rle_bool_case Heqb;
try discriminate; Psatz.lra.
Qed.

Instance IitvToString : ToString iitv := λ i,
match i with
| Az j => to_string j
| Af j => to_string j
end.