diff --git a/Makefile.in b/Makefile.in index 84899e0a3098c217e3e1555f5d072c0ccb775b92..c7c131124fb82cc64169d015f029a1f93f76b002 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1741,7 +1741,6 @@ STDLIBS = algebra \ bag \ bintree \ bool \ - comparison \ floating_point \ graph \ int \ diff --git a/drivers/coq-common.gen b/drivers/coq-common.gen index 0c11ed84b46595771d8faa9a9fc0c101139a49f4..d02e7ee059f16a58da86c84da0d8965148ad2fa0 100644 --- a/drivers/coq-common.gen +++ b/drivers/coq-common.gen @@ -210,6 +210,13 @@ theory real.Abs end +theory real.MinMax + + syntax function min "(Reals.Rbasic_fun.Rmin %1 %2)" + syntax function max "(Reals.Rbasic_fun.Rmax %1 %2)" + +end + theory real.FromInt syntax function from_int "(Reals.Raxioms.IZR %1)" diff --git a/drivers/metitarski.drv b/drivers/metitarski.drv index c915989373bd19df519fd412c12b4a02f76134a9..6ab64e7cc6d230d4ae4ca189226dd63482f0fc32 100644 --- a/drivers/metitarski.drv +++ b/drivers/metitarski.drv @@ -182,10 +182,12 @@ theory real.MinMax syntax function min "min(%1,%2)" syntax function max "max(%1,%2)" - remove prop Max_is_ge - remove prop Max_is_some - remove prop Min_is_le - remove prop Min_is_some + remove prop Max_r + remove prop Min_l + remove prop Max_comm + remove prop Min_comm + remove prop Max_assoc + remove prop Min_assoc end (* support for integers disabled because may be inconsistent diff --git a/drivers/pvs-common.gen b/drivers/pvs-common.gen index 100ce18e4209e398f26e91e142be0da71cb417e7..8f3d6d612001e7c755f39ce9cb885a6dd2411552 100644 --- a/drivers/pvs-common.gen +++ b/drivers/pvs-common.gen @@ -157,10 +157,12 @@ theory real.MinMax syntax function min "min(%1, %2)" syntax function max "max(%1, %2)" - remove prop Max_is_ge - remove prop Max_is_some - remove prop Min_is_le - remove prop Min_is_some + remove prop Max_r + remove prop Min_l + remove prop Max_comm + remove prop Min_comm + remove prop Max_assoc + remove prop Min_assoc end theory real.RealInfix diff --git a/examples/check-builtin/minmax.why b/examples/check-builtin/minmax.why index 3bc6a62f07ce2369d29cf061e85034284e067a24..220a2f26d3722585330a33f8e8eae1747ed91f99 100644 --- a/examples/check-builtin/minmax.why +++ b/examples/check-builtin/minmax.why @@ -1,5 +1,5 @@ theory MinMax - use import comparison.MinMax + use import relations.MinMax goal G : forall x y z : t. ge z y -> ge z x -> ge y x -> min x (max (min z x) y) = x diff --git a/lib/coq/int/MinMax.v b/lib/coq/int/MinMax.v index 6bd69795d283b9c721b09476d67068ef737df9d8..5f70adc78d549ee68a9cde9ede94bf1ad221e151 100644 --- a/lib/coq/int/MinMax.v +++ b/lib/coq/int/MinMax.v @@ -4,83 +4,73 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. -(* Why3 comment *) -(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *) - (* Why3 comment *) (* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *) (* Why3 goal *) -Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (ZArith.BinInt.Z.max x y))%Z /\ - (y <= (ZArith.BinInt.Z.max x y))%Z. -split. -apply Zle_max_l. -apply Zle_max_r. -Qed. - -(* Why3 goal *) -Lemma Max_is_some : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = x) \/ - ((ZArith.BinInt.Z.max x y) = y). +Lemma max_def : forall (x:Z) (y:Z), ((y <= x)%Z -> + ((ZArith.BinInt.Z.max x y) = x)) /\ ((~ (y <= x)%Z) -> + ((ZArith.BinInt.Z.max x y) = y)). +Proof. intros x y. -unfold Zmax. -case Zcompare. -now left. -now right. -now left. +split ; intros H. +now apply Zmax_l. +apply Zmax_r. +omega. Qed. -(* Why3 goal *) -Lemma Min_is_le : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) <= x)%Z /\ - ((ZArith.BinInt.Z.min x y) <= y)%Z. -split. -apply Zle_min_l. -apply Zle_min_r. -Qed. +(* Why3 comment *) +(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *) (* Why3 goal *) -Lemma Min_is_some : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = x) \/ - ((ZArith.BinInt.Z.min x y) = y). +Lemma min_def : forall (x:Z) (y:Z), ((y <= x)%Z -> + ((ZArith.BinInt.Z.min x y) = y)) /\ ((~ (y <= x)%Z) -> + ((ZArith.BinInt.Z.min x y) = x)). +Proof. intros x y. -unfold Zmin. -case Zcompare. -now left. -now left. -now right. +split ; intros H. +now apply Zmin_r. +apply Zmin_l. +omega. Qed. (* Why3 goal *) -Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> - ((ZArith.BinInt.Z.max x y) = x). -exact Zmax_l. -Qed. - -(* Why3 goal *) -Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> +Lemma Max_r : forall (x:Z) (y:Z), (x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y). exact Zmax_r. Qed. (* Why3 goal *) -Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> +Lemma Min_l : forall (x:Z) (y:Z), (x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x). exact Zmin_l. Qed. (* Why3 goal *) -Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> - ((ZArith.BinInt.Z.min x y) = y). -exact Zmin_r. -Qed. - -(* Why3 goal *) -Lemma Max_sym : forall (x:Z) (y:Z), +Lemma Max_comm : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)). exact Zmax_comm. Qed. (* Why3 goal *) -Lemma Min_sym : forall (x:Z) (y:Z), +Lemma Min_comm : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)). exact Zmin_comm. Qed. +(* Why3 goal *) +Lemma Max_assoc : forall (x:Z) (y:Z) (z:Z), + ((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) = (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))). +Proof. +intros x y z. +apply eq_sym, Zmax_assoc. +Qed. + +(* Why3 goal *) +Lemma Min_assoc : forall (x:Z) (y:Z) (z:Z), + ((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) = (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))). +Proof. +intros x y z. +apply eq_sym, Zmin_assoc. +Qed. + diff --git a/lib/coq/real/MinMax.v b/lib/coq/real/MinMax.v index 900880f093a0b307c0161544e870cc41e8198a46..32521486fb2b715d8b0789a2e3804c7e6722ff4e 100644 --- a/lib/coq/real/MinMax.v +++ b/lib/coq/real/MinMax.v @@ -6,51 +6,109 @@ Require real.Real. Require Import Rbasic_fun. +(* Why3 comment *) +(* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *) + (* Why3 goal *) -Definition min: R -> R -> R. -exact Rmin. -Defined. +Lemma max_def : forall (x:R) (y:R), ((y <= x)%R -> + ((Reals.Rbasic_fun.Rmax x y) = x)) /\ ((~ (y <= x)%R) -> + ((Reals.Rbasic_fun.Rmax x y) = y)). +Proof. +intros x y. +split ; intros H. +now apply Rmax_left. +apply Rmax_right. +now apply Rlt_le, Rnot_le_lt. +Qed. + +(* Why3 comment *) +(* min is replaced with (Reals.Rbasic_fun.Rmin x x1) by the coq driver *) (* Why3 goal *) -Definition max: R -> R -> R. -exact Rmax. -Defined. +Lemma min_def : forall (x:R) (y:R), ((y <= x)%R -> + ((Reals.Rbasic_fun.Rmin x y) = y)) /\ ((~ (y <= x)%R) -> + ((Reals.Rbasic_fun.Rmin x y) = x)). +Proof. +intros x y. +split ; intros H. +now apply Rmin_right. +apply Rmin_left. +now apply Rlt_le, Rnot_le_lt. +Qed. (* Why3 goal *) -Lemma Max_is_ge : forall (x:R) (y:R), (x <= (max x y))%R /\ (y <= (max x - y))%R. -split. -apply Rmax_l. -apply Rmax_r. +Lemma Max_r : forall (x:R) (y:R), (x <= y)%R -> + ((Reals.Rbasic_fun.Rmax x y) = y). +exact Rmax_right. Qed. (* Why3 goal *) -Lemma Max_is_some : forall (x:R) (y:R), ((max x y) = x) \/ ((max x y) = y). -intros x y. -destruct (Rle_or_lt x y) as [H|H]. -right. -now apply Rmax_right. -left. -apply Rmax_left. -now apply Rlt_le. +Lemma Min_l : forall (x:R) (y:R), (x <= y)%R -> + ((Reals.Rbasic_fun.Rmin x y) = x). +exact Rmin_left. Qed. (* Why3 goal *) -Lemma Min_is_le : forall (x:R) (y:R), ((min x y) <= x)%R /\ ((min x - y) <= y)%R. -split. -apply Rmin_l. -apply Rmin_r. +Lemma Max_comm : forall (x:R) (y:R), + ((Reals.Rbasic_fun.Rmax x y) = (Reals.Rbasic_fun.Rmax y x)). +exact Rmax_comm. Qed. (* Why3 goal *) -Lemma Min_is_some : forall (x:R) (y:R), ((min x y) = x) \/ ((min x y) = y). +Lemma Min_comm : forall (x:R) (y:R), + ((Reals.Rbasic_fun.Rmin x y) = (Reals.Rbasic_fun.Rmin y x)). +exact Rmin_comm. +Qed. + +(* Why3 goal *) +Lemma Max_assoc : forall (x:R) (y:R) (z:R), + ((Reals.Rbasic_fun.Rmax (Reals.Rbasic_fun.Rmax x y) z) = (Reals.Rbasic_fun.Rmax x (Reals.Rbasic_fun.Rmax y z))). +Proof. +intros x y z. +destruct (Rle_or_lt x y) as [Hxy|Hxy]. +rewrite Rmax_right with (1 := Hxy). +apply eq_sym, Rmax_right. +apply Rle_trans with (1 := Hxy). +apply Rmax_l. +rewrite (Rmax_left x y) by now apply Rlt_le. +destruct (Rle_or_lt x z) as [Hxz|Hxz]. +rewrite Rmax_right with (1 := Hxz). +rewrite Rmax_right. +apply eq_sym, Rmax_right. +apply Rlt_le. +now apply Rlt_le_trans with x. +apply Rle_trans with (1 := Hxz). +apply Rmax_r. +rewrite Rmax_left. +apply eq_sym, Rmax_left. +apply Rmax_case ; now apply Rlt_le. +now apply Rlt_le. +Qed. + +Lemma Rmin_max_opp : + forall x y : R, + Rmin x y = Ropp (Rmax (-x) (-y)). +Proof. intros x y. destruct (Rle_or_lt x y) as [H|H]. -left. -now apply Rmin_left. -right. -apply Rmin_right. +rewrite Rmin_left, Rmax_left. +apply eq_sym, Ropp_involutive. +now apply Ropp_le_contravar. +exact H. +rewrite Rmin_right, Rmax_right. +apply eq_sym, Ropp_involutive. +now apply Ropp_le_contravar, Rlt_le. now apply Rlt_le. Qed. +(* Why3 goal *) +Lemma Min_assoc : forall (x:R) (y:R) (z:R), + ((Reals.Rbasic_fun.Rmin (Reals.Rbasic_fun.Rmin x y) z) = (Reals.Rbasic_fun.Rmin x (Reals.Rbasic_fun.Rmin y z))). +Proof. +intros x y z. +rewrite !Rmin_max_opp. +apply f_equal. +rewrite !Ropp_involutive. +apply Max_assoc. +Qed. + diff --git a/lib/isabelle/Why3_Int.thy b/lib/isabelle/Why3_Int.thy index 134d7e0b43826a569b4168f3f032ce44365852be..98567d1e4f1afe6d2430355af6af9e9a47515fe3 100644 --- a/lib/isabelle/Why3_Int.thy +++ b/lib/isabelle/Why3_Int.thy @@ -68,25 +68,17 @@ section {* Minimum and Maximum *} why3_open "int/MinMax.xml" -why3_vc Max_x using assms by simp +why3_vc Max_r using assms by simp -why3_vc Max_y using assms by simp +why3_vc Max_comm by simp -why3_vc Max_sym by simp +why3_vc Max_assoc by simp -why3_vc Max_is_ge by simp_all +why3_vc Min_l using assms by simp -why3_vc Max_is_some by auto +why3_vc Min_comm by simp -why3_vc Min_x using assms by simp - -why3_vc Min_y using assms by simp - -why3_vc Min_sym by simp - -why3_vc Min_is_le by simp_all - -why3_vc Min_is_some by auto +why3_vc Min_assoc by simp why3_end diff --git a/theories/comparison.why b/theories/comparison.why deleted file mode 100644 index e5f891f74e59f5a684e45c967de5f1201a212a45..0000000000000000000000000000000000000000 --- a/theories/comparison.why +++ /dev/null @@ -1,60 +0,0 @@ - -(** {1 Comparison Operators, Order relations} *) - -(** {2 Absolute value} *) - -theory Abs - - type t - predicate ge t t - function neg t : t - constant zero : t - - function abs t : t - - axiom Pos: forall x:t. ge x zero -> abs x = x - axiom Neg: forall x:t. not ge x zero -> abs x = neg x - -(*** - function abs(x : t) : t - axiom Abs_def : if ge x zero then abs x = x else abs x = neg x -*) - -end - -(** {2 Minimum and maximum} *) - -theory MinMax - - type t - predicate ge t t - - function min t t : t - function max t t : t - - axiom Max_is_ge : forall x y:t. ge (max x y) x /\ ge (max x y) y - axiom Max_is_some : forall x y:t. max x y = x \/ max x y = y - axiom Min_is_le : forall x y:t. ge x (min x y) /\ ge y (min x y) - axiom Min_is_some : forall x y:t. min x y = x \/ min x y = y - - axiom Max_x : forall x y:t. ge x y -> max x y = x - axiom Max_y : forall x y:t. ge y x -> max x y = y - axiom Min_x : forall x y:t. ge y x -> min x y = x - axiom Min_y : forall x y:t. ge x y -> min x y = y - - lemma Max_sym: forall x y:t. max x y = max y x - lemma Min_sym: forall x y:t. min x y = min y x - -(*** - function min (x y : t) : t - axiom Min_def : if ge x y then min x y = y else min x y = x - function max (x y : t) : t - axiom Max_def : if ge x y then max x y = x else max x y = y -*) - -(*** - function min (x y : t) : t = if ge x y then y else x - function max (x y : t) : t = if ge x y then x else y -*) - -end diff --git a/theories/int.why b/theories/int.why index a8ffe30758dff4785a04d5f095aa4be7b8556194..707778a55edeb73b24c68653e953170375472db6 100644 --- a/theories/int.why +++ b/theories/int.why @@ -45,7 +45,11 @@ end theory MinMax use import Int - clone export comparison.MinMax with type t = int, predicate ge = (>=) + clone export relations.MinMax with type t = int, predicate ge = (>=), + goal TotalOrder.Refl, + goal TotalOrder.Trans, + goal TotalOrder.Antisymm, + goal TotalOrder.Total end diff --git a/theories/real.why b/theories/real.why index f6739d65ba3090940befaa88c1fdda635c89d67d..4c75606e68a19f48d5d07856f7c0a76cb4a9cfb1 100644 --- a/theories/real.why +++ b/theories/real.why @@ -81,14 +81,11 @@ end theory MinMax use import Real - - function min real real : real - function max real real : real - - axiom Max_is_ge : forall x y:real. max x y >= x /\ max x y >= y - axiom Max_is_some : forall x y:real. max x y = x \/ max x y = y - axiom Min_is_le : forall x y:real. min x y <= x /\ min x y <= y - axiom Min_is_some : forall x y:real. min x y = x \/ min x y = y + clone export relations.MinMax with type t = real, predicate ge = (>=), + goal TotalOrder.Refl, + goal TotalOrder.Trans, + goal TotalOrder.Antisymm, + goal TotalOrder.Total end diff --git a/theories/relations.why b/theories/relations.why index 3fc80cca273503811d414c6795a3f43147069370..c5f5e0fe7261070a7ee7e85e33a277e9f67a497f 100644 --- a/theories/relations.why +++ b/theories/relations.why @@ -134,16 +134,28 @@ theory Lex end -(*** +(** {2 Minimum and maximum for total orders} *) + theory MinMax - clone export TotalOrder + type t + predicate ge t t + + clone TotalOrder with type t = t, predicate rel = ge + + function max (x y : t) : t = if ge x y then x else y + function min (x y : t) : t = if ge x y then y else x + + lemma Max_r : forall x y:t. ge y x -> max x y = y + lemma Min_l : forall x y:t. ge y x -> min x y = x + + lemma Max_comm : forall x y:t. max x y = max y x + lemma Min_comm : forall x y:t. min x y = min y x - function min t t : t - function max t t : t + lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z) + lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z) end -*) (** {2 Well-founded relation} *)