Require Import Bool PArith DecidableClass Ring Omega Lia.

Ltac bool :=
repeat match goal with
| [ H : ?P && ?Q = true |- _ ] =>
  apply andb_true_iff in H; destruct H
| |- ?P && ?Q = true =>
  apply <- andb_true_iff; split
end.


Hint Extern 5 => progress bool : core.

Ltac define t x H :=
set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.

Lemma Decidable_sound : forall P (H : Decidable P),
                          decide P = true -> P.

Lemma Decidable_complete : forall P (H : Decidable P),
  P -> decide P = true.

Lemma Decidable_sound_alt : forall P (H : Decidable P),
   ~ P -> decide P = false.

Lemma Decidable_complete_alt : forall P (H : Decidable P),
  decide P = false -> ~ P.

Ltac try_rewrite :=
repeat match goal with
| [ H : ?P |- _ ] => rewrite H
end.


Global Opaque decide.

Ltac tac_decide :=
match goal with
| [ H : @decide ?P ?D = true |- _ ] => apply (@Decidable_sound P D) in H
| [ H : @decide ?P ?D = false |- _ ] => apply (@Decidable_complete_alt P D) in H
| [ |- @decide ?P ?D = true ] => apply (@Decidable_complete P D)
| [ |- @decide ?P ?D = false ] => apply (@Decidable_sound_alt P D)
| [ |- negb ?b = true ] => apply negb_true_iff
| [ |- negb ?b = false ] => apply negb_false_iff
| [ H : negb ?b = true |- _ ] => apply negb_true_iff in H
| [ H : negb ?b = false |- _ ] => apply negb_false_iff in H
end.

Ltac try_decide := repeat tac_decide.

Ltac make_decide P := match goal with
| [ |- context [@decide P ?D] ] =>
  let b := fresh "b" in
  let H := fresh "H" in
  define (@decide P D) b H; destruct b; try_decide
| [ X : context [@decide P ?D] |- _ ] =>
  let b := fresh "b" in
  let H := fresh "H" in
  define (@decide P D) b H; destruct b; try_decide
end.

Ltac case_decide := match goal with
| [ |- context [@decide ?P ?D] ] =>
  let b := fresh "b" in
  let H := fresh "H" in
  define (@decide P D) b H; destruct b; try_decide
| [ X : context [@decide ?P ?D] |- _ ] =>
  let b := fresh "b" in
  let H := fresh "H" in
  define (@decide P D) b H; destruct b; try_decide
| [ |- context [Pos.compare ?x ?y] ] =>
  destruct (Pos.compare_spec x y); try lia
| [ X : context [Pos.compare ?x ?y] |- _ ] =>
  destruct (Pos.compare_spec x y); try lia
end.

Section Definitions.

Inductive poly :=
| Cst : bool -> poly
| Poly : poly -> positive -> poly -> poly.


Inductive null : poly -> Prop :=
| null_intro : null (Cst false).

Inductive valid : positive -> poly -> Prop :=
| valid_cst : forall k c, valid k (Cst c)
| valid_poly : forall k p i q,
  Pos.lt i k -> ~ null q -> valid i p -> valid (Pos.succ i) q -> valid k (Poly p i q).

Inductive linear : positive -> poly -> Prop :=
| linear_cst : forall k c, linear k (Cst c)
| linear_poly : forall k p i q, Pos.lt i k -> ~ null q ->
  linear i p -> linear i q -> linear k (Poly p i q).

End Definitions.

Section Computational.

Program Instance Decidable_PosEq : forall (p q : positive), Decidable (p = q) :=
  { Decidable_witness := Pos.eqb p q }.

Program Instance Decidable_PosLt : forall p q, Decidable (Pos.lt p q) :=
  { Decidable_witness := Pos.ltb p q }.

Program Instance Decidable_PosLe : forall p q, Decidable (Pos.le p q) :=
  { Decidable_witness := Pos.leb p q }.

Hint Constructors valid : core.

Fixpoint beq_poly pl pr :=
match pl with
| Cst cl =>
  match pr with
  | Cst cr => decide (cl = cr)
  | Poly _ _ _ => false
  end
| Poly pl il ql =>
  match pr with
  | Cst _ => false
  | Poly pr ir qr =>
    decide (il = ir) && beq_poly pl pr && beq_poly ql qr
  end
end.

Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := {
  Decidable_witness := beq_poly p q
}.


Program Instance Decidable_null : forall p, Decidable (null p) := {
  Decidable_witness := match p with Cst false => true | _ => false end
}.

Definition list_nth {A} p (l : list A) def :=
  Pos.peano_rect (fun _ => list A -> A)
    (fun l => match l with nil => def | cons t l => t end)
    (fun _ F l => match l with nil => def | cons t l => F l end) p l.

Fixpoint eval var (p : poly) :=
match p with
| Cst c => c
| Poly p i q =>
  let vi := list_nth i var false in
  xorb (eval var p) (andb vi (eval var q))
end.

Fixpoint valid_dec k p :=
match p with
| Cst c => true
| Poly p i q =>
  negb (decide (null q)) && decide (i < k)%positive &&
    valid_dec i p && valid_dec (Pos.succ i) q
