Require Import Le Max List Bool NPeano Omega.
Require Import Cecoa.Lib Cecoa.Syntax Cecoa.CBV_cache Cecoa.Bounds Cecoa.Ordering Cecoa.QI.

Section Main.

(* Syntax *)

Variables variable function constructor : Type.
Notation value := (Syntax.value constructor).
Notation term := (Syntax.term variable function constructor).
Notation pattern := (Syntax.pattern variable constructor).
Notation rule := (Syntax.rule variable function constructor).
Variable prog : list rule.
Variable max_arity:nat.
Variable rule_default : rule.

Hypothesis prog_is_wf: wf_prog max_arity prog.

Variable variable_eq_dec : forall (x1 x2 : variable), {x1=x2}+{x1<>x2}.
Variable function_eq_dec : forall (x1 x2 : function), {x1=x2}+{x1<>x2}.
Variable constructor_eq_dec : forall (x1 x2 : constructor), {x1=x2}+{x1<>x2}.

Notation cache := (CBV_cache.cache variable function constructor).
Notation cbv := (CBV_cache.cbv variable function constructor).
Notation wf := (CBV_cache.wf variable_eq_dec function_eq_dec constructor_eq_dec rule_default
                prog max_arity).

(* PPO *)
Variable rank: function -> nat.
Variable max_rank : nat.
Hypothesis pos_max_rank : 0 < max_rank.
Hypothesis max_rank_is_max_rank : forall f, rank f <= max_rank.
Hypothesis prog_is_ppo : PPO_prog prog rank.

Definition gsp := (Bounds.gary_seven_poly variable function constructor prog max_rank).
Definition bep := (Bounds.bobby_eight_poly variable function constructor max_arity prog).

(* QI *)
Variable cs: constructor -> nat.  (* constructor size *)
Variable mcs: nat. (* max constructor size *)
Variable qic: constructor -> list nat -> nat.
Variable qif: function -> list nat -> nat.
Hypothesis prog_has_QI: valid_QI variable function constructor prog mcs qic qif cs.
Notation cache_bounded := (QI.cache_bounded variable function constructor qic qif).

Definition CBV_bound A S C :=  (* generic bound *)
  (* A : number of activations
     S : max size of an activation 
     C : cache *)
  (A * activation_bound prog S + A + 1 + (max_arity * A * (1 + activation_bound prog S))) *
  (activation_bound prog S + S + cache_size C +
  (1 + max S (maxl (map (fun tv : term * value => value_size (snd tv)) C))) *
  (1 + (A * activation_bound prog S + A) + max_arity * (A * activation_bound prog S + A))) +
  cache_size C.

Definition PPO_bound S := gsp (bep S).
(* S : max size of an activation *)

Definition QI_bound (f:function) (lv: list term) := 
  (* f : active function symbol
     lv : list of its arguments *)
  (max_arity + 1) * (qif f (map (fun x=> mcs * (term_size (fapply f lv))) lv)) + 1.

Definition global_bound f lv C :=
  let S:= QI_bound f lv in
  let A:= PPO_bound S in
  CBV_bound A S C.

(********** Proofs **********)

(* All bounds are increasing *)
Lemma gary_increase: (* move to Ordering ? *)
  forall x y, x <=y -> gsp x <= gsp y.
