Require Import Bool DecidableClass Algebra Ring NPeano.

Section Bool.

(* Boolean formulas and their evaluations *)

Inductive formula :=
| formula_var : nat -> 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.

(* Translation of formulas into polynomials *)

Section Translation.

(* This is straightforward. *)

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.

(* Compatibility of translation wrt evaluation *)

Lemma poly_of_formula_eval_compat : forall var f,
  eval var (poly_of_formula f) = formula_eval var f.
Proof.
intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto.
  now simpl; match goal with [ |- ?t = ?u ] => destruct u; reflexivity end.
  rewrite poly_mul_compat, IHf1, IHf2; ring.
  repeat rewrite poly_add_compat.
  rewrite poly_mul_compat; try_rewrite.
  now match goal with [ |- ?t = ?x || ?y ] => destruct x; destruct y; reflexivity end.
  rewrite poly_add_compat; try_rewrite.
  now match goal with [ |- ?t = negb ?x ] => destruct x; reflexivity end.
  rewrite poly_add_compat; congruence.
  rewrite ?poly_add_compat, ?poly_mul_compat; try_rewrite.
  match goal with
    [ |- ?t = if ?b1 then ?b2 else ?b3 ] => destruct b1; destruct b2; destruct b3; reflexivity
  end.
Qed.

Hint Extern 5 => change 0 with (min 0 0).
Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat.
Local Hint Constructors valid.

(* Compatibility with validity *)

Lemma poly_of_formula_valid_compat : forall f, exists n, valid n (poly_of_formula f).
Proof.
intros f; induction f; simpl.
  now exists (S n); constructor; intuition; inversion H.
  now exists 0; auto.
  now exists 0; auto.
  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max n1 n2); auto.
  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max (max n1 n2) (max n1 n2)); auto.
  now destruct IHf as [n Hn]; exists (max 0 n); auto.
  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max n1 n2); auto.
  destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; destruct IHf3 as [n3 Hn3]; eexists; eauto.
Qed.

(* The soundness lemma ; alas not complete! *)

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.
Proof.
intros fl fr var Heq.
repeat rewrite <- poly_of_formula_eval_compat.
rewrite Heq; reflexivity.
Qed.

End Translation.

Section Completeness.

(* Lemma reduce_poly_of_formula_simpl : forall fl fr var,
  simpl_eval (var_of_list var) (reduce (poly_of_formula fl)) = simpl_eval (var_of_list var) (reduce (poly_of_formula fr)) ->
  formula_eval var fl = formula_eval var fr.
Proof.
intros fl fr var Hrw.
do 2 rewrite <- poly_of_formula_eval_compat.
destruct (poly_of_formula_valid_compat fl) as [nl Hl].
destruct (poly_of_formula_valid_compat fr) as [nr Hr].
rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); [|assumption].
rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); [|assumption].
do 2 rewrite <- eval_simpl_eval_compat; assumption.
Qed. *)

(* Soundness of the method ; immediate *)

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.
Proof.
intros fl fr var Heq.
repeat rewrite <- poly_of_formula_eval_compat.
destruct (poly_of_formula_valid_compat fl) as [nl Hl].
destruct (poly_of_formula_valid_compat fr) as [nr Hr].
rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto.
rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto.
rewrite Heq; reflexivity.
Qed.

Fixpoint make_last {A} n (x def : A) :=
match n with
| 0 => cons x nil
| S n => cons def (make_last n x def)
end.

(* Replace the nth element of a list *)

Fixpoint list_replace l n b :=
match l with
| nil => make_last n b false
| cons a l =>
  match n with
  | 0 => cons b l
  | S n => cons a (list_replace l n b)
  end
end.

(** Extract a non-null witness from a polynomial *)

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 make_last_nth_1 : forall A n i x def, i <> n ->
  List.nth i (@make_last A n x def) def = def.
Proof.
intros A n; induction n; intros i x def Hd; simpl.
  destruct i; [exfalso; omega|now destruct i; auto].
  destruct i; intuition.
Qed.

Lemma make_last_nth_2 : forall A n x def, List.nth n (@make_last A n x def) def = x.
Proof.
intros A n; induction n; intros x def; simpl; auto.
Qed.

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.
Proof.
intros var; induction var; intros i j x Hd; simpl.
  rewrite make_last_nth_1; [destruct i; reflexivity|assumption].
  destruct i; destruct j; simpl; solve [auto|congruence].
Qed.

Lemma list_replace_nth_2 : forall var i x, List.nth i (list_replace var i x) false = x.
Proof.
intros var; induction var; intros i x; simpl.
  now apply make_last_nth_2.
  now destruct i; simpl in *; [reflexivity|auto].
Qed.

(* The witness is correct only if the polynomial is linear *)

Lemma boolean_witness_nonzero : forall k p, linear k p -> ~ null p ->
  eval (boolean_witness p) p = true.
Proof.
intros k p Hl Hp; induction Hl; simpl.
  destruct c; [reflexivity|elim Hp; now constructor].
  case_decide.
    rewrite eval_null_zero; [|assumption]; rewrite list_replace_nth_2; simpl.
    match goal with [ |- (if ?b then true else false) = true ] =>
      assert (Hrw : b = true); [|rewrite Hrw; reflexivity]
    end.
    erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
    now intros j Hd; apply list_replace_nth_1; omega.
    rewrite list_replace_nth_2, xorb_false_r.
    erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
    now intros j Hd; apply list_replace_nth_1; omega.
