1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
Require Import ZArith QArith.
From Coq.micromega Require Import RingMicromega EnvRing Tauto.
From Coq.micromega Require Import ZMicromega QMicromega.
Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core".
Declare ML Module "micromega_plugin:coq-core.plugins.micromega".
Goal True.
Proof.
pose (ff :=
IMPL
(EQ
(A isBool
{|
Flhs := PEadd (PEX 1) (PEmul (PEc 2%Q) (PEX 2));
Fop := OpLe;
Frhs := PEc 3%Q
|} tt) (TT isBool)) None
(IMPL
(EQ
(A isBool
{|
Flhs := PEadd (PEmul (PEc 2%Q) (PEX 1)) (PEX 2);
Fop := OpLe;
Frhs := PEc 3%Q
|} tt) (TT isBool)) None
(EQ
(A isBool
{| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLe; Frhs := PEc 2%Q |} 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 3%Q) (PsatzIn Q 0))) :: nil)%list.
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 3%Q) (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 1)
(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 (1 # 2)))
(PsatzAdd (PsatzMulE (PsatzIn Q 1) (PsatzC (1 # 2)))
(PsatzMulE (PsatzIn Q 0) (PsatzC (1 # 2))))) :: nil)%list. *)
Abort.
|
