Require Import List Omega.
Import List.ListNotations.

Require Import Cecoa.Interface.
Require Import Cecoa.Lib.

Inductive variable := x | y.
Inductive function := plus | main | errF.
Inductive constructor := zero | succ | errC.

Scheme Equality for variable.
Scheme Equality for function.
Scheme Equality for constructor.

Module PlusSyntax <: Interface.SYNTAX.
  Definition variable := variable.
  Definition function := function.
  Definition constructor := constructor.

  Definition function_default := errF.
  Definition constructor_default := errC.

  Definition variable_eq_dec := variable_eq_dec.
  Definition function_eq_dec := function_eq_dec.
  Definition constructor_eq_dec := constructor_eq_dec.
End PlusSyntax.

Module Import Syn := Interface.MkSyn(PlusSyntax).
Import Syn.ProgramNotations.

Definition var_coercion : variable -> term := var_coercion_gen.
Coercion var_coercion : variable >-> term.

Notation " 'Z' " := (capply zero []).
Notation " x '.+1' " := (capply succ [x:term]) (at level 60).

Definition plus_prog : list rule :=
  [
    main (: x, y :)    --> plus (: plus (: x, y :), plus (: x, y :) :) ;

    plus (: Z, y :)    --> y ;
    plus (: x.+1, y :) --> (plus (: x, y :)) .+1
  ].

Module PlusProg <: Syn.PROGRAM.
  Definition prog := plus_prog.
End PlusProg.

Module Import Prog := Syn.MkProg (PlusProg).
Import Prog.QI Prog.Evaluator.
Definition rank : function -> nat := ltac:(autorank function_beq ranklist).

Fixpoint quote_value (n : nat) : value :=
  match n with
  | 0    => c_capply zero []
  | S n' => c_capply succ [quote_value n']
  end.

(* It's a program *)
Proposition UnaryAdd_is_wf: wf_prog.
Proof.
(* Goal: wf_prog *)
  cbv; repeat split; tauto.
Qed.

(* PPO *)
Proposition UnaryAdd_is_ppo : PPO_prog rank.
Proof.
(* Goal: PPO_prog rank *)
  cbv.
(* Goal: forall (r : Syntax.rule variable function constructor) (_ : or (@eq (Syntax.rule variable function constructor) (@Syntax.rule_intro variable function constructor main (@cons (Syntax.pattern variable constructor) (@Syntax.p_var variable constructor x) (@cons (Syntax.pattern variable constructor) (@Syntax.p_var variable constructor y) (@nil (Syntax.pattern variable constructor)))) (@Syntax.fapply variable function constructor plus (@cons (Syntax.term variable function constructor) (@Syntax.fapply variable function constructor plus (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor x) (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor y) (@nil (Syntax.term variable function constructor))))) (@cons (Syntax.term variable function constructor) (@Syntax.fapply variable function constructor plus (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor x) (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor y) (@nil (Syntax.term variable function constructor))))) (@nil (Syntax.term variable function constructor)))))) r) (or (@eq (Syntax.rule variable function constructor) (@Syntax.rule_intro variable function constructor plus (@cons (Syntax.pattern variable constructor) (@Syntax.p_capply variable constructor zero (@nil (Syntax.pattern variable constructor))) (@cons (Syntax.pattern variable constructor) (@Syntax.p_var variable constructor y) (@nil (Syntax.pattern variable constructor)))) (@Syntax.var variable function constructor y)) r) (or (@eq (Syntax.rule variable function constructor) (@Syntax.rule_intro variable function constructor plus (@cons (Syntax.pattern variable constructor) (@Syntax.p_capply variable constructor succ (@cons (Syntax.pattern variable constructor) (@Syntax.p_var variable constructor x) (@nil (Syntax.pattern variable constructor)))) (@cons (Syntax.pattern variable constructor) (@Syntax.p_var variable constructor y) (@nil (Syntax.pattern variable constructor)))) (@Syntax.capply variable function constructor succ (@cons (Syntax.term variable function constructor) (@Syntax.fapply variable function constructor plus (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor x) (@cons (Syntax.term variable function constructor) (@Syntax.var variable function constructor y) (@nil (Syntax.term variable function constructor))))) (@nil (Syntax.term variable function constructor))))) r) False))), match r with | Syntax.rule_intro f lp t => @Ordering.PPO variable function constructor (fun f0 : function => match f0 with | plus => O | main => S O | errF => O end) t (@Syntax.fapply variable function constructor f ((fix map (l : list (Syntax.pattern variable constructor)) : list (Syntax.term variable function constructor) := match l with | nil => @nil (Syntax.term variable function constructor) | cons a t0 => @cons (Syntax.term variable function constructor) ((fix term_from_pattern (p : Syntax.pattern variable constructor) : Syntax.term variable function constructor := match p with | Syntax.p_var v => @Syntax.var variable function constructor v | Syntax.p_capply c lp0 => @Syntax.capply variable function constructor c ((fix map0 (l0 : list (Syntax.pattern variable constructor)) : list (Syntax.term variable function constructor) := match l0 with | nil => @nil (Syntax.term variable function constructor) | cons a0 t1 => @cons (Syntax.term variable function constructor) (term_from_pattern a0) (map0 t1) end) lp0) end) a) (map t0) end) lp)) end *)
  intros r H.