Qed.

(* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *)

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.
Proof.
intros var fl fr Heq.
repeat rewrite <- poly_of_formula_eval_compat.
destruct (poly_of_formula_valid_compat fl) as [nl Hl].
destruct (poly_of_formula_valid_compat fr) as [nr Hr].
rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto.
rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto.
rewrite <- xorb_false_l; change false with (eval var (Cst false)).
rewrite <- poly_add_compat, <- Heq.
repeat rewrite poly_add_compat.
rewrite (reduce_eval_compat nl); [|assumption].
rewrite (reduce_eval_compat (max nl nr)); [|apply poly_add_valid_compat; assumption].
rewrite (reduce_eval_compat nr); [|assumption].
rewrite poly_add_compat; ring.
Qed.

(* The completeness lemma *)

(* Lemma reduce_poly_of_formula_complete : forall fl fr,
  reduce (poly_of_formula fl) <> reduce (poly_of_formula fr) ->
  {var | formula_eval var fl <> formula_eval var fr}.
Proof.
intros fl fr H.
pose (p := poly_add (reduce (poly_of_formula fl)) (poly_opp (reduce (poly_of_formula fr)))).
pose (var := boolean_witness p).
exists var.
  intros Hc; apply (f_equal Z_of_bool) in Hc.
  assert (Hfl : linear 0 (reduce (poly_of_formula fl))).
    now destruct (poly_of_formula_valid_compat fl) as [n Hn]; apply (linear_le_compat n); [|now auto]; apply linear_reduce; auto.
  assert (Hfr : linear 0 (reduce (poly_of_formula fr))).
    now destruct (poly_of_formula_valid_compat fr) as [n Hn]; apply (linear_le_compat n); [|now auto]; apply linear_reduce; auto.
  repeat rewrite <- poly_of_formula_eval_compat in Hc.
  define (decide (null p)) b Hb; destruct b; tac_decide.
    now elim H; apply (null_sub_implies_eq 0 0); fold p; auto;
    apply linear_valid_incl; auto.
  elim (boolean_witness_nonzero 0 p); auto.
    unfold p; rewrite <- (min_id 0); apply poly_add_linear_compat; try apply poly_opp_linear_compat; now auto.
    unfold p at 2; rewrite poly_add_compat, poly_opp_compat.
    destruct (poly_of_formula_valid_compat fl) as [nl Hnl].
    destruct (poly_of_formula_valid_compat fr) as [nr Hnr].
    repeat erewrite reduce_eval_compat; eauto.
    fold var; rewrite Hc; ring.
Defined. *)

End Completeness.

(* Reification tactics *)

(* For reflexivity purposes, that would better be transparent *)

Global Transparent decide poly_add.

(* Ltac append_var x l k :=
match l with
| nil => constr: (k, cons x l)
| cons x _ => constr: (k, l)
| cons ?y ?l =>
  let ans := append_var x l (S k) in
  match ans with (?k, ?l) => constr: (k, cons y l) end
end.

Ltac build_formula t l :=
match t with
| true => constr: (formula_top, l)
| false => constr: (formula_btm, l)
| ?fl && ?fr =>
  match build_formula fl l with (?tl, ?l) =>
    match build_formula fr l with (?tr, ?l) =>
      constr: (formula_cnj tl tr, l)
    end
  end
| ?fl || ?fr =>
  match build_formula fl l with (?tl, ?l) =>
    match build_formula fr l with (?tr, ?l) =>
      constr: (formula_dsj tl tr, l)
    end
  end
| negb ?f =>
  match build_formula f l with (?t, ?l) =>
    constr: (formula_neg t, l)
  end
| _ =>
  let ans := append_var t l 0 in
  match ans with (?k, ?l) => constr: (formula_var k, l) end
end.

(* Extract a counterexample from a polynomial and display it *)

Ltac counterexample p l :=
  let var := constr: (boolean_witness p) in
  let var := eval vm_compute in var in
  let rec print l vl :=
    match l with
    | nil => idtac
    | cons ?x ?l =>
      match vl with
      | nil =>
        idtac x ":=" "false"; print l (@nil bool)
      | cons ?v ?vl =>
        idtac x ":=" v; print l vl
      end
    end
  in
  idtac "Counter-example:"; print l var.

Ltac btauto_reify :=
lazymatch goal with
| [ |- @eq bool ?t ?u ] =>
  lazymatch build_formula t (@nil bool) with
  | (?fl, ?l) =>
    lazymatch build_formula u l with
    | (?fr, ?l) =>
      change (formula_eval l fl = formula_eval l fr)
    end
  end
| _ => fail "Cannot recognize a boolean equality"
end.

(* The long-awaited tactic *)

Ltac btauto :=
lazymatch goal with
| [ |- @eq bool ?t ?u ] =>
  lazymatch build_formula t (@nil bool) with
  | (?fl, ?l) =>
    lazymatch build_formula u l with
    | (?fr, ?l) =>
      change (formula_eval l fl = formula_eval l fr);
      apply reduce_poly_of_formula_sound_alt;
      vm_compute; (reflexivity || fail "Not a tautology")
    end
  end
| _ => fail "Cannot recognize a boolean equality"
end. *)