Commit f535480f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use definitions for min and max, assuming the relation is a total order.

parent 100c3825
...@@ -1741,7 +1741,6 @@ STDLIBS = algebra \ ...@@ -1741,7 +1741,6 @@ STDLIBS = algebra \
bag \ bag \
bintree \ bintree \
bool \ bool \
comparison \
floating_point \ floating_point \
graph \ graph \
int \ int \
......
...@@ -210,6 +210,13 @@ theory real.Abs ...@@ -210,6 +210,13 @@ theory real.Abs
end 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 theory real.FromInt
syntax function from_int "(Reals.Raxioms.IZR %1)" syntax function from_int "(Reals.Raxioms.IZR %1)"
......
...@@ -182,10 +182,12 @@ theory real.MinMax ...@@ -182,10 +182,12 @@ theory real.MinMax
syntax function min "min(%1,%2)" syntax function min "min(%1,%2)"
syntax function max "max(%1,%2)" syntax function max "max(%1,%2)"
remove prop Max_is_ge remove prop Max_r
remove prop Max_is_some remove prop Min_l
remove prop Min_is_le remove prop Max_comm
remove prop Min_is_some remove prop Min_comm
remove prop Max_assoc
remove prop Min_assoc
end end
(* support for integers disabled because may be inconsistent (* support for integers disabled because may be inconsistent
......
...@@ -157,10 +157,12 @@ theory real.MinMax ...@@ -157,10 +157,12 @@ theory real.MinMax
syntax function min "min(%1, %2)" syntax function min "min(%1, %2)"
syntax function max "max(%1, %2)" syntax function max "max(%1, %2)"
remove prop Max_is_ge remove prop Max_r
remove prop Max_is_some remove prop Min_l
remove prop Min_is_le remove prop Max_comm
remove prop Min_is_some remove prop Min_comm
remove prop Max_assoc
remove prop Min_assoc
end end
theory real.RealInfix theory real.RealInfix
......
theory MinMax 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 -> goal G : forall x y z : t. ge z y -> ge z x -> ge y x ->
min x (max (min z x) y) = x min x (max (min z x) y) = x
......
...@@ -4,83 +4,73 @@ Require Import BuiltIn. ...@@ -4,83 +4,73 @@ Require Import BuiltIn.
Require BuiltIn. Require BuiltIn.
Require int.Int. Require int.Int.
(* Why3 comment *)
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
(* Why3 comment *) (* Why3 comment *)
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *) (* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
(* Why3 goal *) (* Why3 goal *)
Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (ZArith.BinInt.Z.max x y))%Z /\ Lemma max_def : forall (x:Z) (y:Z), ((y <= x)%Z ->
(y <= (ZArith.BinInt.Z.max x y))%Z. ((ZArith.BinInt.Z.max x y) = x)) /\ ((~ (y <= x)%Z) ->
split. ((ZArith.BinInt.Z.max x y) = y)).
apply Zle_max_l. Proof.
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).
intros x y. intros x y.
unfold Zmax. split ; intros H.
case Zcompare. now apply Zmax_l.
now left. apply Zmax_r.
now right. omega.
now left.
Qed. Qed.
(* Why3 goal *) (* Why3 comment *)
Lemma Min_is_le : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) <= x)%Z /\ (* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
((ZArith.BinInt.Z.min x y) <= y)%Z.
split.
apply Zle_min_l.
apply Zle_min_r.
Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Min_is_some : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = x) \/ Lemma min_def : forall (x:Z) (y:Z), ((y <= x)%Z ->
((ZArith.BinInt.Z.min x y) = y). ((ZArith.BinInt.Z.min x y) = y)) /\ ((~ (y <= x)%Z) ->
((ZArith.BinInt.Z.min x y) = x)).
Proof.
intros x y. intros x y.
unfold Zmin. split ; intros H.
case Zcompare. now apply Zmin_r.
now left. apply Zmin_l.
now left. omega.
now right.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> Lemma Max_r : forall (x:Z) (y:Z), (x <= y)%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 ->
((ZArith.BinInt.Z.max x y) = y). ((ZArith.BinInt.Z.max x y) = y).
exact Zmax_r. exact Zmax_r.
Qed. Qed.
(* Why3 goal *) (* 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). ((ZArith.BinInt.Z.min x y) = x).
exact Zmin_l. exact Zmin_l.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> Lemma Max_comm : forall (x:Z) (y:Z),
((ZArith.BinInt.Z.min x y) = y).
exact Zmin_r.
Qed.
(* Why3 goal *)
Lemma Max_sym : forall (x:Z) (y:Z),
((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)). ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
exact Zmax_comm. exact Zmax_comm.
Qed. Qed.
(* Why3 goal *) (* 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)). ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
exact Zmin_comm. exact Zmin_comm.
Qed. 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.
...@@ -6,51 +6,109 @@ Require real.Real. ...@@ -6,51 +6,109 @@ Require real.Real.
Require Import Rbasic_fun. Require Import Rbasic_fun.
(* Why3 comment *)
(* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *)
(* Why3 goal *) (* Why3 goal *)
Definition min: R -> R -> R. Lemma max_def : forall (x:R) (y:R), ((y <= x)%R ->
exact Rmin. ((Reals.Rbasic_fun.Rmax x y) = x)) /\ ((~ (y <= x)%R) ->
Defined. ((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 *) (* Why3 goal *)
Definition max: R -> R -> R. Lemma min_def : forall (x:R) (y:R), ((y <= x)%R ->
exact Rmax. ((Reals.Rbasic_fun.Rmin x y) = y)) /\ ((~ (y <= x)%R) ->
Defined. ((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 *) (* Why3 goal *)
Lemma Max_is_ge : forall (x:R) (y:R), (x <= (max x y))%R /\ (y <= (max x Lemma Max_r : forall (x:R) (y:R), (x <= y)%R ->
y))%R. ((Reals.Rbasic_fun.Rmax x y) = y).
split. exact Rmax_right.
apply Rmax_l.
apply Rmax_r.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Max_is_some : forall (x:R) (y:R), ((max x y) = x) \/ ((max x y) = y). Lemma Min_l : forall (x:R) (y:R), (x <= y)%R ->
intros x y. ((Reals.Rbasic_fun.Rmin x y) = x).
destruct (Rle_or_lt x y) as [H|H]. exact Rmin_left.
right.
now apply Rmax_right.
left.
apply Rmax_left.
now apply Rlt_le.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Min_is_le : forall (x:R) (y:R), ((min x y) <= x)%R /\ ((min x Lemma Max_comm : forall (x:R) (y:R),
y) <= y)%R. ((Reals.Rbasic_fun.Rmax x y) = (Reals.Rbasic_fun.Rmax y x)).
split. exact Rmax_comm.
apply Rmin_l.
apply Rmin_r.
Qed. Qed.
(* Why3 goal *) (* 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. intros x y.
destruct (Rle_or_lt x y) as [H|H]. destruct (Rle_or_lt x y) as [H|H].
left. rewrite Rmin_left, Rmax_left.
now apply Rmin_left. apply eq_sym, Ropp_involutive.
right. now apply Ropp_le_contravar.
apply Rmin_right. exact H.
rewrite Rmin_right, Rmax_right.
apply eq_sym, Ropp_involutive.
now apply Ropp_le_contravar, Rlt_le.
now apply Rlt_le. now apply Rlt_le.
Qed. 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.
...@@ -68,25 +68,17 @@ section {* Minimum and Maximum *} ...@@ -68,25 +68,17 @@ section {* Minimum and Maximum *}
why3_open "int/MinMax.xml" 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_assoc 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_end why3_end
......
(** {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
...@@ -45,7 +45,11 @@ end ...@@ -45,7 +45,11 @@ end
theory MinMax theory MinMax
use import Int 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 end
......
...@@ -81,14 +81,11 @@ end ...@@ -81,14 +81,11 @@ end
theory MinMax theory MinMax
use import Real use import Real
clone export relations.MinMax with type t = real, predicate ge = (>=),
function min real real : real goal TotalOrder.Refl,
function max real real : real goal TotalOrder.Trans,
goal TotalOrder.Antisymm,
axiom Max_is_ge : forall x y:real. max x y >= x /\ max x y >= y goal TotalOrder.Total
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
end end
......
...@@ -134,16 +134,28 @@ theory Lex ...@@ -134,16 +134,28 @@ theory Lex
end end
(*** (** {2 Minimum and maximum for total orders} *)
theory MinMax 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 lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)
function max t t : t lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
end end
*)
(** {2 Well-founded relation} *) (** {2 Well-founded relation} *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment