Commit decda325 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'minmax'

parents ce13ca28 cf86a47e
......@@ -1741,7 +1741,6 @@ STDLIBS = algebra \
bag \
bintree \
bool \
comparison \
floating_point \
graph \
int \
......
......@@ -153,6 +153,10 @@ goods modules
goods modules/mach
echo ""
echo "=== Checking drivers ==="
drivers drivers
echo ""
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
goods bench/programs/bad-typing --parse-only
......@@ -214,10 +218,6 @@ extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
echo ""
echo "=== Checking drivers ==="
drivers drivers
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
......
......@@ -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)"
......
......@@ -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
......
......@@ -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
......
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
......
......@@ -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.
......@@ -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.
......@@ -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
......
(** {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
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
......
......@@ -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
......
(** {1 Relations} *)
(** {2 Relations and orders} *)
theory EndoRelation
type t
......@@ -83,6 +84,8 @@ theory Inverse
predicate inv_rel (x y : t) = rel y x
end
(** {2 Closures} *)
theory ReflClosure
clone export EndoRelation
......@@ -113,63 +116,7 @@ theory ReflTransClosure
forall x y z: t. relTR x y -> relTR y z -> relTR x z
end
(***
theory PreOrder
type t
predicate le t t
axiom Refl : forall x:t. le(x,x)
axiom Trans : forall x y z:t. le x y /\ le y z -> le x z
end
theory Equiv
type t
predicate eq t t
clone PreOrder with type t = t, predicate le = eq
axiom Symm : forall x y:t. eq x y -> eq y x
end
theory TotalPreOrder
type t
predicate le t t
clone export PreOrder with type t = t, predicate le = le
axiom Totality: forall x y:t. le x y \/ le y x
end
*)
(***
theory TotalOrder
type t
predicate eq t t
clone Equiv with type t = t, predicate eq = eq
predicate le t t
clone PreOrder with type t = t, predicate le = le
axiom Totality: forall x y:t. eq x y \/ le x y \/ le y x
predicate lt (x y : t) = le x y /\ not eq x y
lemma Lt_antirefl: forall x:t. not lt x x
lemma Lt_trans: forall x y z:t. lt x y /\ lt y z -> lt x z
lemma Le_lt_trans: forall x y z:t. le x y /\ lt y z -> lt x z
lemma Lt_le_trans: forall x y z:t. lt x y /\ le y z -> lt x z
end
*)
(** {2 Lexicographic ordering} *)
theory Lex
......@@ -187,16 +134,30 @@ 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
function min t t : t
function max t t : t
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_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} *)
theory WellFounded
......
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