(Joint Center)Library ordered_qelim

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import bigop ssralg finset fingroup zmodp.
Require Import poly ssrnum.

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GRing.

Reserved Notation "p <% q" (at level 70, no associativity).
Reserved Notation "p <=% q" (at level 70, no associativity).

Set Printing Width 30.

Module ord.

Section Formulas.

Variable T : Type.

Inductive formula : Type :=
| Bool of bool
| Equal of (term T) & (term T)
| Lt of (term T) & (term T)
| Le of (term T) & (term T)
| Unit of (term T)
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula
| Exists of nat & formula
| Forall of nat & formula.

End Formulas.

Fixpoint term_eq (T : eqType)(t1 t2 : term T) :=
  match t1, t2 with
    | Var n1, Var n2n1 == n2
    | Const r1, Const r2r1 == r2
    | NatConst n1, NatConst n2n1 == n2
    | Add r1 s1, Add r2 s2(term_eq r1 r2) && (term_eq s1 s2)
    | Opp r1, Opp r2term_eq r1 r2
    | NatMul r1 n1, NatMul r2 n2(term_eq r1 r2) && (n1 == n2)
    | Mul r1 s1, Mul r2 s2(term_eq r1 r2) && (term_eq s1 s2)
    | Inv r1, Inv r2term_eq r1 r2
    | Exp r1 n1, Exp r2 n2(term_eq r1 r2) && (n1 == n2)
    |_, _false
  end.

Lemma term_eqP (T : eqType) : Equality.axiom (@term_eq T).

Canonical term_eqMixin (T : eqType) := EqMixin (@term_eqP T).
Canonical term_eqType (T : eqType) :=
   Eval hnf in EqType (term T) (@term_eqMixin T).

Implicit Arguments term_eqP [x y].


Implicit Arguments Bool [T].

Notation True := (Bool true).
Notation False := (Bool false).

Delimit Scope oterm_scope with oT.
Notation "''X_' i" := (Var _ i) : oterm_scope.
Notation "n %:R" := (NatConst _ n) : oterm_scope.
Notation "x %:T" := (Const x) : oterm_scope.
Notation "0" := 0%:R%oT : oterm_scope.
Notation "1" := 1%:R%oT : oterm_scope.
Infix "+" := Add : oterm_scope.
Notation "- t" := (Opp t) : oterm_scope.
Notation "t - u" := (Add t (- u)) : oterm_scope.
Infix "×" := Mul : oterm_scope.
Infix "*+" := NatMul : oterm_scope.
Notation "t ^-1" := (Inv t) : oterm_scope.
Notation "t / u" := (Mul t u^-1) : oterm_scope.
Infix "^+" := Exp : oterm_scope.
Notation "t ^- n" := (t^-1 ^+ n)%oT : oterm_scope.
Infix "==" := Equal : oterm_scope.
Infix "<%" := Lt : oterm_scope.
Infix "<=%" := Le : oterm_scope.
Infix "∧" := And : oterm_scope.
Infix "∨" := Or : oterm_scope.
Infix "==>" := Implies : oterm_scope.
Notation "~ f" := (Not f) : oterm_scope.
Notation "x != y" := (Not (x == y)) : oterm_scope.
Notation "''exists' ''X_' i , f" := (Exists i f) : oterm_scope.
Notation "''forall' ''X_' i , f" := (Forall i f) : oterm_scope.

Section Substitution.

Variable T : Type.

Fixpoint fsubst (f : formula T) (s : nat × term T) :=
  match f with
  | Bool _f
  | (t1 == t2) ⇒ (tsubst t1 s == tsubst t2 s)
  | (t1 <% t2) ⇒ (tsubst t1 s <% tsubst t2 s)
  | (t1 <=% t2) ⇒ (tsubst t1 s <=% tsubst t2 s)
  | (Unit t1) ⇒ Unit (tsubst t1 s)
  | (f1 f2) ⇒ (fsubst f1 s fsubst f2 s)
  | (f1 f2) ⇒ (fsubst f1 s fsubst f2 s)
  | (f1 ==> f2) ⇒ (fsubst f1 s ==> fsubst f2 s)
  | (¬ f1) ⇒ (¬ fsubst f1 s)
  | (' 'X_i, f1) ⇒ (' 'X_i, if i == s.1 then f1 else fsubst f1 s)
  | (' 'X_i, f1) ⇒ (' 'X_i, if i == s.1 then f1 else fsubst f1 s)
  end%oT.

End Substitution.

Section OrderedClause.

Inductive oclause (R : Type) : Type :=
  Oclause : seq (term R) → seq (term R) → seq (term R) → seq (term R) → oclause R.

Definition eq_of_oclause (R : Type)(x : oclause R) :=
  let: Oclause y _ _ _ := x in y.
Definition neq_of_oclause (R : Type)(x : oclause R) :=
  let: Oclause _ y _ _ := x in y.
Definition lt_of_oclause (R : Type) (x : oclause R) :=
  let: Oclause _ _ y _ := x in y.
Definition le_of_oclause (R : Type) (x : oclause R) :=
  let: Oclause _ _ _ y := x in y.

End OrderedClause.

Delimit Scope oclause_scope with OCLAUSE.
Open Scope oclause_scope.

Notation "p .1" := (@eq_of_oclause _ p)
  (at level 2, left associativity, format "p .1") : oclause_scope.
Notation "p .2" := (@neq_of_oclause _ p)
  (at level 2, left associativity, format "p .2") : oclause_scope.

Notation "p .3" := (@lt_of_oclause _ p)
  (at level 2, left associativity, format "p .3") : oclause_scope.
Notation "p .4" := (@le_of_oclause _ p)
  (at level 2, left associativity, format "p .4") : oclause_scope.

Definition oclause_eq (T : eqType)(t1 t2 : oclause T) :=
  let: Oclause eq_l1 neq_l1 lt_l1 leq_l1 := t1 in
  let: Oclause eq_l2 neq_l2 lt_l2 leq_l2 := t2 in
    [&& eq_l1 == eq_l2, neq_l1 == neq_l2, lt_l1 == lt_l2 & leq_l1 == leq_l2].

Lemma oclause_eqP (T : eqType) : Equality.axiom (@oclause_eq T).

Canonical oclause_eqMixin (T : eqType) := EqMixin (@oclause_eqP T).
Canonical oclause_eqType (T : eqType) :=
   Eval hnf in EqType (oclause T) (@oclause_eqMixin T).

Implicit Arguments oclause_eqP [x y].

Section EvalTerm.

Variable R : realDomainType.

Evaluation of a reified formula

Fixpoint holds (e : seq R) (f : ord.formula R) {struct f} : Prop :=
  match f with
  | Bool bb
  | (t1 == t2)%oTeval e t1 = eval e t2
  | (t1 <% t2)%oTeval e t1 < eval e t2
  | (t1 <=% t2)%oTeval e t1 eval e t2
  | Unit t1eval e t1 \in unit
  | (f1 f2)%oTholds e f1 holds e f2
  | (f1 f2)%oTholds e f1 holds e f2
  | (f1 ==> f2)%oTholds e f1holds e f2
  | (¬ f1)%oT¬ holds e f1
  | (' 'X_i, f1)%oT x, holds (set_nth 0 e i x) f1
  | (' 'X_i, f1)%oT x, holds (set_nth 0 e i x) f1
  end.

Extensionality of formula evaluation
Lemma eq_holds e e' f : same_env e e'holds e fholds e' f.

Evaluation and substitution by a constant
Lemma holds_fsubst e f i v :
  holds e (fsubst f (i, v%:T)%T) holds (set_nth 0 e i v) f.

Boolean test selecting formulas in the theory of rings
Fixpoint rformula (f : formula R) :=
  match f with
  | Bool _true
  | t1 == t2rterm t1 && rterm t2
  | t1 <% t2rterm t1 && rterm t2
  | t1 <=% t2rterm t1 && rterm t2
  | Unit t1false
  | (f1 f2) | (f1 f2) | (f1 ==> f2) ⇒ rformula f1 && rformula f2
  | (¬ f1) | (' 'X__, f1) | (' 'X__, f1) ⇒ rformula f1
  end%oT.

