Commit 17c6239f authored by Andrei Paskevich's avatar Andrei Paskevich

relations.MinMax: define in terms of (<=), not (>=)

- update Coq and Isabelle realizations (TODO: PVS)
parent d8dc17b3
......@@ -182,8 +182,8 @@ theory real.MinMax
syntax function min "min(%1,%2)"
syntax function max "max(%1,%2)"
remove prop Max_r
remove prop Min_l
remove prop Max_l
remove prop Min_r
remove prop Max_comm
remove prop Min_comm
remove prop Max_assoc
......
......@@ -157,8 +157,8 @@ theory real.MinMax
syntax function min "min(%1, %2)"
syntax function max "max(%1, %2)"
remove prop Max_r
remove prop Min_l
remove prop Max_l
remove prop Min_r
remove prop Max_comm
remove prop Min_comm
remove prop Max_assoc
......
......@@ -5,51 +5,45 @@ Require BuiltIn.
Require int.Int.
(* Why3 comment *)
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
(* Why3 goal *)
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)).
Lemma min_def : forall (x:Z) (y:Z), ((x <= y)%Z ->
((ZArith.BinInt.Z.min x y) = x)) /\ ((~ (x <= y)%Z) ->
((ZArith.BinInt.Z.min x y) = y)).
Proof.
intros x y.
split ; intros H.
now apply Zmax_l.
apply Zmax_r.
now apply Zmin_l.
apply Zmin_r.
omega.
Qed.
(* Why3 comment *)
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
(* Why3 goal *)
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)).
Lemma max_def : forall (x:Z) (y:Z), ((x <= y)%Z ->
((ZArith.BinInt.Z.max x y) = y)) /\ ((~ (x <= y)%Z) ->
((ZArith.BinInt.Z.max x y) = x)).
Proof.
intros x y.
split ; intros H.
now apply Zmin_r.
apply Zmin_l.
now apply Zmax_r.
apply Zmax_l.
omega.
Qed.
(* Why3 goal *)
Lemma Max_r : forall (x:Z) (y:Z), (x <= y)%Z ->
((ZArith.BinInt.Z.max x y) = y).
exact Zmax_r.
Lemma Min_r : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.min x y) = y).
exact Zmin_r.
Qed.
(* Why3 goal *)
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 Max_comm : forall (x:Z) (y:Z),
((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
exact Zmax_comm.
Lemma Max_l : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.max x y) = x).
exact Zmax_l.
Qed.
(* Why3 goal *)
......@@ -59,11 +53,9 @@ 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.
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 *)
......@@ -74,3 +66,11 @@ intros x y z.
apply eq_sym, Zmin_assoc.
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.
......@@ -7,45 +7,51 @@ Require real.Real.
Require Import Rbasic_fun.
(* Why3 comment *)
(* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *)
(* min is replaced with (Reals.Rbasic_fun.Rmin x x1) by the coq driver *)
(* Why3 goal *)
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)).
Lemma min_def : forall (x:R) (y:R), ((x <= y)%R ->
((Reals.Rbasic_fun.Rmin x y) = x)) /\ ((~ (x <= y)%R) ->
((Reals.Rbasic_fun.Rmin x y) = y)).
Proof.
intros x y.
split ; intros H.
now apply Rmax_left.
apply Rmax_right.
now apply Rmin_left.
apply Rmin_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 *)
(* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *)
(* Why3 goal *)
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)).
Lemma max_def : forall (x:R) (y:R), ((x <= y)%R ->
((Reals.Rbasic_fun.Rmax x y) = y)) /\ ((~ (x <= y)%R) ->
((Reals.Rbasic_fun.Rmax x y) = x)).
Proof.
intros x y.
split ; intros H.
now apply Rmin_right.
apply Rmin_left.
now apply Rmax_right.
apply Rmax_left.
now apply Rlt_le, Rnot_le_lt.
Qed.
(* Why3 goal *)
Lemma Max_r : forall (x:R) (y:R), (x <= y)%R ->
((Reals.Rbasic_fun.Rmax x y) = y).
exact Rmax_right.
Lemma Min_r : forall (x:R) (y:R), (y <= x)%R ->
((Reals.Rbasic_fun.Rmin x y) = y).
exact Rmin_right.
Qed.
(* Why3 goal *)
Lemma Min_l : forall (x:R) (y:R), (x <= y)%R ->
((Reals.Rbasic_fun.Rmin x y) = x).
exact Rmin_left.
Lemma Max_l : forall (x:R) (y:R), (y <= x)%R ->
((Reals.Rbasic_fun.Rmax x y) = x).
exact Rmax_left.
Qed.
(* Why3 goal *)
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 *)
......@@ -55,9 +61,25 @@ exact Rmax_comm.
Qed.
(* Why3 goal *)
Lemma Min_comm : forall (x:R) (y:R),
((Reals.Rbasic_fun.Rmin x y) = (Reals.Rbasic_fun.Rmin y x)).
exact Rmin_comm.
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.
destruct (Rle_or_lt x y) as [Hxy|Hxy].
rewrite Rmin_left with (1 := Hxy).
destruct (Rle_or_lt x z) as [Hxz|Hxz].
rewrite Rmin_left with (1 := Hxz).
apply eq_sym, Rmin_left.
now apply Rmin_case.
rewrite (Rmin_right y z).
reflexivity.
apply Rlt_le.
now apply Rlt_le_trans with x.
rewrite (Rmin_right x y) by now apply Rlt_le.
apply eq_sym, Rmin_right.
apply Rlt_le.
apply Rle_lt_trans with (2 := Hxy).
apply Rmin_l.
Qed.
(* Why3 goal *)
......@@ -85,30 +107,3 @@ 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].
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.
......@@ -68,13 +68,13 @@ section {* Minimum and Maximum *}
why3_open "int/MinMax.xml"
why3_vc Max_r using assms by simp
why3_vc Max_l using assms by simp
why3_vc Max_comm by simp
why3_vc Max_assoc by simp
why3_vc Min_l using assms by simp
why3_vc Min_r using assms by simp
why3_vc Min_comm by simp
......
......@@ -45,7 +45,7 @@ end
theory MinMax
use import Int
clone export relations.MinMax with type t = int, predicate ge = (>=),
clone export relations.MinMax with type t = int, predicate le = (<=),
goal TotalOrder.Refl,
goal TotalOrder.Trans,
goal TotalOrder.Antisymm,
......
......@@ -81,7 +81,7 @@ end
theory MinMax
use import Real
clone export relations.MinMax with type t = real, predicate ge = (>=),
clone export relations.MinMax with type t = real, predicate le = (<=),
goal TotalOrder.Refl,
goal TotalOrder.Trans,
goal TotalOrder.Antisymm,
......
......@@ -139,21 +139,21 @@ end
theory MinMax
type t
predicate ge t t
predicate le t t
clone TotalOrder with type t = t, predicate rel = ge
clone TotalOrder with type t = t, predicate rel = le
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
function min (x y : t) : t = if le x y then x else y
function max (x y : t) : t = if le 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 Min_r : forall x y:t. le y x -> min x y = y
lemma Max_l : forall x y:t. le y x -> max 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
lemma Max_comm : forall x y:t. max x y = max y x
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)
lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)
end
......
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