Library Interval.Eval.Prog

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq:
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:
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 ZArith Reals List Psatz.

Require Import Xreal.
Require Import Tree.

Inductive term : Set :=
  | Forward : nat term
  | Unary : unary_op nat term
  | Binary : binary_op nat nat term.

Set Implicit Arguments.

Record operations (A : Type) : Type :=
  { constant : Z A
  ; unary : unary_op A A
  ; binary : binary_op A A A
  ; sign : A Xcomparison }.

Unset Implicit Arguments.

Definition eval_generic_body {A} def (ops : operations A) values op :=
  let nth n := nth n values def in
  match op with
  | Forward unth u
  | Unary o uunary ops o (nth u)
  | Binary o u vbinary ops o (nth u) (nth v)
  end :: values.

Definition eval_generic {A} def (ops : operations A) :=
  fold_left (eval_generic_body def ops).

Lemma rev_formula :
   A formula terms def (ops : operations A),
  eval_generic def ops formula terms =
  fold_right (fun y xeval_generic_body def ops x y) terms (rev formula).

Theorem eval_inductive_prop :
   A B (P : A B Prop) defA defB (opsA : operations A) (opsB : operations B),
  P defA defB
 ( o a b, P a b P (unary opsA o a) (unary opsB o b))
 ( o a1 a2 b1 b2, P a1 b1 P a2 b2 P (binary opsA o a1 a2) (binary opsB o b1 b2))
   inpA inpB,
 ( n, P (nth n inpA defA) (nth n inpB defB))
   n, P (nth n (eval_generic defA opsA prog inpA) defA) (nth n (eval_generic defB opsB prog inpB) defB).

Definition real_operations :=
  Build_operations IZR
   unary_real binary_real
   (fun xXcmp (Xreal x) (Xreal 0)).

Definition eval_real :=
  eval_generic 0%R real_operations.

Scheme Equality for expr.

Inductive splitted_expr : Set :=
  | Sconst
  | Scomposed (lp lc : list expr).

Fixpoint rcons_unique (e : expr) (l : list expr) :=
  match l with
  | cons h t
    if expr_beq e h then l else cons h (rcons_unique e t)
  | nilcons e nil

Lemma rcons_unique_correct : e l, l',
  rcons_unique e l = l ++ l'.

