MinMax.v 2.45 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
17

18
(* Why3 comment *)
19
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
20

21
(* Why3 goal *)
22 23 24
Lemma min_def :
  forall (x:Z) (y:Z),
  ((x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x)) /\
25
  (~ (x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = y)).
26
Proof.
27
intros x y.
28
split ; intros H.
29 30
now apply Zmin_l.
apply Zmin_r.
31
omega.
32 33
Qed.

34
(* Why3 comment *)
35
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
36

37
(* Why3 goal *)
38 39 40
Lemma max_def :
  forall (x:Z) (y:Z),
  ((x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y)) /\
41
  (~ (x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = x)).
42
Proof.
43
intros x y.
44
split ; intros H.
45 46
now apply Zmax_r.
apply Zmax_l.
47
omega.
48 49
Qed.

50
(* Why3 goal *)
51 52
Lemma Min_r :
  forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.min x y) = y).
53
exact Zmin_r.
54 55
Qed.

56
(* Why3 goal *)
57 58
Lemma Max_l :
  forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.max x y) = x).
59
exact Zmax_l.
60 61
Qed.

62
(* Why3 goal *)
63 64
Lemma Min_comm :
  forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
65
exact Zmin_comm.
66 67
Qed.

68
(* Why3 goal *)
69 70
Lemma Max_comm :
  forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
71
exact Zmax_comm.
72 73 74
Qed.

(* Why3 goal *)
75 76
Lemma Min_assoc :
  forall (x:Z) (y:Z) (z:Z),
77 78
  ((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) =
   (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
79 80 81 82 83
Proof.
intros x y z.
apply eq_sym, Zmin_assoc.
Qed.

84
(* Why3 goal *)
85 86
Lemma Max_assoc :
  forall (x:Z) (y:Z) (z:Z),
87 88
  ((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) =
   (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
89 90 91 92 93
Proof.
intros x y z.
apply eq_sym, Zmax_assoc.
Qed.