Retrieve computational part of micromega from Stdlib

Author: proux01

doc/corelib/index-list.html.template

@@ -200,4 +200,15 @@ through the <tt>Require Import</tt> command.</p>
     theories/Corelib/ring/field_checker.v
     theories/Corelib/ring/field_eval.v
   </dd>
+
+  <dt id="micromega"> <a href="#micromega"><b>micromega</b></a>:
+    The micromega tactics
+  </dt>
+  <dd>
+    theories/Corelib/micromega/micromega_formula.v
+    theories/Corelib/micromega/micromega_witness.v
+    theories/Corelib/micromega/micromega_tactics.v
+    theories/Corelib/micromega/micromega_checker.v
+    theories/Corelib/micromega/micromega_eval.v
+  </dd>
 </dl>

test-suite/Makefile

@@ -188,7 +188,7 @@ UNIT_TESTS := unit-tests
 DISABLED_SUBSYSTEMS?=
 
 VSUBSYSTEMS := prerequisite success failure bugs bugs-nocoqchk output output-coqtop \
-  output-modulo-time $(INTERACTIVE) $(COMPLEXITY) modules stm \
+  output-modulo-time micromega $(INTERACTIVE) $(COMPLEXITY) modules stm \
   coqdoc ssr $(wildcard primitive/*) ltac2 coqchk
 
 # All subsystems
@@ -281,6 +281,7 @@ summary:
 	  $(call summary_dir, "Interactive tests", interactive); \
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
+	  $(call summary_dir, "Micromega tests", micromega); \
 	  $(call summary_dir, "Module tests", modules); \
 	  $(call summary_dir, "Primitive tests", primitive); \
 	  $(call summary_dir, "STM tests", stm); \
@@ -377,7 +378,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 	$(HIDE)$(call REPORT_TIMER,$@)
 
-$(addsuffix .log,$(wildcard bugs/*.v ssr/*.v success/*.v failure/*.v stm/*.v modules/*.v primitive/*/*.v ltac2/*.v coqchk/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard bugs/*.v ssr/*.v success/*.v failure/*.v stm/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v coqchk/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(SHOW) "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \

test-suite/micromega/witness_tactics.v

@@ -0,0 +1,59 @@
+From Corelib Require Import BinNums RatDef micromega_formula micromega_witness.
+From Corelib Require Import micromega_tactics.
+
+Goal True.
+Proof.
+(* x + 2 y <= 3 -> 2 x + y <= 3 -> x + y <= 2 *)
+pose (ff :=
+  IMPL
+    (EQ
+       (A isBool
+          {|
+            Flhs := PEadd (PEX _ xH) (PEmul (PEc (Qmake (Zpos (xO xH)) xH)) (PEX _ (xO xH)));
+            Fop := OpLe;
+            Frhs := PEc (Qmake (Zpos (xI xH)) xH)
+          |} tt) (TT isBool)) None
+    (IMPL
+       (EQ
+          (A isBool
+             {|
+               Flhs := PEadd (PEmul (PEc (Qmake (Zpos (xO xH)) xH)) (PEX _ xH)) (PEX _ (xO xH));
+               Fop := OpLe;
+               Frhs := PEc (Qmake (Zpos (xI xH)) xH)
+             |} tt) (TT isBool)) None
+       (EQ
+          (A isBool
+             {| Flhs := PEadd (PEX _ xH) (PEX _ (xO xH)); Fop := OpLe; Frhs := PEc (Qmake (Zpos (xO xH)) xH) |} tt)
+          (TT isBool))) : BFormula (Formula Q) isProp).
+let ff' := eval unfold ff in ff in wlra_Q wit0 ff'.
+Check eq_refl : wit0 = (PsatzAdd (PsatzIn Q 2)
+  (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC (Qmake (Zpos (xI xH)) xH)) (PsatzIn Q 0))) :: nil)%list.
+(* indeed, ff is normalized to:
+   ~ (x + y - 2 > 0 /\ - 2 x - y + 3 >= 0 /\ - x - 2 y + 3 >= 0)
+      \-----v-----/    \-------v--------/    \-------v--------/
+           (0)                (1)                   (2)
+   witness is (2) + (1) + 3 * (0) meaning that (0) /\ (1) /\ (2) implies 0 > 0
+   which is inconsistent and proves the original formula by contraposite. *)
+let ff' := eval unfold ff in ff in wlia wit1 ff'.
+Check eq_refl : wit1 = (RatProof (PsatzAdd (PsatzIn Z 2) (PsatzAdd (PsatzIn Z 1)
+  (PsatzIn Z 0))) DoneProof :: nil)%list.
+let ff' := eval unfold ff in ff in wnia wit4 ff'.
+Check eq_refl : wit4 = (RatProof (PsatzAdd (PsatzIn Z 2) (PsatzAdd (PsatzIn Z 1)
+  (PsatzIn Z 0))) DoneProof :: nil)%list.
+let ff' := eval unfold ff in ff in wnra_Q wit5 ff'.
+Check eq_refl : wit5 = (PsatzAdd (PsatzIn Q 2)
+  (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC (Qmake (Zpos (xI xH)) xH)) (PsatzIn Q 0))) :: nil)%list.
+Fail let ff' := eval unfold ff in ff in wsos_Q wit6 ff'.
+Fail let ff' := eval unfold ff in ff in wsos_Z wit6 ff'.
+(* Requires Csdp, not in CI
+let ff' := eval unfold ff in ff in wpsatz_Z 3 wit2 ff'.
+Check eq_refl : wit2 = (RatProof (PsatzAdd (PsatzC (Zpos xH))
+  (PsatzAdd (PsatzIn Z 2) (PsatzAdd (PsatzIn Z 1) (PsatzIn Z 0)))) DoneProof
+  :: nil)%list.
+let ff' := eval unfold ff in ff in wpsatz_Q 3 wit3 ff'.
+Check eq_refl : wit3 = (PsatzAdd (PsatzIn Q 0)
+  (PsatzAdd (PsatzMulE (PsatzIn Q 2) (PsatzC (Qmake (Zpos xH) (xO xH))))
+            (PsatzAdd (PsatzMulE (PsatzIn Q 1) (PsatzC (Qmake (Zpos xH) (xO xH))))
+                      (PsatzMulE (PsatzIn Q 0) (PsatzC (Qmake (Zpos xH) (xO xH)))))) :: nil)%list. *)
+(* (0) + 1/2 * (2) + 1/2 * (1) + 1/2 * (0) *)
+Abort.