Proof.
(* Goal: forall (x1 y1 x2 y2 : nat) (C : CBV_cache.cache variable function constructor) (_ : le x1 y1) (_ : le x2 y2), le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
intros.
(* Goal: le (gsp x) (gsp y) *)
unfold gary_seven_poly.
(* Goal: le (gsp x) (gsp y) *)
apply suml_map_le.
(* Goal: forall (x1 y1 x2 y2 : nat) (C : CBV_cache.cache variable function constructor) (_ : le x1 y1) (_ : le x2 y2), le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
intros.
(* Goal: le (activations_at_rank_bound variable function constructor prog max_rank x x0) (activations_at_rank_bound variable function constructor prog max_rank y x0) *)
unfold activations_at_rank_bound.
(* Goal: le (Init.Nat.mul (@max_rhs variable function constructor prog) (Init.Nat.add (S O) x)) (Init.Nat.mul (@max_rhs variable function constructor prog) (Init.Nat.add (S O) y)) *)
apply Mult.mult_le_compat_l.
(* Goal: le (Nat.pow x (S (Init.Nat.sub max_rank x0))) (Nat.pow y (S (Init.Nat.sub max_rank x0))) *)
apply pow_le_compat;trivial.
Qed.

Lemma PPO_bound_increase:
  forall x y, x <= y -> PPO_bound x <= PPO_bound y.
Proof.
(* Goal: forall (x1 y1 x2 y2 : nat) (C : CBV_cache.cache variable function constructor) (_ : le x1 y1) (_ : le x2 y2), le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
intros.
(* Goal: le (gsp (A_T variable function constructor rank pi)) (PPO_bound (@max_active_size variable function constructor pi)) *)
unfold PPO_bound.
(* Goal: le (gsp (A_T variable function constructor rank pi)) (gsp (bep (@max_active_size variable function constructor pi))) *)
apply gary_increase.
(* Goal: le (bep x) (bep y) *)
apply bobby_increase.
(* Goal: le x y *)
trivial.
Qed.

Lemma activation_bound_increase:
  forall x y, x <= y -> activation_bound prog x <= activation_bound prog y.
Proof.
(* Goal: forall (x1 y1 x2 y2 : nat) (C : CBV_cache.cache variable function constructor) (_ : le x1 y1) (_ : le x2 y2), le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
intros.
(* Goal: le (@activation_bound variable function constructor prog x) (@activation_bound variable function constructor prog y) *)
unfold activation_bound.
(* Goal: le (Init.Nat.mul (@max_rhs variable function constructor prog) (Init.Nat.add (S O) x)) (Init.Nat.mul (@max_rhs variable function constructor prog) (Init.Nat.add (S O) y)) *)
apply Mult.mult_le_compat_l.
(* Goal: le x y *)
apply Plus.plus_le_compat_l;trivial.
Qed.

Lemma CBV_bound_increase:
  forall x1 y1 x2 y2 C, x1 <= y1 -> x2 <= y2 -> CBV_bound x1 x2 C <= CBV_bound y1 y2 C.
Proof.
(* Goal: forall (x1 y1 x2 y2 : nat) (C : CBV_cache.cache variable function constructor) (_ : le x1 y1) (_ : le x2 y2), le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
intros.
(* Goal: le (CBV_bound x1 x2 C) (CBV_bound y1 y2 C) *)
unfold CBV_bound.
(* Goal: le (Init.Nat.add (Init.Nat.mul (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul x1 (@activation_bound variable function constructor prog x2)) x1) (S O)) (Init.Nat.mul (Init.Nat.mul max_arity x1) (Init.Nat.add (S O) (@activation_bound variable function constructor prog x2)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (@activation_bound variable function constructor prog x2) x2) (@cache_size variable function constructor C)) (Init.Nat.mul (Init.Nat.add (S O) (Nat.max x2 (maxl (@map (prod (Syntax.term variable function constructor) (Syntax.value constructor)) nat (fun tv : prod (Syntax.term variable function constructor) (Syntax.value constructor) => @value_size constructor (@snd (Syntax.term variable function constructor) (Syntax.value constructor) tv)) C)))) (Init.Nat.add (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.mul x1 (@activation_bound variable function constructor prog x2)) x1)) (Init.Nat.mul max_arity (Init.Nat.add (Init.Nat.mul x1 (@activation_bound variable function constructor prog x2)) x1)))))) (@cache_size variable function constructor C)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul y1 (@activation_bound variable function constructor prog y2)) y1) (S O)) (Init.Nat.mul (Init.Nat.mul max_arity y1) (Init.Nat.add (S O) (@activation_bound variable function constructor prog y2)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (@activation_bound variable function constructor prog y2) y2) (@cache_size variable function constructor C)) (Init.Nat.mul (Init.Nat.add (S O) (Nat.max y2 (maxl (@map (prod (Syntax.term variable function constructor) (Syntax.value constructor)) nat (fun tv : prod (Syntax.term variable function constructor) (Syntax.value constructor) => @value_size constructor (@snd (Syntax.term variable function constructor) (Syntax.value constructor) tv)) C)))) (Init.Nat.add (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.mul y1 (@activation_bound variable function constructor prog y2)) y1)) (Init.Nat.mul max_arity (Init.Nat.add (Init.Nat.mul y1 (@activation_bound variable function constructor prog y2)) y1)))))) (@cache_size variable function constructor C)) *)
apply Plus.plus_le_compat_r.
apply Mult.mult_le_compat;
repeat (try apply Plus.plus_le_compat; trivial; try apply Mult.mult_le_compat; trivial).
(* Goal: le x y *)
apply Nat.max_le_compat_r;trivial.
Qed.

