Library Interval.Eval.Tree

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2019, Inria
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import Reals List.

Require Import Xreal.
Require Import Basic.
Require Import Interval.

Inductive nullary_op : Set :=
  | Int (n : Z) | Bpow (r n : Z) | Pi.

Inductive unary_op : Set :=
  | Neg | Abs | Inv | Sqr | Sqrt
  | Cos | Sin | Tan | Atan | Exp | Ln
  | PowerInt (n : Z) | Nearbyint (m : rounding_mode)
  | Round (m : rounding_mode) (emin : Z) (prec : positive).

Inductive binary_op : Set :=
  | Add | Sub | Mul | Div.

Inductive expr : Set :=
  | Evar : nat expr
  | Econst : nullary_op expr
  | Eunary : unary_op expr expr
  | Ebinary : binary_op expr expr expr.

Definition bpow' (r e : Z) :=
  match e with
  | 0%Z ⇒ 1%R
  | Z.pos pIZR (Z.pow_pos r p)
  | Z.neg p ⇒ (/ IZR (Z.pow_pos r p))%R
  end.

Definition nullary_real (o : nullary_op) : R :=
  match o with
  | Int nIZR n
  | Bpow r nbpow' r n
  | PiPI
  end.

Definition unary_real (o : unary_op) : R R :=
  match o with
  | NegRopp
  | AbsRabs
  | InvRinv
  | SqrRsqr
  | Sqrtsqrt
  | Coscos
  | Sinsin
  | Tantan
  | Atanatan
  | Expexp
  | Lnln
  | PowerInt nfun xpowerRZ x n
  | Nearbyint mRnearbyint m
  | Round m emin precround_flt m emin prec
  end.

Strategy 1000 [Generic_fmt.round].

Definition binary_real (o : binary_op) : R R R :=
  match o with
  | AddRplus
  | SubRminus
  | MulRmult
  | DivRdiv
  end.

Fixpoint eval (e : expr) (l : list R) :=
  match e with
  | Evar nnth n l 0%R
  | Econst onullary_real o
  | Eunary o e1unary_real o (eval e1 l)
  | Ebinary o e1 e2binary_real o (eval e1 l) (eval e2 l)
  end.

Ltac is_nat_const n :=
  match n with
  | S ?nis_nat_const n
  | Otrue
  | _false
  end.

Ltac is_positive_const x :=
  match x with
  | xO ?pis_positive_const p
  | xI ?pis_positive_const p
  | xHtrue
  | _false
  end.

Ltac is_Z_const x :=
  lazymatch x with
  | Zpos ?pis_positive_const p
  | Zneg ?pis_positive_const p
  | Z0true
  | _false
  end.

Ltac list_add a l :=
  let rec aux l :=
    match l with
    | nilconstr:(cons a l)
    | cons a _l
    | cons ?x ?llet l := aux l in constr:(cons x l)
    end in
  aux l.

Ltac list_find a l :=
  let rec aux l n :=
    match l with
    | cons a _n
    | cons _ ?laux l (S n)
    end in
  aux l O.

Ltac hyp_on_var x :=
  lazymatch goal with
  | H : (?u x ?v)%R |- _true
  | H : (?u x < ?v)%R |- _true
  | H : (?u < x ?v)%R |- _true
  | H : (?u < x < ?v)%R |- _true
  | H : (?u x)%R |- _true
  | H : (x ?u)%R |- _true
  | H : (x ?v)%R |- _true
  | H : (?v x)%R |- _true
  | H : (Rabs x ?v)%R |- _true
  | H : (?v Rabs x)%R |- _true
  | H : (?u < x)%R |- _true
  | H : (x > ?u)%R |- _true
  | H : (x < ?v)%R |- _true
  | H : (?v > x)%R |- _true
  | H : (Rabs x < ?v)%R |- _true
  | H : (?v > Rabs x)%R |- _true
  end.

Ltac reify_round m :=
  lazymatch m with
  | Round_NE.ZnearestErnd_NE
  | Raux.Ztruncrnd_ZR
  | Raux.Zfloorrnd_DN
  | Raux.Zceilrnd_UP
  end.

