Commit 3438e2db authored by Martin Clochard's avatar Martin Clochard
parents 22223efb 17c6239f
......@@ -944,31 +944,31 @@ clean:: clean-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp
update-coq-int: bin/why3 drivers/coq-realizations.aux theories/int.why
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
update-coq-bool: bin/why3 drivers/coq-realizations.aux theories/bool.why
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done
update-coq-real: bin/why3 drivers/coq-realizations.aux theories/real.why
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
update-coq-number: bin/why3 drivers/coq-realizations.aux theories/number.why
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-map: bin/why3 drivers/coq-realizations.aux theories/map.why
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
update-coq-list: bin/why3 drivers/coq-realizations.aux theories/list.why
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
update-coq-option: bin/why3 drivers/coq-realizations.aux theories/option.why
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
update-coq-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......@@ -1042,12 +1042,12 @@ install_no_local::
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3 drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
else
......@@ -1116,62 +1116,61 @@ drivers/isabelle-realizations.aux: Makefile
install_no_local::
cp -r lib/isabelle "$(LIBDIR)/why3"
cp drivers/isabelle-realizations.aux "$(DATADIR)/why3/drivers/"
@(d=`isabelle components -l | grep why3 | sed -e 's/^ *//' `; \
if test "$$d" != "$(LIBDIR)/why3/isabelle"; then \
echo "[Warning] Cannot pre-build the Isabelle heap because the"; \
echo " current Why3 path in Isabelle component configuration [$$d]"; \
echo " is not the same as the current install dir [$(LIBDIR)/why3/isabelle]"; \
else (isabelle build -bc Why3 ; true) \
@(if isabelle components -l | grep -q "$(LIBDIR)/why3/isabelle$$"; then \
isabelle build -bc Why3; true; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [$(LIBDIR)/why3/isabelle]"; \
fi)
install_local::
@(d=`isabelle components -l | grep why3 | sed -e 's/^ *//'`; \
if test "$$d" != "`pwd`/lib/isabelle"; then \
echo "[Warning] Cannot pre-build the Isabelle heap because the"; \
echo " current Why3 path in Isabelle component configuration [$$d]"; \
echo " is not the same as the current install dir [`pwd`/lib/isabelle]"; \
else (isabelle build -bc Why3 ; true)\
@(if isabelle components -l | grep -q "`pwd`/lib/isabelle$$"; then \
isabelle build -bc Why3; true; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [`pwd`/lib/isabelle]"; \
fi)
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
$(ISABELLELIBS_INT): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3 drivers/isabelle-realizations.aux \
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
......
......@@ -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