Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

elements_Elements_Occ_elements_1.v 7.04 KB
Newer Older
1 2 3 4
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
5
Parameter bag : forall (a:Type), Type.
6

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
7
Parameter nb_occ: forall (a:Type), a -> (bag a) -> Z.
8

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
9
Implicit Arguments nb_occ.
10

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
11 12
Axiom occ_non_negative : forall (a:Type), forall (b:(bag a)) (x:a),
  (0%Z <= (nb_occ x b))%Z.
13

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
14 15 16
Definition eq_bag (a:Type)(a1:(bag a)) (b:(bag a)): Prop := forall (x:a),
  ((nb_occ x a1) = (nb_occ x b)).
Implicit Arguments eq_bag.
17

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
18 19
Axiom bag_extensionality : forall (a:Type), forall (a1:(bag a)) (b:(bag a)),
  (eq_bag a1 b) -> (a1 = b).
20

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
21
Parameter empty_bag: forall (a:Type), (bag a).
22 23

Set Contextual Implicit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
24
Implicit Arguments empty_bag.
25 26
Unset Contextual Implicit.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
27 28
Axiom occ_empty : forall (a:Type), forall (x:a), ((nb_occ x (empty_bag:(bag
  a))) = 0%Z).
29

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
30 31
Axiom is_empty : forall (a:Type), forall (b:(bag a)), (forall (x:a),
  ((nb_occ x b) = 0%Z)) -> (b = (empty_bag:(bag a))).
32

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
33
Parameter singleton: forall (a:Type), a -> (bag a).
34

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
35
Implicit Arguments singleton.
36

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
37 38 39
Axiom occ_singleton : forall (a:Type), forall (x:a) (y:a), ((x = y) /\
  ((nb_occ y (singleton x)) = 1%Z)) \/ ((~ (x = y)) /\ ((nb_occ y
  (singleton x)) = 0%Z)).
40 41

Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
42
  ((nb_occ y (singleton x)) = 1%Z).
43 44

Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
45
  ((nb_occ y (singleton x)) = 0%Z).
46

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
47
Parameter union: forall (a:Type), (bag a) -> (bag a) -> (bag a).
48 49 50

Implicit Arguments union.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
51 52
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(bag a)) (b:(bag a)),
  ((nb_occ x (union a1 b)) = ((nb_occ x a1) + (nb_occ x b))%Z).
53

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
54
Axiom Union_comm : forall (a:Type), forall (a1:(bag a)) (b:(bag a)),
55 56
  ((union a1 b) = (union b a1)).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
57 58
Axiom Union_identity : forall (a:Type), forall (a1:(bag a)), ((union a1
  (empty_bag:(bag a))) = a1).
59

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
60 61
Axiom Union_assoc : forall (a:Type), forall (a1:(bag a)) (b:(bag a)) (c:(bag
  a)), ((union a1 (union b c)) = (union (union a1 b) c)).
62

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
63 64
Axiom bag_simpl : forall (a:Type), forall (a1:(bag a)) (b:(bag a)) (c:(bag
  a)), ((union a1 b) = (union c b)) -> (a1 = c).
65

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
66 67
Axiom bag_simpl_left : forall (a:Type), forall (a1:(bag a)) (b:(bag a))
  (c:(bag a)), ((union a1 b) = (union a1 c)) -> (b = c).
68

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
69
Definition add (a:Type)(x:a) (b:(bag a)): (bag a) := (union (singleton x) b).
70 71
Implicit Arguments add.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
72 73
Axiom occ_add_eq : forall (a:Type), forall (b:(bag a)) (x:a) (y:a),
  (x = y) -> ((nb_occ x (add x b)) = ((nb_occ x b) + 1%Z)%Z).
74

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
75 76
Axiom occ_add_neq : forall (a:Type), forall (b:(bag a)) (x:a) (y:a),
  (~ (x = y)) -> ((nb_occ y (add x b)) = (nb_occ y b)).
77

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
78
Parameter card: forall (a:Type), (bag a) -> Z.
79 80 81

Implicit Arguments card.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
82
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(bag a))) = 0%Z).
83 84

Axiom Card_singleton : forall (a:Type), forall (x:a),
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
85
  ((card (singleton x)) = 1%Z).