Ltac unfold_head t :=
  let rec head t :=
    lazymatch t with
    | Ropp _t
    | Rabs _t
    | Rinv _t
    | Rsqr _t
    | Rmult _ _t
    | sqrt _t
    | cos _t
    | sin _t
    | tan _t
    | atan _t
    | exp _t
    | ln _t
    | powerRZ _ _t
    | pow _ _t
    | Rdiv _ _t
    | Rpower _ _t
    | Rnearbyint _ _t
    | Generic_fmt.round _ _ _ _t
    | IZR _t
    | Raux.bpow _ _t
    | ?f _head f
    | _t
    end in
  let h := head t in
  eval unfold h in t.

Ltac get_vars t l :=
  let rec aux t l top :=
    let aux_u a := aux a l top in
    let aux_b a b :=
      let l := aux a l top in
      aux b l top in
    match True with
    | True
    lazymatch t with
    | Ropp ?aaux_u a
    | Rabs ?aaux_u a
    | Rinv ?aaux_u a
    | Rsqr ?aaux_u a
    | Rmult ?a ?aaux_u a
    | sqrt ?aaux_u a
    | cos ?aaux_u a
    | sin ?aaux_u a
    | tan ?aaux_u a
    | atan ?aaux_u a
    | exp ?aaux_u a
    | ln ?aaux_u a
    | powerRZ ?a ?b
      let b := eval lazy in b in
      lazymatch is_Z_const b with trueaux_u a end
    | pow ?a ?b
      let b := eval lazy in b in
      lazymatch is_nat_const b with trueaux_u a end
    | Rplus ?a (Ropp ?b) ⇒ aux_b a b
    | Rplus ?a ?baux_b a b
    | Rminus ?a ?baux_b a b
    | Rmult ?a (Rinv ?b) ⇒ aux_b a b
    | Rmult ?a ?baux_b a b
    | Rdiv ?a ?baux_b a b
    | Rpower ?a ?baux_b a b
    | Rnearbyint ?a ?baux_u b
    | Generic_fmt.round Zaux.radix2 (FLT.FLT_exp ?emin ?prec) ?mode ?a
      let mode := reify_round mode in
      let prec := eval lazy in prec in
      let emin := eval lazy in emin in
      lazymatch is_Z_const prec with true
      lazymatch is_Z_const emin with true
      lazymatch prec with Z.pos ?p
        aux_u a
      end end end
    | IZR (Raux.Ztrunc ?a) ⇒ aux_u a
    | IZR (Raux.Zfloor ?a) ⇒ aux_u a
    | IZR (Raux.Zceil ?a) ⇒ aux_u a
    | IZR (Round_NE.ZnearestE ?a) ⇒ aux_u a
    | PIl
    | Raux.bpow ?r ?n
      let r := eval lazy in (Zaux.radix_val r) in
      let n := eval lazy in n in
      lazymatch is_Z_const r with true
      lazymatch is_Z_const n with truel end end
    | IZR ?n
      let n := eval lazy in n in
      lazymatch is_Z_const n with truel end
    end
    | _
      let v := hyp_on_var t in
      list_add t l
    | _
      let t' := unfold_head t in
      aux t' l false
    | _
      lazymatch t with
      | _ _
        lazymatch top with
        | truelist_add t l
        end
      | _list_add t l
      end
    end in
  aux t l true.

Import Stdlib.Compatibility Rdefinitions.