Definition cons_unique (e : expr) (l : list expr) :=
  let fix aux (l' : list expr) :=
    match l' with
    | cons h t
      if expr_beq e h then l else aux t
    | nilcons e l
    end in
  aux l.

Fixpoint split_expr (e : expr) (lp lc : list expr) :=
  match e with
  | Evar nScomposed lp lc
  | Econst oSconst
  | Eunary o e1
    match split_expr e1 lp lc with
    | SconstSconst
    | Scomposed lp lcScomposed (cons_unique e lp) lc
  | Ebinary o e1 e2
    match split_expr e2 lp lc with
    | Sconst
      match split_expr e1 lp lc with
      | SconstSconst
      | Scomposed lp lcScomposed (cons_unique e lp) (rcons_unique e2 lc)
    | Scomposed lp lc
      match split_expr e1 lp lc with
      | SconstScomposed (cons_unique e lp) (rcons_unique e1 lc)
      | Scomposed lp lcScomposed (cons_unique e lp) lc

Lemma eval_nth_rcons_unique :
   d vars vars' e l,
  eval e vars = eval e vars'
  ( n, eval (nth n l d) vars = eval (nth n l d) vars')
  eval (nth n (rcons_unique e l) d) vars = eval (nth n (rcons_unique e l) d) vars'.

Theorem split_expr_correct :
   d vars vars' e lp lc,
  ( n, eval (nth n lc d) vars = eval (nth n lc d) vars')
  match split_expr e lp lc with
  | Sconsteval e vars = eval e vars'
  | Scomposed lp' lc'
     n, eval (nth n lc' d) vars = eval (nth n lc' d) vars'

Fixpoint find_expr_aux (e : expr) (n : nat) (l : list expr) :=
  match l with
  | cons h tif expr_beq e h then Some n else find_expr_aux e (S n) t
  | nilNone

Definition find_expr (e : expr) (vars : nat) (lp lc : list expr) :=
  match e with
  | Evar n
    if Nat.ltb n vars then Some (List.length lp + n)%nat else None
  | _
    match find_expr_aux e 0%nat lp with
    | Some nSome n
    | Nonefind_expr_aux e (length lp + vars)%nat lc

Theorem find_expr_correct :
   e vars lp lc,
  match find_expr e vars lp lc with
  | Some nnth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e
  | NoneTrue

Fixpoint decompose (vars : nat) (p : list term) (lp lc : list expr) :=
  match lp with
  | nilSome p
  | cons h t
    match find_expr h vars t lc with
    | Some ndecompose vars (cons (Forward n) p) t lc
    | None
      match h with
      | Evar ndecompose vars (cons (Forward (length t + n)) p) t lc
      | Econst _None
      | Eunary o e1
        match find_expr e1 vars t lc with
        | Some ndecompose vars (cons (Unary o n) p) t lc
        | NoneNone
      | Ebinary o e1 e2
        match find_expr e1 vars t lc with
        | Some n1
          match find_expr e2 vars t lc with
          | Some n2decompose vars (cons (Binary o n1 n2) p) t lc
          | NoneNone
        | NoneNone

Theorem decompose_correct :
   vars p lp lc,
  ( vars n, eval (nth n lc (Econst (Int 0))) vars = eval (nth n lc (Econst (Int 0))) nil)
  let lc' := map (fun ceval c nil) lc in
  match decompose (length vars) p lp lc with
  | NoneTrue
  | Some lp'
    eval_real lp' (vars ++ lc') =
    eval_real p ((map (fun ceval c (vars ++ lc')) lp) ++ (vars ++ lc'))

Fixpoint max_arity (e : expr) (n : nat) :=
  match e with
  | Evar kNat.ltb k n
  | Econst _true
  | Eunary o e1max_arity e1 n
  | Ebinary o e1 e2if max_arity e1 n then max_arity e2 n else false

Lemma max_arity_correct :
   e vars v,
  max_arity e (length vars) = true
  eval e (vars ++ v) = eval e vars.

Inductive extracted_expr : Set :=
  | Eabort
  | Eprog (lp : list term) (lc : list expr).

Fixpoint fold_split (le lp lc : list expr) :=
  match le with
  | nil(lp, lc)
  | e :: le
    let (lp, lc) := fold_split le lp lc in
    match split_expr e lp lc with
    | Sconst(lp, (rcons_unique e lc))
    | Scomposed lp lc(lp, lc)

Fixpoint max_arity_list (le : list expr) (vars : nat) :=
  match le with
  | niltrue
  | e :: leandb (max_arity e vars) (max_arity_list le vars)

Lemma max_arity_nth :
   le vars k d,
  max_arity_list le vars = true
  k < length le
  max_arity (nth k le d) vars = true.

Definition extract_list (le : list expr) (vars : nat) :=
  if max_arity_list le vars then
    let (lp, lc) := fold_split le nil nil in
    let lp' := le ++ lp in
    match decompose vars nil lp' lc with
    | Some pEprog p lc
    | NoneEabort
  else Eabort.

Definition eval_real_nth k prog vars consts :=
  nth k (eval_real prog (vars ++ map (fun ceval c nil) consts)) 0%R.

Theorem extract_list_correct :
   le vars,
  match extract_list le (length vars) with
  | EabortTrue
  | Eprog lp lc k, k < length le eval_real_nth k lp vars lc = eval (nth k le (Econst (Int 0))) vars

Definition extract e vars := extract_list (e :: nil) vars.

Definition eval_real' prog vars consts :=
  nth O (eval_real prog (vars ++ map (fun ceval c nil) consts)) 0%R.

Theorem extract_correct :
   e vars,
  match extract e (length vars) with
  | EabortTrue
  | Eprog lp lceval_real' lp vars lc = eval e vars