(* Goal: match r with | Syntax.rule_intro f lp t => @Ordering.PPO variable function constructor (fun f0 : function => match f0 with | plus => O | main => S O | errF => O end) t (@Syntax.fapply variable function constructor f ((fix map (l : list (Syntax.pattern variable constructor)) : list (Syntax.term variable function constructor) := match l with | nil => @nil (Syntax.term variable function constructor) | cons a t0 => @cons (Syntax.term variable function constructor) ((fix term_from_pattern (p : Syntax.pattern variable constructor) : Syntax.term variable function constructor := match p with | Syntax.p_var v => @Syntax.var variable function constructor v | Syntax.p_capply c lp0 => @Syntax.capply variable function constructor c ((fix map0 (l0 : list (Syntax.pattern variable constructor)) : list (Syntax.term variable function constructor) := match l0 with | nil => @nil (Syntax.term variable function constructor) | cons a0 t1 => @cons (Syntax.term variable function constructor) (term_from_pattern a0) (map0 t1) end) lp0) end) a) (map t0) end) lp)) end *)
  decompose sum H; subst; ppo.
Qed.

(* QI *)
Definition cs (c : constructor) := 1. (* same for all *)
Lemma qic_nonzero : constructor_non_zero cs.
Proof. cbv; auto. Qed.

Definition mcs := 1.
Lemma qic_bounded : mcs_is_max_constructor_size mcs cs.
Proof. cbv; auto. Qed.

Definition qic (c : constructor) args := suml args + cs c.
Lemma qic_additivity : additive qic cs.
Proof. cbv; auto. Qed.

Definition qif (f : function) args := match f with
  | main => 2*(suml args)
  | plus => suml args
  | errF => suml args
  end.

Lemma qif_subterm : subterm qif.
Proof.
(* Goal: subterm qif *)
  intros f l x H.
(* Goal: le x (qif f l) *)
  destruct f; unfold qif.
  - apply in_le_suml; trivial.
  - apply le_trans with (m:= suml l).
(* Goal: le x (suml l) *)
    + apply in_le_suml; trivial.
    + omega.
  - apply in_le_suml; trivial.
Qed.

Lemma qif_monotonic : monotonicity_qif qif.
Proof.
(* Goal: monotonicity_qif qif *)
  intros f xs ys Hfor.
(* Goal: le (qif f xs) (qif f ys) *)
  destruct f; unfold qif; try apply Mult.mult_le_compat_l; apply forall2_le_suml; trivial.
Qed.

Lemma qi_is_compatible : compatible_QI qic qif.
Proof.
(* Goal: compatible_QI qic qif *)
  intros f lp t s; cbn.
  intros [ H | [ H | [ H | H ]]];
    try tauto;
    injection H; clear H; intros; subst; trivial; cbn;
