Int.v 3.71 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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
(* This file is generated by Why3's Coq-realize driver *)
13
(* Beware! Only edit allowed sections below    *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
14 15
Require Import BuiltIn.
Require BuiltIn.
16

17
(* Why3 comment *)
18
(* prefix_mn is replaced with (-x)%Z by the coq driver *)
19

20 21
(* Why3 comment *)
(* infix_pl is replaced with (x + x1)%Z by the coq driver *)
22

23
(* Why3 comment *)
24
(* infix_as is replaced with (x * x1)%Z by the coq driver *)
25

26
(* Why3 comment *)
27 28 29 30 31 32 33 34 35 36 37 38
(* infix_ls is replaced with (x < x1)%Z by the coq driver *)

(* Why3 goal *)
Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
reflexivity.
Qed.

(* Why3 goal *)
Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/
  (x = y)).
exact Zle_lt_or_eq_iff.
Qed.
39

40
(* Why3 goal *)
41 42
Lemma Assoc : forall (x:Z) (y:Z) (z:Z),
  (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
43
Proof.
44 45 46 47 48
intros x y z.
apply sym_eq.
apply Zplus_assoc.
Qed.

49
(* Why3 goal *)
50
Lemma Unit_def_l : forall (x:Z), ((0%Z + x)%Z = x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
51 52 53 54 55
Proof.
exact Zplus_0_l.
Qed.

(* Why3 goal *)
56
Lemma Unit_def_r : forall (x:Z), ((x + 0%Z)%Z = x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
57 58 59 60 61
Proof.
exact Zplus_0_r.
Qed.

(* Why3 goal *)
62
Lemma Inv_def_l : forall (x:Z), (((-x)%Z + x)%Z = 0%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
63 64 65 66 67
Proof.
exact Zplus_opp_l.
Qed.

(* Why3 goal *)
68
Lemma Inv_def_r : forall (x:Z), ((x + (-x)%Z)%Z = 0%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
69
Proof.
70 71 72
exact Zplus_opp_r.
Qed.

73
(* Why3 goal *)
74
Lemma Comm : forall (x:Z) (y:Z), ((x + y)%Z = (y + x)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
75
Proof.
76 77 78
exact Zplus_comm.
Qed.

79
(* Why3 goal *)
80 81
Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z),
  (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
82
Proof.
83 84 85 86 87
intros x y z.
apply sym_eq.
apply Zmult_assoc.
Qed.

88
(* Why3 goal *)
89 90
Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z),
  ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
91 92 93 94 95 96
Proof.
intros x y z.
apply Zmult_plus_distr_r.
Qed.

(* Why3 goal *)
97 98
Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z),
  (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
99 100 101
Proof.
intros x y z.
apply Zmult_plus_distr_l.
102 103
Qed.

104
(* Why3 goal *)
105
Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
106
Proof.
107 108 109
exact Zmult_comm.
Qed.

110
(* Why3 goal *)
111
Lemma Unitary : forall (x:Z), ((1%Z * x)%Z = x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
112
Proof.
113 114 115
exact Zmult_1_l.
Qed.

116
(* Why3 goal *)
117
Lemma NonTrivialRing : ~ (0%Z = 1%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
118
Proof.
119 120 121
discriminate.
Qed.

122
(* Why3 goal *)
123
Lemma Refl : forall (x:Z), (x <= x)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
124
Proof.
125 126 127 128
intros x.
apply Zle_refl.
Qed.

129
(* Why3 goal *)
130 131
Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z ->
  (x <= z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
132
Proof.
133
exact Zle_trans.
134 135
Qed.

136
(* Why3 goal *)
137
Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> ((y <= x)%Z -> (x = y)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
138
Proof.
139
exact Zle_antisym.
140 141
Qed.

142
(* Why3 goal *)
143
Lemma Total : forall (x:Z) (y:Z), (x <= y)%Z \/ (y <= x)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
144
Proof.
145 146 147
intros x y.
destruct (Zle_or_lt x y) as [H|H].
left.
148
assumption.
149 150 151 152
right.
now apply Zlt_le_weak.
Qed.

153
(* Why3 goal *)
154
Lemma ZeroLessOne : (0%Z <= 1%Z)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
155
Proof.
156
apply Zle_lt_or_eq_iff.
157 158
now left.
Qed.
159

160
(* Why3 goal *)
161 162
Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z ->
  ((x + z)%Z <= (y + z)%Z)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
163
Proof.
164
exact Zplus_le_compat_r.
165 166
Qed.

167
(* Why3 goal *)
168 169
Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z ->
  ((0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
170
Proof.
171
exact Zmult_le_compat_r.
172 173
Qed.