An oformula stating that t1 is equal to 0 in the ring theory.
Definition eq0_rform t1 :=
  let m := @ub_var R t1 in
  let: (t1', r1) := to_rterm t1 [::] m in
  let fix loop r i := match r with
  | [::]t1' == 0
  | t :: r'
    let f := ('X_i × t == 1 t × 'X_i == 1) in
     ' 'X_i, (f 'X_i == t ¬ (' 'X_i, f)) ==> loop r' i.+1
  end%oT
  in loop r1 m.

An oformula stating that t1 is less than 0 in the equational ring theory. Definition leq0_rform t1 := let m := @ub_var R t1 in let: (t1', r1) := to_rterm t1 [:: ] m in let fix loop r i := match r with | [:: ] => 'exists 'X_m.+1, t1' == 'X_m.+1 * 'X_m.+1 | t :: r' => let f := ('X_i * t == 1 /\ t * 'X_i == 1) in 'forall 'X_i, (f \/ 'X_i == t /\ ~ ('exists 'X_i, f)) ==> loop r' i.+1 end%oT in loop r1 m.
Definition leq0_rform t1 :=
  let m := @ub_var R t1 in
  let: (t1', r1) := to_rterm t1 [::] m in
  let fix loop r i := match r with
  | [::]t1' <=% 0
  | t :: r'
    let f := ('X_i × t == 1 t × 'X_i == 1) in
     ' 'X_i, (f 'X_i == t ¬ (' 'X_i, f)) ==> loop r' i.+1
  end%oT
  in loop r1 m.

Definition lt0_rform t1 := let m := @ub_var R t1 in let: (t1', r1) := to_rterm t1 [:: ] m in let fix loop r i := match r with | [:: ] => 'exists 'X_m.+1, (t1' == 'X_m.+1 * 'X_m.+1 /\ ~ ('X_m.+1 == 0)) | t :: r' => let f := ('X_i * t == 1 /\ t * 'X_i == 1) in 'forall 'X_i, (f \/ 'X_i == t /\ ~ ('exists 'X_i, f)) ==> loop r' i.+1 end%oT in loop r1 m.

Definition lt0_rform t1 :=
  let m := @ub_var R t1 in
  let: (t1', r1) := to_rterm t1 [::] m in
  let fix loop r i := match r with
  | [::]t1' <% 0
  | t :: r'
    let f := ('X_i × t == 1 t × 'X_i == 1) in
     ' 'X_i, (f 'X_i == t ¬ (' 'X_i, f)) ==> loop r' i.+1
  end%oT
  in loop r1 m.

Transformation of a formula in the theory of rings with units into an
equivalent formula in the sub-theory of rings.
Fixpoint to_rform f :=
  match f with
  | Bool bf
  | t1 == t2eq0_rform (t1 - t2)
  | t1 <% t2lt0_rform (t1 - t2)
  | t1 <=% t2leq0_rform (t1 - t2)
  | Unit t1eq0_rform (t1 × t1^-1 - 1)
  | f1 f2to_rform f1 to_rform f2
  | f1 f2to_rform f1 to_rform f2
  | f1 ==> f2to_rform f1 ==> to_rform f2
  | ¬ f1¬ to_rform f1
  | (' 'X_i, f1) ⇒ ' 'X_i, to_rform f1
  | (' 'X_i, f1) ⇒ ' 'X_i, to_rform f1
  end%oT.

The transformation gives a ring formula. the last part of the proof consists in 3 cases that are exactly the same. how to factorize ?
Lemma to_rform_rformula f : rformula (to_rform f).

Import Num.Theory.

Correctness of the transformation.
Lemma to_rformP e f : holds e (to_rform f) holds e f.

The above proof is ugly but is in fact copypaste
Boolean test selecting formulas which describe a constructible set, i.e. formulas without quantifiers.
The quantifier elimination check.
Fixpoint qf_form (f : formula R) :=
  match f with
  | Bool _ | _ == _ | Unit _ | Lt _ _ | Le _ _true
  | f1 f2 | f1 f2 | f1 ==> f2qf_form f1 && qf_form f2
  | ¬ f1qf_form f1
  | _false
  end%oT.

Boolean holds predicate for quantifier free formulas
Definition qf_eval e := fix loop (f : formula R) : bool :=
  match f with
  | Bool bb
  | t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
  | t1 <% t2 ⇒ (eval e t1 < eval e t2)%bool
  | t1 <=% t2 ⇒ (eval e t1 eval e t2)%bool
  | Unit t1eval e t1 \in unit
  | f1 f2loop f1 && loop f2
  | f1 f2loop f1 || loop f2
  | f1 ==> f2 ⇒ (loop f1 ==> loop f2)%bool
  | ¬ f1~~ loop f1
  |_false
  end%oT.

qf_eval is equivalent to holds
Lemma qf_evalP e f : qf_form freflect (holds e f) (qf_eval e f).

Quantifier-free formula are normalized into DNF. A DNF is represented by the type seq (seq (term R) * seq (term R)), where we separate positive and negative literals
DNF preserving conjunction

Definition and_odnf (bcs1 bcs2 : seq (oclause R)) :=
  \big[cat/nil]_(bc1 <- bcs1)
     map (fun bc2 : oclause R
       (Oclause (bc1.1 ++ bc2.1) (bc1.2 ++ bc2.2) (bc1.3 ++ bc2.3) (bc1.4 ++ bc2.4)))%OCLAUSE bcs2.

Computes a DNF from a qf ring formula
Fixpoint qf_to_odnf (f : formula R) (neg : bool) {struct f} : seq (oclause R) :=
  match f with
  | Bool bif b (+) neg then [:: (Oclause [::] [::] [::] [::])] else [::]
  | t1 == t2
    [:: if neg then (Oclause [::] [:: t1 - t2] [::] [::]) else (Oclause [:: t1 - t2] [::] [::] [::])]
  | t1 <% t2
    [:: if neg then (Oclause [::] [::] [::] [:: t1 - t2]) else (Oclause [::] [::] [:: t2 - t1] [::])]
  | t1 <=% t2
    [:: if neg then (Oclause [::] [::] [:: t1 - t2] [::]) else (Oclause [::] [::] [::] [:: t2 - t1])]
  | f1 f2 ⇒ (if neg then cat else and_odnf) [rec f1, neg] [rec f2, neg]
  | f1 f2 ⇒ (if neg then and_odnf else cat) [rec f1, neg] [rec f2, neg]
  | f1 ==> f2 ⇒ (if neg then and_odnf else cat) [rec f1, ~~ neg] [rec f2, neg]
  | ¬ f1[rec f1, ~~ neg]
  | _if neg then [:: (Oclause [::] [::] [::] [::])] else [::]
  end%oT where "[ 'rec' f , neg ]" := (qf_to_odnf f neg).

Conversely, transforms a DNF into a formula
Definition odnf_to_oform :=
  let pos_lit t := And (t == 0)%oT in let neg_lit t := And (t != 0)%oT in
  let lt_lit t := And (0 <% t)%oT in let le_lit t := And (0 <=% t)%oT in
  let ocls (bc : oclause R) :=
    Or
    (foldr pos_lit True bc.1 foldr neg_lit True bc.2
     foldr lt_lit True bc.3 foldr le_lit True bc.4) in
  foldr ocls False.

Catenation of dnf is the Or of formulas
and_dnf is the And of formulas
Lemma and_odnfP e bcs1 bcs2 :
  qf_eval e (odnf_to_oform (and_odnf bcs1 bcs2))
   = qf_eval e (odnf_to_oform bcs1 odnf_to_oform bcs2).

Lemma qf_to_dnfP e :
  let qev f b := qf_eval e (odnf_to_oform (qf_to_odnf f b)) in
   f, qf_form f && rformula fqev f false = qf_eval e f.

Lemma dnf_to_form_qf bcs : qf_form (odnf_to_oform bcs).

Definition dnf_rterm (cl : oclause R) :=
  [&& all (@rterm R) cl.1, all (@rterm R) cl.2,
  all (@rterm R) cl.3 & all (@rterm R) cl.4].

Lemma qf_to_dnf_rterm f b : rformula fall dnf_rterm (qf_to_odnf f b).

Lemma dnf_to_rform bcs : rformula (odnf_to_oform bcs) = all dnf_rterm bcs.

Implicit Type f : formula R.

Fixpoint leq_elim_aux (eq_l lt_l le_l : seq (term R)) :=
  match le_l with
    [::][:: (eq_l, lt_l)]
    |le1 :: le_l'
  let res := leq_elim_aux eq_l lt_l le_l' in
  let as_eq := map (fun x(le1 :: x.1%PAIR, x.2%PAIR)) res in
  let as_lt := map (fun x(x.1%PAIR, le1 :: x.2%PAIR)) res in
    as_eq ++ as_lt
  end.

Definition oclause_leq_elim oc : seq (oclause R) :=
  let: Oclause eq_l neq_l lt_l le_l := oc in
    map (fun xOclause x.1%PAIR neq_l x.2%PAIR [::])
    (leq_elim_aux eq_l lt_l le_l).

Definition terms_of_oclause (oc : oclause R) :=
  let: Oclause eq_l neq_l lt_l le_l := oc in
    eq_l ++ neq_l ++ lt_l ++ le_l.

Lemma terms_of_leq_elim oc1 oc2:
  oc2 \in (oclause_leq_elim oc1)
  (terms_of_oclause oc2) =i (terms_of_oclause oc1).

Lemma odnf_to_oform_cat e c d : holds e (odnf_to_oform (c ++ d))
               holds e ((odnf_to_oform c) (odnf_to_oform d))%oT.

Lemma oclause_leq_elimP oc e :
  holds e (odnf_to_oform [:: oc])
  holds e (odnf_to_oform (oclause_leq_elim oc)).

Fixpoint neq_elim_aux (lt_l neq_l : seq (term R)) :=
  match neq_l with
    [::][:: lt_l]
    |neq1 :: neq_l'
  let res := neq_elim_aux lt_l neq_l' in
  let as_pos := map (fun xneq1 :: x) res in
  let as_neg := map (fun xOpp neq1 :: x) res in
    as_pos ++ as_neg
  end.

Definition oclause_neq_elim oc : seq (oclause R) :=
  let: Oclause eq_l neq_l lt_l le_l := oc in
    map (fun xOclause eq_l [::] x le_l) (neq_elim_aux lt_l neq_l).

Lemma terms_of_neq_elim oc1 oc2:
  oc2 \in (oclause_neq_elim oc1)
  {subset (terms_of_oclause oc2) (terms_of_oclause oc1) ++ (map Opp oc1.2)}.

Lemma oclause_neq_elimP oc e :
  holds e (odnf_to_oform [:: oc])
  holds e (odnf_to_oform (oclause_neq_elim oc)).

Definition oclause_neq_leq_elim oc :=
  flatten (map oclause_neq_elim (oclause_leq_elim oc)).

Lemma terms_of_neq_leq_elim oc1 oc2:
  oc2 \in (oclause_neq_leq_elim oc1)
  {subset (terms_of_oclause oc2) (terms_of_oclause oc1) ++ map Opp oc1.2}.

Lemma oclause_neq_leq_elimP oc e :
  holds e (odnf_to_oform [:: oc])
  holds e (odnf_to_oform (oclause_neq_leq_elim oc)).

Definition oclause_to_w oc :=
  let s := oclause_neq_leq_elim oc in
    map (fun xlet: Oclause eq_l neq_l lt_l leq_l := x in (eq_l, lt_l)) s.

Definition w_to_oclause (t : seq (term R) × seq (term R)) :=
  Oclause t.1%PAIR [::] t.2%PAIR [::].

Lemma oclause_leq_elim4 bc oc : oc \in (oclause_leq_elim bc)oc.4 == [::].

Lemma oclause_neq_elim2 bc oc :
  oc \in (oclause_neq_elim bc)(oc.2 == [::]) && (oc.4 == bc.4).

Lemma oclause_to_wP e bc :
  holds e (odnf_to_oform (oclause_neq_leq_elim bc))
  holds e (odnf_to_oform (map w_to_oclause (oclause_to_w bc))).

Variable wproj : nat → (seq (term R) × seq (term R)) → formula R.

Definition proj (n : nat)(oc : oclause R) :=
  foldr Or False (map (wproj n) (oclause_to_w oc)).

Hypothesis wf_QE_wproj : i bc (bc_i := wproj i bc),
  dnf_rterm (w_to_oclause bc) → qf_form bc_i && rformula bc_i.

Lemma dnf_rterm_subproof bc : dnf_rterm bc
  all (dnf_rterm \o w_to_oclause) (oclause_to_w bc).

Lemma wf_QE_proj i : bc (bc_i := proj i bc),
  dnf_rterm bcqf_form bc_i && rformula bc_i.

Hypothesis valid_QE_wproj :
   i bc (bc' := w_to_oclause bc)
    (ex_i_bc := (' 'X_i, odnf_to_oform [:: bc'])%oT) e,
  dnf_rterm bc'
  reflect (holds e ex_i_bc) (qf_eval e (wproj i bc)).

Lemma valid_QE_proj e i : bc (bc_i := proj i bc)
  (ex_i_bc := (' 'X_i, odnf_to_oform [:: bc])%oT),
  dnf_rterm bcreflect (holds e ex_i_bc) (qf_eval e (proj i bc)).

Let elim_aux f n := foldr Or False (map (proj n) (qf_to_odnf f false)).

Fixpoint quantifier_elim f :=
  match f with
  | f1 f2(quantifier_elim f1) (quantifier_elim f2)
  | f1 f2(quantifier_elim f1) (quantifier_elim f2)
  | f1 ==> f2(¬ quantifier_elim f1) (quantifier_elim f2)
  | ¬ f¬ quantifier_elim f
  | (' 'X_n, f) ⇒ elim_aux (quantifier_elim f) n
  | (' 'X_n, f) ⇒ ¬ elim_aux (¬ quantifier_elim f) n
  | _f
  end%oT.

Lemma quantifier_elim_wf f :
  let qf := quantifier_elim f in rformula fqf_form qf && rformula qf.

Lemma quantifier_elim_rformP e f :
  rformula freflect (holds e f) (qf_eval e (quantifier_elim f)).

Definition proj_sat e f := qf_eval e (quantifier_elim (to_rform f)).

Lemma proj_satP : e f, reflect (holds e f) (proj_sat e f).

End EvalTerm.

End ord.