(* Goal: le (suml l) (Init.Nat.mul (S (S O)) (suml l)) *)
    omega.
Qed.

Proposition qi_is_valid : valid_QI mcs qic qif cs.
Proof.
(* Goal: valid_QI mcs qic qif cs *)
  repeat split.
(* Goal: Cecoa.QI.mcs_is_max_constructor_size PlusSyntax.constructor mcs cs *)
(* Goal: Cecoa.QI.constructor_non_zero PlusSyntax.constructor cs *)
(* Goal: Cecoa.QI.subterm PlusSyntax.function qif *)
(* Goal: Cecoa.QI.monotonicity_qif PlusSyntax.function qif *)
(* Goal: Cecoa.QI.compatible_QI PlusSyntax.variable PlusSyntax.function PlusSyntax.constructor PlusProg.prog qic qif *)
  apply qic_bounded.
(* Goal: Cecoa.QI.constructor_non_zero PlusSyntax.constructor cs *)
(* Goal: Cecoa.QI.subterm PlusSyntax.function qif *)
(* Goal: Cecoa.QI.monotonicity_qif PlusSyntax.function qif *)
(* Goal: Cecoa.QI.compatible_QI PlusSyntax.variable PlusSyntax.function PlusSyntax.constructor PlusProg.prog qic qif *)
  apply qic_nonzero.
(* Goal: Cecoa.QI.subterm PlusSyntax.function qif *)
(* Goal: Cecoa.QI.monotonicity_qif PlusSyntax.function qif *)
(* Goal: Cecoa.QI.compatible_QI PlusSyntax.variable PlusSyntax.function PlusSyntax.constructor PlusProg.prog qic qif *)
  apply qif_subterm.
(* Goal: Cecoa.QI.monotonicity_qif PlusSyntax.function qif *)
(* Goal: Cecoa.QI.compatible_QI PlusSyntax.variable PlusSyntax.function PlusSyntax.constructor PlusProg.prog qic qif *)
  apply qif_monotonic.
(* Goal: Cecoa.QI.compatible_QI PlusSyntax.variable PlusSyntax.function PlusSyntax.constructor PlusProg.prog qic qif *)
  apply qi_is_compatible.
Qed.

(* P-criterion *)
Theorem plus_polytime: 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
  cbv_wf pi -> cache_bounded qic qif c ->
  cbv_size pi <= global_bound mcs qif f lv c.
Proof.
(* Goal: forall (i : nat) (s : forall _ : PlusSyntax.variable, value) (p : cbv) (c : cache) (f : PlusSyntax.function) (lv : list term) (d : cache) (v : value), let t := fapply f lv in let pi := cbv_update i s p c t d v in forall (_ : cbv_wf pi) (_ : cache_bounded qic qif c), le (cbv_size pi) (global_bound mcs qif f lv c) *)
  intros.
(* Goal: le (cbv_size pi) (global_bound mcs qif f lv c) *)
  apply P_criterion with (rank:=rank) (cs:=cs) (qic:=qic);auto.
  - split; [ apply UnaryAdd_is_wf | trivial ].
  - intro g; destruct g; auto; simpl; apply le_0_n.
  - apply UnaryAdd_is_ppo.
  - apply qi_is_valid.
Qed.

Definition value_default := quote_value 0.

Theorem plus_correct n m : 
  evaluates (fapply plus [term_from_value(quote_value n); term_from_value(quote_value m)]) (quote_value(n+m)).
Proof.
(* Goal: evaluates (fapply plus (@cons term (term_from_value (quote_value n)) (@cons term (term_from_value (quote_value m)) (@nil term)))) (quote_value (Init.Nat.add n m)) *)
  revert m.
(* Goal: forall m : nat, evaluates (fapply plus (@cons term (term_from_value (quote_value n)) (@cons term (term_from_value (quote_value m)) (@nil term)))) (quote_value (Init.Nat.add n m)) *)
  induction n as [| n IH]; cbn; intro m.
  - reduce.
  - reduce. cbn. apply IH.
Qed.
