Library Interval.Language.Lang_simpl
From Coq Require Import Bool Floats Reals List Lia Lra.
From Flocq Require Import Core PrimFloat BinarySingleNaN Operations.
Require Import Specific_bigint Specific_ops.
Require Import Interval_helper.
Require Import Float_full.
Require Import Prog.
Require Import Lang_expr.
Local Open Scope R_scope.
Ltac destruct_tuple := try match goal with
| |- match ?t with _ ⇒ _ end ⇒ match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t); destruct_tuple end end.
Ltac destruct_tuple_hyp H := try match type of H with
| match ?t with _ ⇒ _ end ⇒ match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t) in H; destruct_tuple_hyp H end end.
Ltac destruct_tuple_obj t := try match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t) in *; destruct_tuple_obj (fst t) end.
Fixpoint toList {Tl} : evalExprTypeReal_list Tl → list R :=
match Tl with
| nil ⇒ fun _ ⇒ nil
| _ :: Tl' ⇒ fun l ⇒ let x := fst l in let l' := snd l in x :: toList l'
end.
Fixpoint exprsucc t := match t with
| Tree.Evar n ⇒ Tree.Evar (S n)
| Tree.Econst _ ⇒ t
| Tree.Eunary op t' ⇒ Tree.Eunary op (exprsucc t')
| Tree.Ebinary op t1 t2 ⇒ Tree.Ebinary op (exprsucc t1) (exprsucc t2) end.
Lemma eval_exprsucc : ∀ t l x, Tree.eval (exprsucc t) (x :: l) = Tree.eval t l.
Inductive CArithOp := CADD | CSUB | CMUL | CFLTDIV | CINTDIV.
Definition ArithOpToCArithOp T OP := match OP with
| ADD ⇒ CADD
| SUB ⇒ CSUB
| MUL ⇒ CMUL
| DIV ⇒ match T with
| Integer ⇒ CINTDIV
| BinFloat ⇒ CFLTDIV
end
end.
Definition rounding_mode_of_mode md := match md with
| mode_NE | mode_NA ⇒ Basic.rnd_NE
| mode_ZR ⇒ Basic.rnd_ZR
| mode_DN ⇒ Basic.rnd_DN
| mode_UP ⇒ Basic.rnd_UP
end.
Inductive CArithExpr :=
| CInt: Z → CArithExpr
| CBinFl: Z → Z → CArithExpr
| CVar: nat → CArithExpr
| COp: CArithOp → CArithExpr → CArithExpr → CArithExpr
| CRnd: mode → CArithExpr → CArithExpr
| CNearbyint: CArithExpr → CArithExpr
| CTrunc: CArithExpr → CArithExpr
| CLdexp: CArithExpr → CArithExpr → CArithExpr
| CSqrt: CArithExpr → CArithExpr.
Fixpoint CArithExprToTree t := match t with
| CInt n ⇒ Tree.Econst (Tree.Int n)
| CBinFl n1 n2 ⇒ Tree.Ebinary Tree.Mul (Tree.Econst (Tree.Int n1)) (Tree.Econst (Tree.Bpow 2 n2))
| CVar n ⇒ Tree.Evar n
| COp OP t1 t2 ⇒ let u1 := CArithExprToTree t1 in let u2 := CArithExprToTree t2 in match OP with
| CADD ⇒ Tree.Ebinary Tree.Add u1 u2
| CSUB ⇒ Tree.Ebinary Tree.Sub u1 u2
| CMUL ⇒ Tree.Ebinary Tree.Mul u1 u2
| CFLTDIV ⇒ Tree.Ebinary Tree.Div u1 u2
| CINTDIV ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_ZR) (Tree.Ebinary Tree.Div u1 u2)
end
| CRnd md t' ⇒ Tree.Eunary (Tree.RoundFlt (rounding_mode_of_mode md) Rrnd.emin Format64.prec) (CArithExprToTree t')
| CNearbyint t' ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_NE) (CArithExprToTree t')
| CTrunc t' ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_ZR) (CArithExprToTree t')
| CLdexp t' p ⇒ Tree.Econst (Tree.Int 0)
| CSqrt t' ⇒ Tree.Eunary Tree.Sqrt (CArithExprToTree t') end.
Fixpoint Psucc t := match t with
| CInt _ | CBinFl _ _ ⇒ t
| CVar n ⇒ CVar (S n)
| COp OP t1 t2 ⇒ COp OP (Psucc t1) (Psucc t2)
| CRnd md t' ⇒ CRnd md (Psucc t')
| CNearbyint t' ⇒ CNearbyint (Psucc t')
| CTrunc t' ⇒ CTrunc (Psucc t')
| CLdexp t' p ⇒ CLdexp (Psucc t') (Psucc p)
| CSqrt t' ⇒ CSqrt (Psucc t') end.
Lemma CArithExprToTree_Psucc : ∀ t, CArithExprToTree (Psucc t) = exprsucc (CArithExprToTree t).
Definition evalCArithExpr1 t l := Tree.eval (CArithExprToTree t) l.
Fixpoint evalCArithExpr2 t l := match t with
| CInt n ⇒ IZR n
| CBinFl n1 n2 ⇒ IZR n1 × Rpow2 n2
| CVar n ⇒ nth n l R0
| COp OP t1 t2 ⇒ let x1 := evalCArithExpr2 t1 l in let x2 := evalCArithExpr2 t2 l in
match OP with
| CADD ⇒ (evalCArithExpr2 t1 l) + (evalCArithExpr2 t2 l)
| CSUB ⇒ (evalCArithExpr2 t1 l) - (evalCArithExpr2 t2 l)
| CMUL ⇒ (evalCArithExpr2 t1 l) × (evalCArithExpr2 t2 l)
| CFLTDIV ⇒ (evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l)
| CINTDIV ⇒ @Rrnd.nearbyint mode_ZR ((evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l))
end
| CRnd md t' ⇒ round radix2 (FLT_exp emin prec) (round_mode md) (evalCArithExpr2 t' l)
| CNearbyint t' ⇒ @Rrnd.nearbyint mode_NE (evalCArithExpr2 t' l)
| CTrunc t' ⇒ @Rrnd.nearbyint mode_ZR (evalCArithExpr2 t' l)
| CLdexp t' p ⇒ ((evalCArithExpr2 t' l) × Rpower 2 (evalCArithExpr2 p l))
| CSqrt t' ⇒ sqrt (evalCArithExpr2 t' l) end.
Lemma evalCArithExpr2_succ : ∀ t l x, evalCArithExpr2 (Psucc t) (x :: l) = evalCArithExpr2 t l.
Inductive Atom :=
| InInt32: CArithExpr → Atom
| InInt51: CArithExpr → Atom
| InInt64: CArithExpr → Atom
| InFloat64: CArithExpr → Atom
| InFloat64Int: CArithExpr → Atom
| NonZero: CArithExpr → Atom
| NonNeg: CArithExpr → Atom
| RndExact: mode → CArithExpr → Atom
| LdexpControl: Z → CArithExpr → CArithExpr → Atom
.
Definition AtomToProp g l := match g with
| InInt32 t ⇒ - IZR (Int32.N / 2) ≤ evalCArithExpr2 t l ≤ IZR (Int32.N / 2 - 1)
| InInt51 t ⇒ -2251799813685248 ≤ evalCArithExpr2 t l ≤ 2251799813685247
| InInt64 t ⇒ - IZR (Int64.N / 2) ≤ evalCArithExpr2 t l ≤ IZR (Int64.N / 2 - 1)
| InFloat64 t ⇒ Rabs (evalCArithExpr2 t l) ≤ Rrnd.maxval
| InFloat64Int t ⇒ Rabs (evalCArithExpr2 t l) ≤ Rpow2 53
| NonZero t ⇒ evalCArithExpr2 t l ≠ 0
| NonNeg t ⇒ 0 ≤ evalCArithExpr2 t l
| RndExact md t ⇒ let u := evalCArithExpr2 t l in round radix2 (FLT_exp emin prec) (round_mode md) u = u
| LdexpControl n t p ⇒
Rabs (evalCArithExpr2 t l) ≤ IZR (radix2 ^ Rrnd.prec - 1) × Rpow2 (n - Rrnd.prec) ∧
IZR n + evalCArithExpr2 p l ≤ IZR Rrnd.emax end.
Inductive CProp :=
| CTrue | CFalse
| CAtom: Atom → CProp
| CAnd: CProp → CProp → CProp.
Fixpoint CPropToProp p l := match p with
| CFalse ⇒ False
| CTrue ⇒ True
| CAtom i ⇒ AtomToProp i l
| CAnd p1 p2 ⇒ CPropToProp p1 l ∧ CPropToProp p2 l end.
Fixpoint simplifyCProp p := match p with
| CFalse ⇒ CFalse
| CTrue ⇒ CTrue
| CAtom i ⇒ CAtom i
| CAnd p1 p2 ⇒ match simplifyCProp p1, simplifyCProp p2 with
| CTrue, p' | p', CTrue ⇒ p'
| p1', p2' ⇒ CAnd p1' p2' end
end.
Lemma simplifyCProp_correct :
∀ p l, CPropToProp (simplifyCProp p) l ↔ CPropToProp p l.
Fixpoint list_var_aux n init := match n with
| O ⇒ nil
| S n' ⇒ CVar init :: list_var_aux n' (S init) end.
Lemma length_list_var_aux : ∀ n i, length (list_var_aux n i) = n.
Lemma nth_list_var_aux_S: ∀ n k i t, nth (S n) (list_var_aux (S k) i) (Psucc t) =
Psucc (nth n (list_var_aux k i) t).
Definition list_var n := list_var_aux n O.
Lemma list_var_correct1 : ∀ Tl (l : evalExprTypeReal_list Tl) n,
evalCArithExpr1 (nth n (list_var (length Tl)) (CInt 0)) (toList l) = nthExprTypeReal n l 0.
Lemma list_var_correct2 : ∀ Tl (l : evalExprTypeReal_list Tl) n,
evalCArithExpr2 (nth n (list_var (length Tl)) (CInt 0)) (toList l) = nthExprTypeReal n l 0.
Fixpoint compatible t := match t with
| CInt _ | CBinFl _ _ | CVar _ ⇒ true
| COp _ t1 t2 ⇒ andb (compatible t1) (compatible t2)
| CNearbyint t | CTrunc t | CSqrt t ⇒ compatible t
| CRnd md t ⇒ match md with mode_NA ⇒ false | _ ⇒ compatible t end
| CLdexp _ _ ⇒ false end.
Lemma compatible_correct :
∀ t l, compatible t = true → evalCArithExpr1 t l = evalCArithExpr2 t l.
Definition compatible_atom a := match a with
| InInt32 t | InInt51 t | InInt64 t | InFloat64 t
| InFloat64Int t | NonZero t | NonNeg t ⇒ compatible t
| _ ⇒ false
end.
Definition add_compatibility t := (t, compatible t).
Inductive BTree :=
| Void: BTree
| Leaf: Atom → BTree
| Node: BTree → BTree → BTree.
Fixpoint BTreeToList_aux bt acc := match bt with
| Void ⇒ acc
| Leaf i ⇒ i :: acc
| Node bt1 bt2 ⇒
let acc' := BTreeToList_aux bt2 acc in BTreeToList_aux bt1 acc'
end.
Definition BTreeToList bt := BTreeToList_aux bt nil.
Lemma BTreeToList_aux_concat : ∀ bt acc,
BTreeToList_aux bt acc = BTreeToList bt ++ acc.
Fixpoint merge l p := match l with
| nil ⇒ p
| i :: l' ⇒ merge l' (CAnd p (CAtom i))
end.
Lemma merge_decomp : ∀ l1 p l,
CPropToProp (merge l1 p) l ↔ CPropToProp (merge l1 CTrue) l ∧ CPropToProp p l.
Lemma merge_app : ∀ l1 l2 p l,
CPropToProp (merge (l1 ++ l2) p) l ↔
(CPropToProp (merge l1 p) l ∧ CPropToProp (merge l2 p) l).
Fixpoint well_formed {Tl} : evalExprTypeReal_list Tl → _ :=
match Tl with
| nil ⇒ fun _ vars _ ⇒ vars = nil
| _ :: Tl' ⇒ fun lR vars l ⇒ let x := fst lR in let lR' := snd lR in
match vars with
| nil ⇒ False
| (t, b) :: vars' ⇒ (b = true → compatible t = true) ∧
(evalCArithExpr2 t l) = x ∧ well_formed lR' vars' l
end
end.
Lemma well_formed_list_var_aux {Tl} : ∀ (lR : evalExprTypeReal_list Tl) l,
well_formed lR (map add_compatibility (list_var_aux (length Tl) (length l))) (l ++ toList lR).
Corollary well_formed_list_var {Tl} : ∀ (lR : evalExprTypeReal_list Tl),
well_formed lR (map add_compatibility (list_var (length Tl))) (toList lR).
Fixpoint ArrayFree {Tl T} (t : ArithExpr Tl T) := match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ True
| Op _ _ _ t1 t2
| OpExact _ _ t1 t2
⇒ ArrayFree t1 ∧ ArrayFree t2
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ ArrayFree t1 ∧ ArrayFree t2 ∧ ArrayFree t3
| Let _ _ _ t1 t2 ⇒ ArrayFree t1 ∧ ArrayFree t2
| ArrayAcc _ _ _ ⇒ False
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t
| Sqrt _ _ t
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ ArrayFree t
end.
Fixpoint decomposeToCProp {Tl T} (t : ArithExpr Tl T) vars md := match t with
| Int _ n ⇒ (CInt n, true, Void, CTrue)
| BinFl _ x ⇒
let f := Prim2B x in
match f with
| B754_zero _ ⇒ (CBinFl 0 0, true, Void, CTrue)
| B754_finite s m e _ ⇒ (CBinFl (if s then Z.neg m else Z.pos m) e, true, Void, CTrue)
| _ ⇒ (CInt 0%Z, false, Void, CTrue)
end
| Var _ n ⇒
let (u, b) := nth n vars (CInt 0%Z, false) in (u, b, Void, CTrue)
| Op _ T'' OP t1 t2 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let b := andb b1 b2 in
let bt := Node (if b2 then match OP with
| DIV ⇒ Leaf (NonZero u2)
| _ ⇒ Void end else Void) (Node bt1 bt2) in
let p := CAnd (if b2 then CTrue else match OP with
| DIV ⇒ CAtom (NonZero u2)
| _ ⇒ CTrue end) (CAnd p1 p2) in
match T'' with
| Integer ⇒
let t := COp (ArithOpToCArithOp T'' OP) u1 u2 in
let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in
(t, b, bt', p')
| BinFloat ⇒
let t := CRnd md (COp (ArithOpToCArithOp T'' OP) u1 u2) in
let bt' := Node (if b then Leaf (InFloat64 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InFloat64 t)) p in
(t, b, bt', p')
end
| OpExact _ OP t1 t2 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let t := COp (ArithOpToCArithOp BinFloat OP) u1 u2 in
let b := andb b1 b2 in
let bt := Node (if b then match OP with
| DIV ⇒ Node (Leaf (NonZero u2)) (Leaf (InFloat64 t))
| _ ⇒ Leaf (InFloat64 t)
end else Void) (Node bt1 bt2) in
let p := CAnd
(CAnd (if b then CTrue else match OP with
| DIV ⇒ CAnd (CAtom (NonZero u2)) (CAtom (InFloat64 t))
| _ ⇒ CAtom (InFloat64 t)
end) (CAtom (RndExact md t))) (CAnd p1 p2) in
(t, b, bt, p)
| Fma _ t1 t2 t3 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in
let t := CRnd md (COp CADD (COp CMUL u1 u2) u3) in
let b := andb (andb b1 b2) b3 in
let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in
let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in
(t, b, bt, p)
| FmaExact _ t1 t2 t3 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in
let t := COp CADD (COp CMUL u1 u2) u3 in
let b := andb (andb b1 b2) b3 in
let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in
let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in
(t, b, bt, CAnd p (CAtom (RndExact md t)))
| Nearbyint _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
(CNearbyint u, b, bt, p)
| FastNearbyint _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CNearbyint u in
let bt' := Node (if b then Leaf (InInt51 u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt51 u)) p in
(t, b, bt', p')
| FastNearbyintToInt _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CNearbyint u in
let bt' := Node (if b then Leaf (InInt32 u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 u)) p in
(t, b, bt', p')
| TruncToInt _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CTrunc u in
let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in
(t, b, bt', p')
| FloatInj _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let bt' := Node (if b then Leaf (InFloat64Int u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InFloat64Int u)) p in
(u, b, bt', p')
| Sqrt _ T'' t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CSqrt u in
let bt' := Node (if b then Leaf (NonNeg u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (NonNeg u)) p in
match T'' with
| Integer ⇒ (CTrunc t, b, bt', p')
| BinFloat ⇒ (CRnd md t, b, bt', p')
end
| ArrayAcc _ _ _ ⇒ (CInt 0%Z, false, Void, CTrue)
| Let _ _ _ t1 t2 ⇒
let '(u, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(t, b2, bt2, p2) := decomposeToCProp t2 ((u, b1) :: vars) md in
let b := b2 in
let bt := Node bt2 bt1 in
let p := CAnd p1 p2 in
(t, b, bt, p)
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ decomposeToCProp t vars md
end.
Lemma decomposeToCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) vars l md,
md ≠ mode_NA → let lR := M2R_list lM in well_formed lR vars l →
let '(t', b, bt, p) := decomposeToCProp t vars md in
let l' := BTreeToList bt in (
((b = true → compatible t' = true) ∧
(evalCArithExpr2 t' l = evalReal t lR md)) ∧
∀ k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) ∧
(CPropToProp (merge l' p) l → wellBehaved t lM md).
Definition extractCProp {Tl T} (t : ArithExpr Tl T) md :=
let '(_, _, l, p) :=
decomposeToCProp t (map add_compatibility (list_var (length Tl))) md
in (l, simplifyCProp p).
Corollary extractCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md,
md ≠ mode_NA → let lR := M2R_list lM in
let '(bt, p) := extractCProp t md in let l' := BTreeToList bt in
(∀ k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) ∧
(CPropToProp (merge l' p) (toList lR) → wellBehaved t lM md).
Module Faux := SpecificFloat BigIntRadix2.
Module Iaux := FloatIntervalFull Faux.
Module IH := IntervalTacticAux Iaux.
Definition prec := Faux.PtoP 80.
Definition degree := 10%nat.
Definition AtomToGoal g := match g with
| InInt32 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (- Int32.N / 2))) (Tree.Econst (Tree.Int (Int32.N / 2 - 1)))
| InInt51 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (-2251799813685248))) (Tree.Econst (Tree.Int 2251799813685247))
| InInt64 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (- Int64.N / 2))) (Tree.Econst (Tree.Int (Int64.N / 2 - 1)))
| InFloat64 _ ⇒ Reify.Gabsle true (Tree.Ebinary Tree.Mul
(Tree.Ebinary Tree.Sub (Tree.Econst (Tree.Bpow 2 53)) (Tree.Econst (Tree.Int 1)))
(Tree.Econst (Tree.Bpow 2 971)))
| InFloat64Int _ ⇒ Reify.Gabsle true (Tree.Econst (Tree.Bpow 2 53))
| NonZero _ ⇒ Reify.Gne true (Tree.Econst (Tree.Int 0))
| NonNeg _ ⇒ Reify.Gge true (Tree.Econst (Tree.Int 0))
| _ ⇒ Reify.Glt (Tree.Evar O)
end.
Definition getCArithExpr g := match g with
| InInt32 t | InInt64 t | InInt51 t | InFloat64 t
| InFloat64Int t | NonZero t | NonNeg t ⇒ t
| _ ⇒ CInt 0
end.
Lemma AtomToGoal_correct : ∀ i a l,
compatible_atom a = true →
Interval.contains (Iaux.convert i)
(Xreal.Xreal (Tree.eval (CArithExprToTree (getCArithExpr a)) l)) →
IH.R.eval_goal_bnd prec (AtomToGoal a) i = true →
AtomToProp a l.
Fixpoint compareResults goals results := match goals with
| nil ⇒ nil
| g :: goals' ⇒ match results with
| nil ⇒ nil
| res :: results' ⇒ IH.R.eval_goal_bnd prec g res :: compareResults goals' results'
end
end.
Fixpoint par_construct Al (bl : list bool) := match Al with
| nil ⇒ CTrue
| p :: Al' ⇒ match bl with
| nil ⇒ CTrue
| b :: bl' ⇒ let P := par_construct Al' bl' in
if b then (CAnd P (CAtom p)) else P
end
end.
Fixpoint par_mergerest Al (bl : list bool) P := match Al with
| nil ⇒ P
| p :: Al' ⇒ match bl with
| nil ⇒ merge Al' (CAnd P (CAtom p))
| b :: bl' ⇒ let P' := if b then P else (CAnd P (CAtom p)) in
par_mergerest Al' bl' P'
end
end.
Lemma par_mergerest_decomp : ∀ Al bl P l,
CPropToProp (par_mergerest Al bl P) l ↔
CPropToProp (par_mergerest Al bl CTrue) l ∧ CPropToProp P l.
Lemma par_construct_mergerest : ∀ Al bl P l,
CPropToProp (par_construct Al bl) l ∧ CPropToProp (par_mergerest Al bl P) l ↔
CPropToProp (merge Al P) l.
Definition generateCProp {Tl T} (t : ArithExpr Tl T) md vars hyps :=
let (tointerval, unsolvable) := extractCProp t md in
let tointerval := BTreeToList tointerval in
let lexpr := map (fun p ⇒ CArithExprToTree (getCArithExpr p)) tointerval in
match extract_list lexpr vars with
| Eabort ⇒ merge tointerval unsolvable
| Eprog prog consts ⇒
let goals := map (fun p ⇒ AtomToGoal p) tointerval in
let ieval := fun xi ⇒ IH.A.BndValuator.eval prec prog xi in
let bounds := IH.compute_inputs prec hyps consts in
let results := ieval bounds in
let compared := compareResults goals results in
par_mergerest tointerval compared unsolvable end.
Theorem generateCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md hyps P,
md ≠ mode_NA → let lR := M2R_list lM in let l := toList lR in
generateCProp t md (length l) hyps = P →
Reify.eval_hyps hyps l (CPropToProp P l → wellBehaved t lM md).
Definition generateCProp_taylor {Tl T} (t : ArithExpr Tl T) md vars hyps :=
let (tointerval, unsolvable) := extractCProp t md in
let tointerval := BTreeToList tointerval in
let lexpr := map (fun p ⇒ CArithExprToTree (getCArithExpr p)) tointerval in
match extract_list lexpr vars with
| Eabort ⇒ merge tointerval unsolvable
| Eprog prog consts ⇒
let goals := map (fun p ⇒ AtomToGoal p) tointerval in
let bounds := IH.compute_inputs prec hyps consts in
match bounds with
| nil ⇒ merge tointerval unsolvable
| xi :: li ⇒
let li := IH.A.TaylorValuator.TM.var :: map IH.A.TaylorValuator.TM.const li in
let polys := (IH.A.TaylorValuator.eval prec degree xi prog li) in
let results := map (fun p ⇒ IH.A.TaylorValuator.TM.eval (prec, degree) p xi xi) polys in
let compared := compareResults goals results in
par_mergerest tointerval compared unsolvable
end end.
Theorem generateCProp_taylor_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md hyps P,
md ≠ mode_NA → let lR := M2R_list lM in let l := toList lR in
generateCProp_taylor t md (length l) hyps = P →
Reify.eval_hyps hyps l (CPropToProp P l → wellBehaved t lM md).
From Flocq Require Import Core PrimFloat BinarySingleNaN Operations.
Require Import Specific_bigint Specific_ops.
Require Import Interval_helper.
Require Import Float_full.
Require Import Prog.
Require Import Lang_expr.
Local Open Scope R_scope.
Ltac destruct_tuple := try match goal with
| |- match ?t with _ ⇒ _ end ⇒ match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t); destruct_tuple end end.
Ltac destruct_tuple_hyp H := try match type of H with
| match ?t with _ ⇒ _ end ⇒ match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t) in H; destruct_tuple_hyp H end end.
Ltac destruct_tuple_obj t := try match type of t with
| prod _ _ ⇒ rewrite (surjective_pairing t) in *; destruct_tuple_obj (fst t) end.
Fixpoint toList {Tl} : evalExprTypeReal_list Tl → list R :=
match Tl with
| nil ⇒ fun _ ⇒ nil
| _ :: Tl' ⇒ fun l ⇒ let x := fst l in let l' := snd l in x :: toList l'
end.
Fixpoint exprsucc t := match t with
| Tree.Evar n ⇒ Tree.Evar (S n)
| Tree.Econst _ ⇒ t
| Tree.Eunary op t' ⇒ Tree.Eunary op (exprsucc t')
| Tree.Ebinary op t1 t2 ⇒ Tree.Ebinary op (exprsucc t1) (exprsucc t2) end.
Lemma eval_exprsucc : ∀ t l x, Tree.eval (exprsucc t) (x :: l) = Tree.eval t l.
Inductive CArithOp := CADD | CSUB | CMUL | CFLTDIV | CINTDIV.
Definition ArithOpToCArithOp T OP := match OP with
| ADD ⇒ CADD
| SUB ⇒ CSUB
| MUL ⇒ CMUL
| DIV ⇒ match T with
| Integer ⇒ CINTDIV
| BinFloat ⇒ CFLTDIV
end
end.
Definition rounding_mode_of_mode md := match md with
| mode_NE | mode_NA ⇒ Basic.rnd_NE
| mode_ZR ⇒ Basic.rnd_ZR
| mode_DN ⇒ Basic.rnd_DN
| mode_UP ⇒ Basic.rnd_UP
end.
Inductive CArithExpr :=
| CInt: Z → CArithExpr
| CBinFl: Z → Z → CArithExpr
| CVar: nat → CArithExpr
| COp: CArithOp → CArithExpr → CArithExpr → CArithExpr
| CRnd: mode → CArithExpr → CArithExpr
| CNearbyint: CArithExpr → CArithExpr
| CTrunc: CArithExpr → CArithExpr
| CLdexp: CArithExpr → CArithExpr → CArithExpr
| CSqrt: CArithExpr → CArithExpr.
Fixpoint CArithExprToTree t := match t with
| CInt n ⇒ Tree.Econst (Tree.Int n)
| CBinFl n1 n2 ⇒ Tree.Ebinary Tree.Mul (Tree.Econst (Tree.Int n1)) (Tree.Econst (Tree.Bpow 2 n2))
| CVar n ⇒ Tree.Evar n
| COp OP t1 t2 ⇒ let u1 := CArithExprToTree t1 in let u2 := CArithExprToTree t2 in match OP with
| CADD ⇒ Tree.Ebinary Tree.Add u1 u2
| CSUB ⇒ Tree.Ebinary Tree.Sub u1 u2
| CMUL ⇒ Tree.Ebinary Tree.Mul u1 u2
| CFLTDIV ⇒ Tree.Ebinary Tree.Div u1 u2
| CINTDIV ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_ZR) (Tree.Ebinary Tree.Div u1 u2)
end
| CRnd md t' ⇒ Tree.Eunary (Tree.RoundFlt (rounding_mode_of_mode md) Rrnd.emin Format64.prec) (CArithExprToTree t')
| CNearbyint t' ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_NE) (CArithExprToTree t')
| CTrunc t' ⇒ Tree.Eunary (Tree.Nearbyint Basic.rnd_ZR) (CArithExprToTree t')
| CLdexp t' p ⇒ Tree.Econst (Tree.Int 0)
| CSqrt t' ⇒ Tree.Eunary Tree.Sqrt (CArithExprToTree t') end.
Fixpoint Psucc t := match t with
| CInt _ | CBinFl _ _ ⇒ t
| CVar n ⇒ CVar (S n)
| COp OP t1 t2 ⇒ COp OP (Psucc t1) (Psucc t2)
| CRnd md t' ⇒ CRnd md (Psucc t')
| CNearbyint t' ⇒ CNearbyint (Psucc t')
| CTrunc t' ⇒ CTrunc (Psucc t')
| CLdexp t' p ⇒ CLdexp (Psucc t') (Psucc p)
| CSqrt t' ⇒ CSqrt (Psucc t') end.
Lemma CArithExprToTree_Psucc : ∀ t, CArithExprToTree (Psucc t) = exprsucc (CArithExprToTree t).
Definition evalCArithExpr1 t l := Tree.eval (CArithExprToTree t) l.
Fixpoint evalCArithExpr2 t l := match t with
| CInt n ⇒ IZR n
| CBinFl n1 n2 ⇒ IZR n1 × Rpow2 n2
| CVar n ⇒ nth n l R0
| COp OP t1 t2 ⇒ let x1 := evalCArithExpr2 t1 l in let x2 := evalCArithExpr2 t2 l in
match OP with
| CADD ⇒ (evalCArithExpr2 t1 l) + (evalCArithExpr2 t2 l)
| CSUB ⇒ (evalCArithExpr2 t1 l) - (evalCArithExpr2 t2 l)
| CMUL ⇒ (evalCArithExpr2 t1 l) × (evalCArithExpr2 t2 l)
| CFLTDIV ⇒ (evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l)
| CINTDIV ⇒ @Rrnd.nearbyint mode_ZR ((evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l))
end
| CRnd md t' ⇒ round radix2 (FLT_exp emin prec) (round_mode md) (evalCArithExpr2 t' l)
| CNearbyint t' ⇒ @Rrnd.nearbyint mode_NE (evalCArithExpr2 t' l)
| CTrunc t' ⇒ @Rrnd.nearbyint mode_ZR (evalCArithExpr2 t' l)
| CLdexp t' p ⇒ ((evalCArithExpr2 t' l) × Rpower 2 (evalCArithExpr2 p l))
| CSqrt t' ⇒ sqrt (evalCArithExpr2 t' l) end.
Lemma evalCArithExpr2_succ : ∀ t l x, evalCArithExpr2 (Psucc t) (x :: l) = evalCArithExpr2 t l.
Inductive Atom :=
| InInt32: CArithExpr → Atom
| InInt51: CArithExpr → Atom
| InInt64: CArithExpr → Atom
| InFloat64: CArithExpr → Atom
| InFloat64Int: CArithExpr → Atom
| NonZero: CArithExpr → Atom
| NonNeg: CArithExpr → Atom
| RndExact: mode → CArithExpr → Atom
| LdexpControl: Z → CArithExpr → CArithExpr → Atom
.
Definition AtomToProp g l := match g with
| InInt32 t ⇒ - IZR (Int32.N / 2) ≤ evalCArithExpr2 t l ≤ IZR (Int32.N / 2 - 1)
| InInt51 t ⇒ -2251799813685248 ≤ evalCArithExpr2 t l ≤ 2251799813685247
| InInt64 t ⇒ - IZR (Int64.N / 2) ≤ evalCArithExpr2 t l ≤ IZR (Int64.N / 2 - 1)
| InFloat64 t ⇒ Rabs (evalCArithExpr2 t l) ≤ Rrnd.maxval
| InFloat64Int t ⇒ Rabs (evalCArithExpr2 t l) ≤ Rpow2 53
| NonZero t ⇒ evalCArithExpr2 t l ≠ 0
| NonNeg t ⇒ 0 ≤ evalCArithExpr2 t l
| RndExact md t ⇒ let u := evalCArithExpr2 t l in round radix2 (FLT_exp emin prec) (round_mode md) u = u
| LdexpControl n t p ⇒
Rabs (evalCArithExpr2 t l) ≤ IZR (radix2 ^ Rrnd.prec - 1) × Rpow2 (n - Rrnd.prec) ∧
IZR n + evalCArithExpr2 p l ≤ IZR Rrnd.emax end.
Inductive CProp :=
| CTrue | CFalse
| CAtom: Atom → CProp
| CAnd: CProp → CProp → CProp.
Fixpoint CPropToProp p l := match p with
| CFalse ⇒ False
| CTrue ⇒ True
| CAtom i ⇒ AtomToProp i l
| CAnd p1 p2 ⇒ CPropToProp p1 l ∧ CPropToProp p2 l end.
Fixpoint simplifyCProp p := match p with
| CFalse ⇒ CFalse
| CTrue ⇒ CTrue
| CAtom i ⇒ CAtom i
| CAnd p1 p2 ⇒ match simplifyCProp p1, simplifyCProp p2 with
| CTrue, p' | p', CTrue ⇒ p'
| p1', p2' ⇒ CAnd p1' p2' end
end.
Lemma simplifyCProp_correct :
∀ p l, CPropToProp (simplifyCProp p) l ↔ CPropToProp p l.
Fixpoint list_var_aux n init := match n with
| O ⇒ nil
| S n' ⇒ CVar init :: list_var_aux n' (S init) end.
Lemma length_list_var_aux : ∀ n i, length (list_var_aux n i) = n.
Lemma nth_list_var_aux_S: ∀ n k i t, nth (S n) (list_var_aux (S k) i) (Psucc t) =
Psucc (nth n (list_var_aux k i) t).
Definition list_var n := list_var_aux n O.
Lemma list_var_correct1 : ∀ Tl (l : evalExprTypeReal_list Tl) n,
evalCArithExpr1 (nth n (list_var (length Tl)) (CInt 0)) (toList l) = nthExprTypeReal n l 0.
Lemma list_var_correct2 : ∀ Tl (l : evalExprTypeReal_list Tl) n,
evalCArithExpr2 (nth n (list_var (length Tl)) (CInt 0)) (toList l) = nthExprTypeReal n l 0.
Fixpoint compatible t := match t with
| CInt _ | CBinFl _ _ | CVar _ ⇒ true
| COp _ t1 t2 ⇒ andb (compatible t1) (compatible t2)
| CNearbyint t | CTrunc t | CSqrt t ⇒ compatible t
| CRnd md t ⇒ match md with mode_NA ⇒ false | _ ⇒ compatible t end
| CLdexp _ _ ⇒ false end.
Lemma compatible_correct :
∀ t l, compatible t = true → evalCArithExpr1 t l = evalCArithExpr2 t l.
Definition compatible_atom a := match a with
| InInt32 t | InInt51 t | InInt64 t | InFloat64 t
| InFloat64Int t | NonZero t | NonNeg t ⇒ compatible t
| _ ⇒ false
end.
Definition add_compatibility t := (t, compatible t).
Inductive BTree :=
| Void: BTree
| Leaf: Atom → BTree
| Node: BTree → BTree → BTree.
Fixpoint BTreeToList_aux bt acc := match bt with
| Void ⇒ acc
| Leaf i ⇒ i :: acc
| Node bt1 bt2 ⇒
let acc' := BTreeToList_aux bt2 acc in BTreeToList_aux bt1 acc'
end.
Definition BTreeToList bt := BTreeToList_aux bt nil.
Lemma BTreeToList_aux_concat : ∀ bt acc,
BTreeToList_aux bt acc = BTreeToList bt ++ acc.
Fixpoint merge l p := match l with
| nil ⇒ p
| i :: l' ⇒ merge l' (CAnd p (CAtom i))
end.
Lemma merge_decomp : ∀ l1 p l,
CPropToProp (merge l1 p) l ↔ CPropToProp (merge l1 CTrue) l ∧ CPropToProp p l.
Lemma merge_app : ∀ l1 l2 p l,
CPropToProp (merge (l1 ++ l2) p) l ↔
(CPropToProp (merge l1 p) l ∧ CPropToProp (merge l2 p) l).
Fixpoint well_formed {Tl} : evalExprTypeReal_list Tl → _ :=
match Tl with
| nil ⇒ fun _ vars _ ⇒ vars = nil
| _ :: Tl' ⇒ fun lR vars l ⇒ let x := fst lR in let lR' := snd lR in
match vars with
| nil ⇒ False
| (t, b) :: vars' ⇒ (b = true → compatible t = true) ∧
(evalCArithExpr2 t l) = x ∧ well_formed lR' vars' l
end
end.
Lemma well_formed_list_var_aux {Tl} : ∀ (lR : evalExprTypeReal_list Tl) l,
well_formed lR (map add_compatibility (list_var_aux (length Tl) (length l))) (l ++ toList lR).
Corollary well_formed_list_var {Tl} : ∀ (lR : evalExprTypeReal_list Tl),
well_formed lR (map add_compatibility (list_var (length Tl))) (toList lR).
Fixpoint ArrayFree {Tl T} (t : ArithExpr Tl T) := match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ True
| Op _ _ _ t1 t2
| OpExact _ _ t1 t2
⇒ ArrayFree t1 ∧ ArrayFree t2
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ ArrayFree t1 ∧ ArrayFree t2 ∧ ArrayFree t3
| Let _ _ _ t1 t2 ⇒ ArrayFree t1 ∧ ArrayFree t2
| ArrayAcc _ _ _ ⇒ False
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t
| Sqrt _ _ t
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ ArrayFree t
end.
Fixpoint decomposeToCProp {Tl T} (t : ArithExpr Tl T) vars md := match t with
| Int _ n ⇒ (CInt n, true, Void, CTrue)
| BinFl _ x ⇒
let f := Prim2B x in
match f with
| B754_zero _ ⇒ (CBinFl 0 0, true, Void, CTrue)
| B754_finite s m e _ ⇒ (CBinFl (if s then Z.neg m else Z.pos m) e, true, Void, CTrue)
| _ ⇒ (CInt 0%Z, false, Void, CTrue)
end
| Var _ n ⇒
let (u, b) := nth n vars (CInt 0%Z, false) in (u, b, Void, CTrue)
| Op _ T'' OP t1 t2 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let b := andb b1 b2 in
let bt := Node (if b2 then match OP with
| DIV ⇒ Leaf (NonZero u2)
| _ ⇒ Void end else Void) (Node bt1 bt2) in
let p := CAnd (if b2 then CTrue else match OP with
| DIV ⇒ CAtom (NonZero u2)
| _ ⇒ CTrue end) (CAnd p1 p2) in
match T'' with
| Integer ⇒
let t := COp (ArithOpToCArithOp T'' OP) u1 u2 in
let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in
(t, b, bt', p')
| BinFloat ⇒
let t := CRnd md (COp (ArithOpToCArithOp T'' OP) u1 u2) in
let bt' := Node (if b then Leaf (InFloat64 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InFloat64 t)) p in
(t, b, bt', p')
end
| OpExact _ OP t1 t2 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let t := COp (ArithOpToCArithOp BinFloat OP) u1 u2 in
let b := andb b1 b2 in
let bt := Node (if b then match OP with
| DIV ⇒ Node (Leaf (NonZero u2)) (Leaf (InFloat64 t))
| _ ⇒ Leaf (InFloat64 t)
end else Void) (Node bt1 bt2) in
let p := CAnd
(CAnd (if b then CTrue else match OP with
| DIV ⇒ CAnd (CAtom (NonZero u2)) (CAtom (InFloat64 t))
| _ ⇒ CAtom (InFloat64 t)
end) (CAtom (RndExact md t))) (CAnd p1 p2) in
(t, b, bt, p)
| Fma _ t1 t2 t3 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in
let t := CRnd md (COp CADD (COp CMUL u1 u2) u3) in
let b := andb (andb b1 b2) b3 in
let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in
let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in
(t, b, bt, p)
| FmaExact _ t1 t2 t3 ⇒
let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in
let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in
let t := COp CADD (COp CMUL u1 u2) u3 in
let b := andb (andb b1 b2) b3 in
let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in
let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in
(t, b, bt, CAnd p (CAtom (RndExact md t)))
| Nearbyint _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
(CNearbyint u, b, bt, p)
| FastNearbyint _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CNearbyint u in
let bt' := Node (if b then Leaf (InInt51 u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt51 u)) p in
(t, b, bt', p')
| FastNearbyintToInt _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CNearbyint u in
let bt' := Node (if b then Leaf (InInt32 u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 u)) p in
(t, b, bt', p')
| TruncToInt _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CTrunc u in
let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in
(t, b, bt', p')
| FloatInj _ t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let bt' := Node (if b then Leaf (InFloat64Int u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (InFloat64Int u)) p in
(u, b, bt', p')
| Sqrt _ T'' t ⇒
let '(u, b, bt, p) := decomposeToCProp t vars md in
let t := CSqrt u in
let bt' := Node (if b then Leaf (NonNeg u) else Void) bt in
let p' := CAnd (if b then CTrue else CAtom (NonNeg u)) p in
match T'' with
| Integer ⇒ (CTrunc t, b, bt', p')
| BinFloat ⇒ (CRnd md t, b, bt', p')
end
| ArrayAcc _ _ _ ⇒ (CInt 0%Z, false, Void, CTrue)
| Let _ _ _ t1 t2 ⇒
let '(u, b1, bt1, p1) := decomposeToCProp t1 vars md in
let '(t, b2, bt2, p2) := decomposeToCProp t2 ((u, b1) :: vars) md in
let b := b2 in
let bt := Node bt2 bt1 in
let p := CAnd p1 p2 in
(t, b, bt, p)
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ decomposeToCProp t vars md
end.
Lemma decomposeToCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) vars l md,
md ≠ mode_NA → let lR := M2R_list lM in well_formed lR vars l →
let '(t', b, bt, p) := decomposeToCProp t vars md in
let l' := BTreeToList bt in (
((b = true → compatible t' = true) ∧
(evalCArithExpr2 t' l = evalReal t lR md)) ∧
∀ k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) ∧
(CPropToProp (merge l' p) l → wellBehaved t lM md).
Definition extractCProp {Tl T} (t : ArithExpr Tl T) md :=
let '(_, _, l, p) :=
decomposeToCProp t (map add_compatibility (list_var (length Tl))) md
in (l, simplifyCProp p).
Corollary extractCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md,
md ≠ mode_NA → let lR := M2R_list lM in
let '(bt, p) := extractCProp t md in let l' := BTreeToList bt in
(∀ k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) ∧
(CPropToProp (merge l' p) (toList lR) → wellBehaved t lM md).
Module Faux := SpecificFloat BigIntRadix2.
Module Iaux := FloatIntervalFull Faux.
Module IH := IntervalTacticAux Iaux.
Definition prec := Faux.PtoP 80.
Definition degree := 10%nat.
Definition AtomToGoal g := match g with
| InInt32 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (- Int32.N / 2))) (Tree.Econst (Tree.Int (Int32.N / 2 - 1)))
| InInt51 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (-2251799813685248))) (Tree.Econst (Tree.Int 2251799813685247))
| InInt64 _ ⇒ Reify.Glele (Tree.Econst (Tree.Int (- Int64.N / 2))) (Tree.Econst (Tree.Int (Int64.N / 2 - 1)))
| InFloat64 _ ⇒ Reify.Gabsle true (Tree.Ebinary Tree.Mul
(Tree.Ebinary Tree.Sub (Tree.Econst (Tree.Bpow 2 53)) (Tree.Econst (Tree.Int 1)))
(Tree.Econst (Tree.Bpow 2 971)))
| InFloat64Int _ ⇒ Reify.Gabsle true (Tree.Econst (Tree.Bpow 2 53))
| NonZero _ ⇒ Reify.Gne true (Tree.Econst (Tree.Int 0))
| NonNeg _ ⇒ Reify.Gge true (Tree.Econst (Tree.Int 0))
| _ ⇒ Reify.Glt (Tree.Evar O)
end.
Definition getCArithExpr g := match g with
| InInt32 t | InInt64 t | InInt51 t | InFloat64 t
| InFloat64Int t | NonZero t | NonNeg t ⇒ t
| _ ⇒ CInt 0
end.
Lemma AtomToGoal_correct : ∀ i a l,
compatible_atom a = true →
Interval.contains (Iaux.convert i)
(Xreal.Xreal (Tree.eval (CArithExprToTree (getCArithExpr a)) l)) →
IH.R.eval_goal_bnd prec (AtomToGoal a) i = true →
AtomToProp a l.
Fixpoint compareResults goals results := match goals with
| nil ⇒ nil
| g :: goals' ⇒ match results with
| nil ⇒ nil
| res :: results' ⇒ IH.R.eval_goal_bnd prec g res :: compareResults goals' results'
end
end.
Fixpoint par_construct Al (bl : list bool) := match Al with
| nil ⇒ CTrue
| p :: Al' ⇒ match bl with
| nil ⇒ CTrue
| b :: bl' ⇒ let P := par_construct Al' bl' in
if b then (CAnd P (CAtom p)) else P
end
end.
Fixpoint par_mergerest Al (bl : list bool) P := match Al with
| nil ⇒ P
| p :: Al' ⇒ match bl with
| nil ⇒ merge Al' (CAnd P (CAtom p))
| b :: bl' ⇒ let P' := if b then P else (CAnd P (CAtom p)) in
par_mergerest Al' bl' P'
end
end.
Lemma par_mergerest_decomp : ∀ Al bl P l,
CPropToProp (par_mergerest Al bl P) l ↔
CPropToProp (par_mergerest Al bl CTrue) l ∧ CPropToProp P l.
Lemma par_construct_mergerest : ∀ Al bl P l,
CPropToProp (par_construct Al bl) l ∧ CPropToProp (par_mergerest Al bl P) l ↔
CPropToProp (merge Al P) l.
Definition generateCProp {Tl T} (t : ArithExpr Tl T) md vars hyps :=
let (tointerval, unsolvable) := extractCProp t md in
let tointerval := BTreeToList tointerval in
let lexpr := map (fun p ⇒ CArithExprToTree (getCArithExpr p)) tointerval in
match extract_list lexpr vars with
| Eabort ⇒ merge tointerval unsolvable
| Eprog prog consts ⇒
let goals := map (fun p ⇒ AtomToGoal p) tointerval in
let ieval := fun xi ⇒ IH.A.BndValuator.eval prec prog xi in
let bounds := IH.compute_inputs prec hyps consts in
let results := ieval bounds in
let compared := compareResults goals results in
par_mergerest tointerval compared unsolvable end.
Theorem generateCProp_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md hyps P,
md ≠ mode_NA → let lR := M2R_list lM in let l := toList lR in
generateCProp t md (length l) hyps = P →
Reify.eval_hyps hyps l (CPropToProp P l → wellBehaved t lM md).
Definition generateCProp_taylor {Tl T} (t : ArithExpr Tl T) md vars hyps :=
let (tointerval, unsolvable) := extractCProp t md in
let tointerval := BTreeToList tointerval in
let lexpr := map (fun p ⇒ CArithExprToTree (getCArithExpr p)) tointerval in
match extract_list lexpr vars with
| Eabort ⇒ merge tointerval unsolvable
| Eprog prog consts ⇒
let goals := map (fun p ⇒ AtomToGoal p) tointerval in
let bounds := IH.compute_inputs prec hyps consts in
match bounds with
| nil ⇒ merge tointerval unsolvable
| xi :: li ⇒
let li := IH.A.TaylorValuator.TM.var :: map IH.A.TaylorValuator.TM.const li in
let polys := (IH.A.TaylorValuator.eval prec degree xi prog li) in
let results := map (fun p ⇒ IH.A.TaylorValuator.TM.eval (prec, degree) p xi xi) polys in
let compared := compareResults goals results in
par_mergerest tointerval compared unsolvable
end end.
Theorem generateCProp_taylor_correct {Tl T} :
∀ (t : ArithExpr Tl T), ArrayFree t →
∀ (lM : evalExprTypeRounded_list Tl) md hyps P,
md ≠ mode_NA → let lR := M2R_list lM in let l := toList lR in
generateCProp_taylor t md (length l) hyps = P →
Reify.eval_hyps hyps l (CPropToProp P l → wellBehaved t lM md).