Library Stdlib.btauto.Reflect

Require Import Bool DecidableClass Algebra Ring PArith Lia.

Section Bool.


Inductive formula :=
| formula_var : positive -> formula
| formula_btm : formula
| formula_top : formula
| formula_cnj : formula -> formula -> formula
| formula_dsj : formula -> formula -> formula
| formula_neg : formula -> formula
| formula_xor : formula -> formula -> formula
| formula_ifb : formula -> formula -> formula -> formula.

Fixpoint formula_eval var f := match f with
| formula_var x => list_nth x var false
| formula_btm => false
| formula_top => true
| formula_cnj fl fr => (formula_eval var fl) && (formula_eval var fr)
| formula_dsj fl fr => (formula_eval var fl) || (formula_eval var fr)
| formula_neg f => negb (formula_eval var f)
| formula_xor fl fr => xorb (formula_eval var fl) (formula_eval var fr)
| formula_ifb fc fl fr =>
  if formula_eval var fc then formula_eval var fl else formula_eval var fr
end.

End Bool.


Section Translation.


Fixpoint poly_of_formula f := match f with
| formula_var x => Poly (Cst false) x (Cst true)
| formula_btm => Cst false
| formula_top => Cst true
| formula_cnj fl fr =>
  let pl := poly_of_formula fl in
  let pr := poly_of_formula fr in
  poly_mul pl pr
| formula_dsj fl fr =>
  let pl := poly_of_formula fl in
  let pr := poly_of_formula fr in
  poly_add (poly_add pl pr) (poly_mul pl pr)
| formula_neg f => poly_add (Cst true) (poly_of_formula f)
| formula_xor fl fr => poly_add (poly_of_formula fl) (poly_of_formula fr)
| formula_ifb fc fl fr =>
  let pc := poly_of_formula fc in
  let pl := poly_of_formula fl in
  let pr := poly_of_formula fr in
  poly_add pr (poly_add (poly_mul pc pl) (poly_mul pc pr))
end.

Opaque poly_add.


Lemma poly_of_formula_eval_compat : forall var f,
  eval var (poly_of_formula f) = formula_eval var f.

#[local]
Hint Extern 5 => change 0 with (min 0 0) : core.
Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
Local Hint Constructors valid : core.
#[local]
Hint Extern 5 => lia : core.


Lemma poly_of_formula_valid_compat : forall f, exists n, valid n (poly_of_formula f).


Lemma poly_of_formula_sound : forall fl fr var,
  poly_of_formula fl = poly_of_formula fr -> formula_eval var fl = formula_eval var fr.

End Translation.

Section Completeness.



Lemma reduce_poly_of_formula_sound : forall fl fr var,
  reduce (poly_of_formula fl) = reduce (poly_of_formula fr) ->
  formula_eval var fl = formula_eval var fr.

Definition make_last {A} n (x def : A) :=
  Pos.peano_rect (fun _ => list A)
    (cons x nil)
    (fun _ F => cons def F) n.


Fixpoint list_replace l n b :=
match l with
| nil => make_last n b false
| cons a l =>
  Pos.peano_rect _
    (cons b l) (fun n _ => cons a (list_replace l n b)) n
end.

Existing Instance Decidable_null.

Fixpoint boolean_witness p :=
match p with
| Cst c => nil
| Poly p i q =>
  if decide (null p) then
    let var := boolean_witness q in
    list_replace var i true
  else
    let var := boolean_witness p in
    list_replace var i false
end.

Lemma list_nth_base : forall A (def : A) l,
  list_nth 1 l def = match l with nil => def | cons x _ => x end.

Lemma list_nth_succ : forall A n (def : A) l,
  list_nth (Pos.succ n) l def =
    match l with nil => def | cons _ l => list_nth n l def end.

Lemma list_nth_nil : forall A n (def : A),
  list_nth n nil def = def.

Lemma make_last_nth_1 : forall A n i x def, i <> n ->
  list_nth i (@make_last A n x def) def = def.

Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.

Lemma list_replace_nth_1 : forall var i j x, i <> j ->
  list_nth i (list_replace var j x) false = list_nth i var false.
Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.


Lemma boolean_witness_nonzero : forall k p, linear k p -> ~ null p ->
  eval (boolean_witness p) p = true.


Lemma reduce_poly_of_formula_sound_alt : forall var fl fr,
  reduce (poly_add (poly_of_formula fl) (poly_of_formula fr)) = Cst false ->
  formula_eval var fl = formula_eval var fr.



End Completeness.



Global Transparent decide poly_add.


Register formula_var as plugins.btauto.f_var.
Register formula_btm as plugins.btauto.f_btm.
Register formula_top as plugins.btauto.f_top.
Register formula_cnj as plugins.btauto.f_cnj.
Register formula_dsj as plugins.btauto.f_dsj.
Register formula_neg as plugins.btauto.f_neg.
Register formula_xor as plugins.btauto.f_xor.
Register formula_ifb as plugins.btauto.f_ifb.

Register formula_eval as plugins.btauto.eval.
Register boolean_witness as plugins.btauto.witness.
Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness.