aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Classes/CRelationClasses.v2
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/micromega/MExtraction.v5
-rw-r--r--theories/micromega/Tauto.v32
-rw-r--r--theories/micromega/ZMicromega.v78
-rw-r--r--theories/ssr/ssreflect.v43
6 files changed, 111 insertions, 51 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 236d35b68e..c489d82d0b 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -236,8 +236,6 @@ Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
-(** A HintDb for crelations. *)
-
Ltac solve_crelation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 54ee06343a..353496dfba 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -235,8 +235,6 @@ Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
-(** A HintDb for relations. *)
-
Ltac solve_relation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
diff --git a/theories/micromega/MExtraction.v b/theories/micromega/MExtraction.v
index fcb07c4774..a02d7adfa2 100644
--- a/theories/micromega/MExtraction.v
+++ b/theories/micromega/MExtraction.v
@@ -53,12 +53,13 @@ Extract Constant Rinv => "fun x -> 1 / x".
(** In order to avoid annoying build dependencies the actual
extraction is only performed as a test in the test suite. *)
-(*Extraction "micromega.ml"
+(*
+Extraction "micromega.ml"
Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
Tauto.abst_form
ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ
List.map simpl_cone (*map_cone indexes*)
- denorm Qpower vm_add
+ denorm QArith_base.Qpower vm_add
normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
*)
(* Local Variables: *)
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index ce12b02359..515372466a 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -611,13 +611,15 @@ Section S.
let '(e1 , t1) := (RXCNF (negb polarity) e1) in
if polarity
then
- if is_cnf_ff e1
- then
- RXCNF polarity e2
- else (* compute disjunction *)
- let '(e2 , t2) := (RXCNF polarity e2) in
- let (f',t') := ror_cnf_opt e1 e2 in
- (f', t1 +++ t2 +++ t') (* record the hypothesis *)
+ if is_cnf_tt e1
+ then (e1,t1)
+ else if is_cnf_ff e1
+ then
+ RXCNF polarity e2
+ else (* compute disjunction *)
+ let '(e2 , t2) := (RXCNF polarity e2) in
+ let (f',t') := ror_cnf_opt e1 e2 in
+ (f', t1 +++ t2 +++ t') (* record the hypothesis *)
else
let '(e2 , t2) := (RXCNF polarity e2) in
(and_cnf_opt e1 e2, t1 +++ t2).
@@ -1349,6 +1351,7 @@ Section S.
reflexivity.
Qed.
+
Lemma rxcnf_impl_xcnf :
forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
(IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
@@ -1366,9 +1369,15 @@ Section S.
simpl in *.
subst.
destruct pol;auto.
- generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
+ generalize (is_cnf_tt_inv (xcnf (negb true) f1)).
+ destruct (is_cnf_tt (xcnf (negb true) f1)).
+ + intros.
+ rewrite H by auto.
+ reflexivity.
+ +
+ generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
destruct (is_cnf_ff (xcnf (negb true) f1)).
- + intros H.
+ * intros.
rewrite H by auto.
unfold or_cnf_opt.
simpl.
@@ -1377,16 +1386,13 @@ Section S.
destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
apply is_cnf_ff_inv in EQ1. congruence.
reflexivity.
- +
+ *
rewrite <- ror_opt_cnf_cnf.
destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
intros.
reflexivity.
Qed.
-
-
-
Lemma rxcnf_iff_xcnf :
forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
(IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index 935757f30a..1616b5a2a4 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -296,6 +296,9 @@ Qed.
Definition psub := psub Z0 Z.add Z.sub Z.opp Zeq_bool.
Declare Equivalent Keys psub RingMicromega.psub.
+Definition popp := popp Z.opp.
+Declare Equivalent Keys popp RingMicromega.popp.
+
Definition padd := padd Z0 Z.add Zeq_bool.
Declare Equivalent Keys padd RingMicromega.padd.
@@ -608,16 +611,18 @@ Inductive ZArithProof :=
| DoneProof
| RatProof : ZWitness -> ZArithProof -> ZArithProof
| CutProof : ZWitness -> ZArithProof -> ZArithProof
+| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof
| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof
| ExProof : positive -> ZArithProof -> ZArithProof
(*ExProof x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *)
.
-(*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*)
+
Register ZArithProof as micromega.ZArithProof.type.
Register DoneProof as micromega.ZArithProof.DoneProof.
Register RatProof as micromega.ZArithProof.RatProof.
Register CutProof as micromega.ZArithProof.CutProof.
+Register SplitProof as micromega.ZArithProof.SplitProof.
Register EnumProof as micromega.ZArithProof.EnumProof.
Register ExProof as micromega.ZArithProof.ExProof.
@@ -1042,13 +1047,14 @@ Fixpoint max_var_prf (w : ZArithProof) : positive :=
match w with
| DoneProof => xH
| RatProof w pf | CutProof w pf => Pos.max (max_var_psatz w) (max_var_prf pf)
- | EnumProof w1 w2 l => List.fold_left (fun acc prf => Pos.max acc (max_var_prf prf)) l
- (Pos.max (max_var_psatz w1) (max_var_psatz w2))
+ | SplitProof p pf1 pf2 => Pos.max (max_var xH p) (Pos.max (max_var_prf pf1) (max_var_prf pf1))
+ | EnumProof w1 w2 l => List.fold_left
+ (fun acc prf => Pos.max acc (max_var_prf prf)) l
+ (Pos.max (max_var_psatz w1) (max_var_psatz w2))
| ExProof _ pf => max_var_prf pf
end.
-
Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool :=
match pf with
| DoneProof => false
@@ -1068,6 +1074,14 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool
| Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf
end
end
+ | SplitProof p pf1 pf2 =>
+ match genCuttingPlane (p,NonStrict) , genCuttingPlane (popp p, NonStrict) with
+ | None , _ | _ , None => false
+ | Some cp1 , Some cp2 =>
+ ZChecker (nformula_of_cutting_plane cp1::l) pf1
+ &&
+ ZChecker (nformula_of_cutting_plane cp2::l) pf2
+ end
| ExProof x prf =>
let fr := max_var_nformulae l in
if Pos.leb x fr then
@@ -1105,6 +1119,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat :=
| DoneProof => O
| RatProof _ p => S (bdepth p)
| CutProof _ p => S (bdepth p)
+ | SplitProof _ p1 p2 => S (Nat.max (bdepth p1) (bdepth p2))
| EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l)
| ExProof _ p => S (bdepth p)
end.
@@ -1140,6 +1155,26 @@ Proof.
apply Nat.le_max_r.
Qed.
+Lemma ltof_bdepth_split_l :
+ forall p pf1 pf2,
+ ltof ZArithProof bdepth pf1 (SplitProof p pf1 pf2).
+Proof.
+ intros.
+ unfold ltof. simpl.
+ rewrite Nat.lt_succ_r.
+ apply Nat.le_max_l.
+Qed.
+
+Lemma ltof_bdepth_split_r :
+ forall p pf1 pf2,
+ ltof ZArithProof bdepth pf2 (SplitProof p pf1 pf2).
+Proof.
+ intros.
+ unfold ltof. simpl.
+ rewrite Nat.lt_succ_r.
+ apply Nat.le_max_r.
+Qed.
+
Lemma eval_Psatz_sound : forall env w l f',
make_conj (eval_nformula env) l ->
@@ -1470,11 +1505,23 @@ Ltac pos_tac :=
apply (Pos2Z.pos_le_pos X Y) in H
end.
+Lemma eval_nformula_split : forall env p,
+ eval_nformula env (p,NonStrict) \/ eval_nformula env (popp p,NonStrict).
+Proof.
+ unfold popp.
+ simpl. intros. rewrite (eval_pol_opp Zsor ZSORaddon).
+ rewrite Z.opp_nonneg_nonpos.
+ apply Z.le_ge_cases.
+Qed.
+
+
+
+
Lemma ZChecker_sound : forall w l,
ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False.
Proof.
induction w using (well_founded_ind (well_founded_ltof _ bdepth)).
- destruct w as [ | w pf | w pf | w1 w2 pf | x pf].
+ destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf].
- (* DoneProof *)
simpl. discriminate.
- (* RatProof *)
@@ -1527,6 +1574,26 @@ Proof.
intros.
apply eval_Psatz_sound with (2:= Hlc) in H2.
apply genCuttingPlaneNone with (2:= H2) ; auto.
+ - (* SplitProof *)
+ intros l.
+ cbn - [genCuttingPlane].
+ case_eq (genCuttingPlane (p, NonStrict)) ; [| discriminate].
+ case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate].
+ intros cp1 GCP1 cp2 GCP2 ZC1 env.
+ flatten_bool.
+ destruct (eval_nformula_split env p).
+ + apply H with (env:=env) in H0.
+ rewrite <- make_conj_impl in *.
+ intro ; apply H0.
+ rewrite make_conj_cons. split; auto.
+ apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto.
+ apply ltof_bdepth_split_l.
+ + apply H with (env:=env) in H1.
+ rewrite <- make_conj_impl in *.
+ intro ; apply H1.
+ rewrite make_conj_cons. split; auto.
+ apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto.
+ apply ltof_bdepth_split_r.
- (* EnumProof *)
intros l.
simpl.
@@ -1758,6 +1825,7 @@ Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat :=
| DoneProof => acc
| RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
| CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
+ | SplitProof p pt1 pt2 => xhyps_of_pt (S base) (xhyps_of_pt (S base) acc pt1) pt2
| EnumProof c1 c2 l =>
let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
List.fold_left (xhyps_of_pt (S base)) l acc
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index dc81b5cca7..db572d25d8 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -671,43 +671,32 @@ Module Export ipat.
Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
(at level 0, only parsing) : ssripat_scope.
-(** We try to preserve the naming by matching the names from the goal.
- We do 'move' to perform a hnf before trying to match. **)
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match *)
Notation "'[' 'swap' ']'" := (ltac:(move;
- lazymatch goal with
- | |- forall (x : _), _ => let x := fresh x in move=> x; move;
- lazymatch goal with
- | |- forall (y : _), _ => let y := fresh y in move=> y; move: y x
- | |- let y := _ in _ => let y := fresh y in move=> y; move: @y x
- | _ => let y := fresh "_top_" in move=> y; move: y x
- end
- | |- let x := _ in _ => let x := fresh x in move => x; move;
- lazymatch goal with
- | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
- | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
- | _ => let y := fresh "_top_" in move=> y; move: y x
- end
- | _ => let x := fresh "_top_" in let x := fresh x in move=> x; move;
- lazymatch goal with
- | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
- | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
- | _ => let y := fresh "_top_" in move=> y; move: y x
- end
- end))
+ let x := lazymatch goal with
+ | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_"
+ end in intro x; move;
+ let y := lazymatch goal with
+ | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_"
+ end in intro y; revert x; revert y))
(at level 0, only parsing) : ssripat_scope.
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match *)
Notation "'[' 'dup' ']'" := (ltac:(move;
lazymatch goal with
| |- forall (x : _), _ =>
- let x := fresh x in move=> x;
- let copy := fresh x in have copy := x; move: copy x
+ let x := fresh x in intro x;
+ let copy := fresh x in have copy := x; revert x; revert copy
| |- let x := _ in _ =>
- let x := fresh x in move=> x;
+ let x := fresh x in intro x;
let copy := fresh x in pose copy := x;
- do [unfold x in (value of copy)]; move: @copy @x
+ do [unfold x in (value of copy)]; revert x; revert copy
| |- _ =>
let x := fresh "_top_" in move=> x;
- let copy := fresh "_top" in have copy := x; move: copy x
+ let copy := fresh "_top" in have copy := x; revert x; revert copy
end))
(at level 0, only parsing) : ssripat_scope.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:23:42 +0000