86

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
87
Axiom Card_union : forall (a:Type), forall (x:(bag a)) (y:(bag a)),
88 89
  ((card (union x y)) = ((card x) + (card y))%Z).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
90 91
Axiom Card_zero_empty : forall (a:Type), forall (x:(bag a)),
  ((card x) = 0%Z) -> (x = (empty_bag:(bag a))).
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114

Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
  (y <= (Zmax x y))%Z.

Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).

Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
  ((Zmin x y) <= y)%Z.

Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).

Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).

Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).

Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).

Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).

Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).

Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
115
Parameter diff: forall (a:Type), (bag a) -> (bag a) -> (bag a).
116 117 118

Implicit Arguments diff.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
119 120 121 122 123
Axiom Diff_occ : forall (a:Type), forall (b1:(bag a)) (b2:(bag a)) (x:a),
  ((nb_occ x (diff b1 b2)) = (Zmax 0%Z ((nb_occ x b1) - (nb_occ x b2))%Z)).

Axiom Diff_empty_right : forall (a:Type), forall (b:(bag a)), ((diff b
  (empty_bag:(bag a))) = b).
124

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
125 126
Axiom Diff_empty_left : forall (a:Type), forall (b:(bag a)),
  ((diff (empty_bag:(bag a)) b) = (empty_bag:(bag a))).
127

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
128 129
Axiom Diff_add : forall (a:Type), forall (b:(bag a)) (x:a), ((diff (add x b)
  (singleton x)) = b).
130

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
131 132
Axiom Diff_comm : forall (a:Type), forall (b:(bag a)) (b1:(bag a)) (b2:(bag
  a)), ((diff (diff b b1) b2) = (diff (diff b b2) b1)).
133

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
134 135
Axiom Add_diff : forall (a:Type), forall (b:(bag a)) (x:a), (0%Z <  (nb_occ x
  b))%Z -> ((add x (diff b (singleton x))) = b).
136

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.

Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).

Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (b:Type) (a:Type), b -> (map a b).

Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
  b1):(map a b)) a1) = b1).
163 164 165

Definition array (a:Type) := (map Z a).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
166
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (bag a).
167 168 169 170

Implicit Arguments elements.

Axiom Elements_empty : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
171 172 173 174 175
  (j <= i)%Z -> ((elements a1 i j) = (empty_bag:(bag a))).

Axiom Elements_add : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
  (i <  j)%Z -> ((elements a1 i j) = (add (get a1 (j - 1%Z)%Z) (elements a1 i
  (j - 1%Z)%Z))).
176 177

Axiom Elements_singleton : forall (a:Type), forall (a1:(map Z a)) (i:Z)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
178
  (j:Z), (j = (i + 1%Z)%Z) -> ((elements a1 i j) = (singleton (get a1 i))).
179 180 181 182 183

Axiom Elements_union : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
  (k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i
  k) = (union (elements a1 i j) (elements a1 j k))).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
184
Axiom Elements_add1 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
185 186 187 188 189
  (i <  j)%Z -> ((elements a1 i j) = (add (get a1 i) (elements a1 (i + 1%Z)%Z
  j))).

Axiom Elements_remove_last : forall (a:Type), forall (a1:(map Z a)) (i:Z)
  (j:Z), (i <  (j - 1%Z)%Z)%Z -> ((elements a1 i
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
190
  (j - 1%Z)%Z) = (diff (elements a1 i j) (singleton (get a1 (j - 1%Z)%Z)))).
191 192 193 194 195 196

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem Occ_elements : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
197 198
  (n:Z), ((i <= j)%Z /\ (j <  n)%Z) -> (0%Z <  (nb_occ (get a1 j)
  (elements a1 i n)))%Z.
199 200 201 202
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a i j n H.
rewrite Elements_union with (j:=j); auto with zarith.
rewrite occ_union.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
203
rewrite Elements_add1 with (i:=j) (j:=n); auto with zarith.
204 205 206 207 208
rewrite occ_add_eq with (y:=(get a j)); auto.
generalize (occ_non_negative X (elements a i j) (get a j)).
generalize (occ_non_negative X (elements a (j+1)n) (get a j)).
omega.
Qed.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
209
(* DO NOT EDIT BELOW *)