Library Interval.Eval.Prog

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 u ⇒ nth u
  | Unary o u ⇒ unary ops o (nth u)
  | Binary o u v ⇒ binary 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 x ⇒ eval_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)) →
  ∀ prog,
  ∀ 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 x ⇒ Xcmp (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)
  | nil ⇒ cons e nil
  end.

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
    | nil ⇒ cons e l
    end in
  aux l.

Fixpoint split_expr (e : expr) (lp lc : list expr) :=
  match e with
  | Evar n ⇒ Scomposed lp lc
  | Econst o ⇒ Sconst
  | Eunary o e1 ⇒
    match split_expr e1 lp lc with
    | Sconst ⇒ Sconst
    | Scomposed lp lc ⇒ Scomposed (cons_unique e lp) lc
    end
  | Ebinary o e1 e2 ⇒
    match split_expr e2 lp lc with
    | Sconst ⇒
      match split_expr e1 lp lc with
      | Sconst ⇒ Sconst
      | Scomposed lp lc ⇒ Scomposed (cons_unique e lp) (rcons_unique e2 lc)
      end
    | Scomposed lp lc ⇒
      match split_expr e1 lp lc with
      | Sconst ⇒ Scomposed (cons_unique e lp) (rcons_unique e1 lc)
      | Scomposed lp lc ⇒ Scomposed (cons_unique e lp) lc
      end
    end
  end.

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') →
  ∀ n,
  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
  | Sconst ⇒ eval e vars = eval e vars'
  | Scomposed lp' lc' ⇒
    ∀ n, eval (nth n lc' d) vars = eval (nth n lc' d) vars'
  end.

Fixpoint find_expr_aux (e : expr) (n : nat) (l : list expr) :=
  match l with
  | cons h t ⇒ if expr_beq e h then Some n else find_expr_aux e (S n) t
  | nil ⇒ None
  end.

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 n ⇒ Some n
    | None ⇒ find_expr_aux e (length lp + vars)%nat lc
    end
  end.

Theorem find_expr_correct :
  ∀ e vars lp lc,
  match find_expr e vars lp lc with
  | Some n ⇒ nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e
  | None ⇒ True
  end.

Fixpoint decompose (vars : nat) (p : list term) (lp lc : list expr) :=
  match lp with
  | nil ⇒ Some p
  | cons h t ⇒
    match find_expr h vars t lc with
    | Some n ⇒ decompose vars (cons (Forward n) p) t lc
    | None ⇒
      match h with
      | Evar n ⇒ decompose vars (cons (Forward (length t + n)) p) t lc
      | Econst _ ⇒ None
      | Eunary o e1 ⇒
        match find_expr e1 vars t lc with
        | Some n ⇒ decompose vars (cons (Unary o n) p) t lc
        | None ⇒ None
        end
      | Ebinary o e1 e2 ⇒
        match find_expr e1 vars t lc with
        | Some n1 ⇒
          match find_expr e2 vars t lc with
          | Some n2 ⇒ decompose vars (cons (Binary o n1 n2) p) t lc
          | None ⇒ None
          end
        | None ⇒ None
        end
      end
    end
  end.

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 c ⇒ eval c nil) lc in
  match decompose (length vars) p lp lc with
  | None ⇒ True
  | Some lp' ⇒
    eval_real lp' (vars ++ lc') =
    eval_real p ((map (fun c ⇒ eval c (vars ++ lc')) lp) ++ (vars ++ lc'))
  end.

Fixpoint max_arity (e : expr) (n : nat) :=
  match e with
  | Evar k ⇒ Nat.ltb k n
  | Econst _ ⇒ true
  | Eunary o e1 ⇒ max_arity e1 n
  | Ebinary o e1 e2 ⇒ if max_arity e1 n then max_arity e2 n else false
  end.

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)
    end
  end.

Fixpoint max_arity_list (le : list expr) (vars : nat) :=
  match le with
  | nil ⇒ true
  | e :: le ⇒ andb (max_arity e vars) (max_arity_list le vars)
  end.

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 p ⇒ Eprog p lc
    | None ⇒ Eabort
    end
  else Eabort.

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

Theorem extract_list_correct :
  ∀ le vars,
  match extract_list le (length vars) with
  | Eabort ⇒ True
  | Eprog lp lc ⇒ ∀ k, k < length le → eval_real_nth k lp vars lc = eval (nth k le (Econst (Int 0))) vars
  end.

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

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

Theorem extract_correct :
  ∀ e vars,
  match extract e (length vars) with
  | Eabort ⇒ True
  | Eprog lp lc ⇒ eval_real' lp vars lc = eval e vars
  end.