Ltac reify t l :=
  let rec aux t :=
    let aux_u o a :=
      let u := aux a in
      constr:(Eunary o u) in
    let aux_b o a b :=
      let u := aux a in
      let v := aux b in
      constr:(Ebinary o u v) in
    match True with
    | True
      let n := list_find t l in
      constr:(Evar n)
    | True
    lazymatch t with
    | Ropp ?aaux_u Neg a
    | Rabs ?aaux_u Abs a
    | Rinv ?aaux_u Inv a
    | Rsqr ?aaux_u Sqr a
    | Rmult ?a ?aaux_u Sqr a
    | sqrt ?aaux_u Sqrt a
    | cos ?aaux_u Cos a
    | sin ?aaux_u Sin a
    | tan ?aaux_u Tan a
    | atan ?aaux_u Atan a
    | exp ?aaux_u Exp a
    | ln ?aaux_u Ln a
    | powerRZ ?a ?b
      let b := eval lazy in b in
      lazymatch is_Z_const b with trueaux_u (PowerInt b) a end
    | pow ?a ?b
      let b := eval lazy in (Z_of_nat b) in
      lazymatch is_Z_const b with trueaux_u (PowerInt b) a end
    | Rplus ?a (Ropp ?b) ⇒ aux_b Sub a b
    | Rplus ?a ?baux_b Add a b
    | Rminus ?a ?baux_b Sub a b
    | Rmult ?a (Rinv ?b) ⇒ aux_b Div a b
    | Q2R (QArith_base.Qmake ?a ?b) ⇒
      aux_b Div constr:(IZR a) constr:(IZR (Zpos b))
    | Rmult ?a ?baux_b Mul a b
    | Rdiv ?a ?baux_b Div a b
    | Rpower ?a ?baux (exp (b × ln a))
    | Rnearbyint ?a ?baux_u (Nearbyint a) b
    | Generic_fmt.round Zaux.radix2 (FLT.FLT_exp ?emin ?prec) ?mode ?a
      let mode := reify_round mode in
      let prec := eval lazy in prec in
      let emin := eval lazy in emin in
      lazymatch is_Z_const prec with true
      lazymatch is_Z_const emin with true
      lazymatch prec with Z.pos ?p
        aux_u (Round mode emin p) a
      end end end
    | IZR (Raux.Ztrunc ?a) ⇒ aux_u (Nearbyint rnd_ZR) a
    | IZR (Raux.Zfloor ?a) ⇒ aux_u (Nearbyint rnd_DN) a
    | IZR (Raux.Zceil ?a) ⇒ aux_u (Nearbyint rnd_UP) a
    | IZR (Round_NE.ZnearestE ?a) ⇒ aux_u (Nearbyint rnd_NE) a
    | PIconstr:(Econst Pi)
    | Raux.bpow ?r ?n
      let r := eval lazy in (Zaux.radix_val r) in
      let n := eval lazy in n in
      lazymatch is_Z_const r with true
      lazymatch is_Z_const n with true
      constr:(Econst (Bpow r n)) end end
    | IZR ?n
      let n := eval lazy in n in
      match is_Z_const n with trueconstr:(Econst (Int n)) end
    end
    | _
      let t' := unfold_head t in
      aux t'
    end in
  aux t.

Module Bnd (I : IntervalOps).

Module J := IntervalExt I.

Definition nullary_bnd prec (o : nullary_op) : I.type :=
  match o with
  | Int nI.fromZ prec n
  | Bpow r nI.power_int prec (I.fromZ prec r) n
  | PiI.pi prec
  end.

Lemma nullary_bnd_correct :
   prec o,
  contains (I.convert (nullary_bnd prec o)) (Xreal (nullary_real o)).

Definition unary_bnd prec (o : unary_op) : I.type I.type :=
  match o with
  | NegI.neg
  | AbsI.abs
  | InvI.inv prec
  | SqrI.sqr prec
  | SqrtI.sqrt prec
  | CosI.cos prec
  | SinI.sin prec
  | TanI.tan prec
  | AtanI.atan prec
  | ExpI.exp prec
  | LnI.ln prec
  | PowerInt nfun xI.power_int prec x n
  | Nearbyint mI.nearbyint m
  | Round m emin pJ.round_flt prec emin p
  end.

Lemma unary_bnd_correct :
   prec o xi x,
  contains (I.convert xi) (Xreal x)
  contains (I.convert (unary_bnd prec o xi)) (Xreal (unary_real o x)).

Definition binary_bnd prec (o : binary_op) : I.type I.type I.type :=
  match o with
  | AddI.add prec
  | SubI.sub prec
  | MulI.mul prec
  | DivI.div prec
  end.

Lemma binary_bnd_correct :
   prec o xi yi x y,
  contains (I.convert xi) (Xreal x)
  contains (I.convert yi) (Xreal y)
  contains (I.convert (binary_bnd prec o xi yi)) (Xreal (binary_real o x y)).

Fixpoint eval_bnd (prec : I.precision) (e : expr) :=
  match e with
  | Evar _I.nai
  | Econst onullary_bnd prec o
  | Eunary o e1unary_bnd prec o (eval_bnd prec e1)
  | Ebinary o e1 e2binary_bnd prec o (eval_bnd prec e1) (eval_bnd prec e2)
  end.

Theorem eval_bnd_correct :
   prec e,
  contains (I.convert (eval_bnd prec e)) (Xreal (eval e nil)).

End Bnd.