Theorem P_criterion: forall i s p c f lv d v,
  let t :=  (fapply f lv) in
  let pi := cbv_update i s p c t d v in
  wf pi -> cache_bounded c ->
  size pi <= global_bound f lv c.
Proof.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c : CBV_cache.cache variable function constructor) (f : function) (lv : list (Syntax.term variable function constructor)) (d : CBV_cache.cache variable function constructor) (v : Syntax.value constructor), let t := @fapply variable function constructor f lv in let pi := @cbv_update variable function constructor i s p c t d v in forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi) (_ : QI.cache_bounded variable function constructor qic qif c), le (@size variable function constructor pi) (global_bound f lv c) *)
intros i s p c f lv d v t pi well_formed cache_bound.
(* Goal: le (@size variable function constructor pi) (global_bound f lv c) *)
unfold global_bound.
(* Goal: le (@size variable function constructor pi) (CBV_bound (PPO_bound (QI_bound f lv)) (QI_bound f lv) c) *)
assert (max_active_size pi <= QI_bound f lv).
- apply max_active_size_bound with (prog:=prog) (rule_default:=rule_default)
        (variable_eq_dec:=variable_eq_dec) (function_eq_dec :=function_eq_dec) (constructor_eq_dec:=constructor_eq_dec)
(* Goal: le x y *)
        (qic:=qic) (cs:=cs);trivial.
- apply le_trans with (m:= CBV_bound (PPO_bound (max_active_size pi)) (max_active_size pi) c).
  + assert (length (activations pi) <= PPO_bound (max_active_size pi)).
    * { 
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi)) (PPO_bound (@max_active_size variable function constructor pi)) *)
        apply le_trans with (m:=gsp (A_T variable function constructor rank pi)).
        - apply gary_seven with (variable_eq_dec:=variable_eq_dec) (function_eq_dec:=function_eq_dec) 
                                (constructor_eq_dec:=constructor_eq_dec) (rule_default:=rule_default)
(* Goal: le x y *)
                                (max_arity:=max_arity);try trivial.
(* Goal: le x y *)
          apply PPO_is_compatible_prog;trivial.
(* Goal: le (gsp (A_T variable function constructor rank pi)) (PPO_bound (@max_active_size variable function constructor pi)) *)
        - unfold PPO_bound.
(* Goal: le (gsp (A_T variable function constructor rank pi)) (gsp (bep (@max_active_size variable function constructor pi))) *)
          apply gary_increase.
          apply A_T_bound with (variable_eq_dec:=variable_eq_dec) (function_eq_dec:=function_eq_dec) 
                               (constructor_eq_dec:=constructor_eq_dec) (rule_default:=rule_default)
(* Goal: le x y *)
                               (max_rank:=max_rank);trivial.
      }
    * {
(* Goal: le (@size variable function constructor pi) (CBV_bound (PPO_bound (@max_active_size variable function constructor pi)) (@max_active_size variable function constructor pi) c) *)
        apply le_trans with (m:=CBV_bound (length (activations pi)) (max_active_size pi) c).
        - apply size_bound_gen with (variable_eq_dec:=variable_eq_dec) (function_eq_dec:=function_eq_dec) 
(* Goal: le x y *)
                                    (constructor_eq_dec:=constructor_eq_dec) (rule_default:=rule_default);trivial.
(* Goal: le x y *)
        - apply CBV_bound_increase;trivial.
      }
(* Goal: le x y *)
  + apply CBV_bound_increase;try trivial.
(* Goal: le x y *)
    apply PPO_bound_increase;try trivial.
Qed.

End Main.