end.

Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
  Decidable_witness := valid_dec n p
}.

Fixpoint poly_add pl {struct pl} :=
match pl with
| Cst cl =>
  fix F pr := match pr with
  | Cst cr => Cst (xorb cl cr)
  | Poly pr ir qr => Poly (F pr) ir qr
  end
| Poly pl il ql =>
  fix F pr {struct pr} := match pr with
  | Cst cr => Poly (poly_add pl pr) il ql
  | Poly pr ir qr =>
    match Pos.compare il ir with
    | Eq =>
      let qs := poly_add ql qr in
      
      if decide (null qs) then poly_add pl pr
      else Poly (poly_add pl pr) il qs
    | Gt => Poly (poly_add pl (Poly pr ir qr)) il ql
    | Lt => Poly (F pr) ir qr
    end
  end
end.


Fixpoint poly_mul_cst v p :=
match p with
| Cst c => Cst (andb c v)
| Poly p i q =>
  let r := poly_mul_cst v q in
  
  if decide (null r) then poly_mul_cst v p
  else Poly (poly_mul_cst v p) i r
end.


Fixpoint poly_mul_mon k p :=
match p with
| Cst c =>
  if decide (null p) then p
  else Poly (Cst false) k p
| Poly p i q =>
  if decide (i <= k)%positive then Poly (Cst false) k (Poly p i q)
  else Poly (poly_mul_mon k p) i (poly_mul_mon k q)
end.


Fixpoint poly_mul pl {struct pl} :=
match pl with
| Cst cl => poly_mul_cst cl
| Poly pl il ql =>
  fun pr =>
    
    let qs := poly_mul ql pr in
    
    if decide (null qs) then poly_mul pl pr
    else poly_add (poly_mul pl pr) (poly_mul_mon il qs)
end.

Fixpoint reduce_aux k p :=
match p with
| Cst c => Cst c
| Poly p i q =>
  if decide (i = k) then poly_add (reduce_aux k p) (reduce_aux k q)
  else
    let qs := reduce_aux i q in
    
    if decide (null qs) then (reduce_aux k p)
    else Poly (reduce_aux k p) i qs
end.


Fixpoint reduce p :=
match p with
| Cst c => Cst c
| Poly p i q =>
  let qs := reduce_aux i q in
  
  if decide (null qs) then reduce p
  else Poly (reduce p) i qs
end.

End Computational.

Section Validity.


Hint Constructors valid linear : core.

Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.

Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p.

Lemma linear_valid_incl : forall k p, linear k p -> valid k p.

End Validity.

Section Evaluation.


Lemma eval_null_zero : forall p var, null p -> eval var p = false.

Lemma eval_extensional_eq_compat : forall p var1 var2,
  (forall x, list_nth x var1 false = list_nth x var2 false) -> eval var1 p = eval var2 p.

Lemma eval_suffix_compat : forall k p var1 var2,
  (forall i, (i < k)%positive -> list_nth i var1 false = list_nth i var2 false) -> valid k p ->
  eval var1 p = eval var2 p.

End Evaluation.

Section Algebra.


Lemma poly_add_compat : forall pl pr var, eval var (poly_add pl pr) = xorb (eval var pl) (eval var pr).

Lemma poly_mul_cst_compat : forall v p var,
  eval var (poly_mul_cst v p) = andb v (eval var p).

Lemma poly_mul_mon_compat : forall i p var,
  eval var (poly_mul_mon i p) = (list_nth i var false && eval var p).

Lemma poly_mul_compat : forall pl pr var, eval var (poly_mul pl pr) = andb (eval var pl) (eval var pr).

Hint Extern 5 =>
match goal with
| [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
  apply Pos.max_case_strong; intros; lia
| [ |- (?z <= Pos.max ?x ?y)%positive ] =>
  apply Pos.max_case_strong; intros; lia
| [ |- (Pos.max ?x ?y < ?z)%positive ] =>
  apply Pos.max_case_strong; intros; lia
| [ |- (?z < Pos.max ?x ?y)%positive ] =>
  apply Pos.max_case_strong; intros; lia
| _ => zify; omega
end : core.
Hint Resolve Pos.le_max_r Pos.le_max_l : core.

Hint Constructors valid linear : core.


Lemma poly_add_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
  valid (Pos.max kl kr) (poly_add pl pr).
Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_cst v p).

Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.

Lemma poly_mul_mon_valid_compat : forall k i p,
  valid k p -> valid (Pos.max (Pos.succ i) k) (poly_mul_mon i p).

Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
  valid (Pos.max kl kr) (poly_mul pl pr).


Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr ->
  linear (Pos.max kl kr) (poly_add pl pr).
End Algebra.

Section Reduce.


Lemma reduce_aux_eval_compat : forall k p var, valid (Pos.succ k) p ->
  (list_nth k var false && eval var (reduce_aux k p) = list_nth k var false && eval var p).


Lemma reduce_eval_compat : forall k p var, valid k p ->
  eval var (reduce p) = eval var p.

Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive ->
  reduce_aux l p = reduce_aux k p.


Lemma linear_reduce_aux : forall i p, valid (Pos.succ i) p -> linear i (reduce_aux i p).
Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).

End Reduce.