test.v 4.72 KB
Newer Older
1
Require Import Why3.
2
3
Ltac ae := why3 "alt-ergo".

4
Require Export ZArith.
5
Open Scope Z_scope.
6
Require Export Lists.List.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7

8
9
10
11
12
13
14
15
16
17
18
19
20
Section S0.
  Variable a:Set->Set.

  Goal forall b:Set->Set, forall x:a nat, x=x.
    intros; ae.
  Qed.

Goal
  forall f: (nat->nat)->nat, f S = O -> True.
intros; ae.
Qed.

End S0.
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

(* Mutually inductive types *)

Inductive tree : Set :=
  | Leaf : tree
  | Node : Z -> forest -> tree
with forest : Set :=
  | Nil : forest
  | Cons : tree -> forest -> forest.

Fixpoint tree_size (t:tree) : Z := match t with
  | Leaf => 0
  | Node _ f => 1 + forest_size f end
with forest_size (f:forest) : Z := match f with
  | Nil => 0
  | Cons t f => tree_size t + forest_size f end.


Goal tree_size (Node 42 (Cons Leaf Nil)) = 1.
ae.
Qed.

Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1.
ae.
Qed.


(*
49
50
51
52
53
Inductive foo : Set :=
  | OO : foo
  | SS : forall x:nat, p x -> foo
with p : nat -> Prop :=
  | cc : p O.
54

55
56
Goal p O.
ae.
57
*)
58
59
60
61
62
63

Inductive foo : nat -> Prop :=
  c : bar O -> foo O
with bar : nat -> Prop :=
  d : forall f:nat->nat, bar (f O).

64
(*
65
66
Goal foo O.
ae.
67
68
69
70
71
72
73
74
75
76
77
78
79
*)

Inductive tree' : Set :=
  | Empty' : tree'
  | Node' : forest' -> tree'
with forest' : Set :=
  | Forest' : (nat -> tree') -> forest'.

(*
Goal forall f: nat ->tree, True.
intros.
ae.
*)
80

81
(*
82
83
84
85
Parameter f : (nat -> nat) -> nat.

Goal f (plus O) = f (plus O).
ae.
86
87
88
89
90
91
92
93
Qed.*)

Parameter f: nat -> nat.

Axiom f_def: f O = O.

Goal f (f O) = O.
ae.
94
95
Qed.

96
Variable b:Set.
97
98
99

Section S.

100
101
Variable b:Set->Set.

102
103
104
Variable a:Set.

Inductive sorted : list a -> Prop :=
105
106
  cc: sorted (@nil a)
| dd: forall x: a, sorted (cons x nil).
107
108
109

Variable f : a -> a.

110
111
112
113
Goal True.
ae.
Qed.

114
115
116
117
118
119
120
121
122
123
124
Goal forall x: a, f (f x) = f x -> f (f (f x)) = f x.
intros.
ae.
Qed.

Goal forall l: list a, l=l.
ae.
Qed.

End S.

125
126
127
128
Goal True.
ae.
Qed.

129
130
131
132
133
134
135
136
137
Parameter p: Z -> Prop.

(* let in *)
Goal
  let t := Z in
  let f := p 0 in
  (forall x:t, p x -> p (let y := x+1 in y)) ->
  f -> p 1.
ae.
138
Qed.
139
140
141
142
143
144
145

(* cast *)
Goal
  (
  (forall x:Z, p x -> p (x+1)) -> p (0 : Z) -> p 1 : Prop).
ae.
Qed.
146

147
148
(* type definitions *)

149
150
Parameter t : Set -> Set.

151
Inductive foobar : Set :=
152
  C : t nat -> foobar.
153

154
Goal forall x:foobar, x=x.
155
intros.
156
ae.
157
158
Qed.

159
160
(* predicate definition *)

161
Definition p' (x:nat) := x=O.
162

163
Goal p' O.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
164
ae.
165
166
Qed.

167
168
169
170
Goal plus O O = O.
ae.
Qed.

171

172
173
174
175
Definition eq' (A:Set) (x y : A) := x=y.

Goal
  eq' nat O O.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
176
ae.
177
(*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178
why "z3".  (* BUG encoding decorate ici ? *)
179
Qed.
180
181
*)
Admitted.
182

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183
184
185
186
Definition pred (n:nat) := match n with 
  | O => O
  | S p => p
  end.
187

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188
189
Goal pred (S O) = O.
ae.
190
Qed.
191
192

(* function definition *)
193

194
Definition ff (x:Z) (y:Z) := x+y.
195

196
Goal ff 1 2 = 3.
197
ae.
198
199
Qed.

200
201
202
Definition id A (x:A) := x.

Goal id nat O = O.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203
ae.
204
205
Qed.

206
207
208
209
210
211
(* recursive function definition *)

Goal length (cons 1 (cons 2 nil)) = S (S O).
ae.
Qed.

212
213
214
(* recursive predicate definition *)

Goal In 0 (cons 1 (cons 0 nil)).
215
ae.
216
Qed.
217

218
(* inductive types *)
219

220
221
222
223
224
Parameter P : (nat -> nat) -> Prop.

Goal forall (a:Set), forall x:nat, x=S O -> P S -> 
  let y := (S (S O)) in S x=y.
intros.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
ae.
226
Qed.
227
228
229

Goal  forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y.
intros.
230
ae.
231
Qed.
232

233
Goal  forall x: list nat, x=x.
234
intros.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235
ae.
236
Qed.
237

238
Goal (match (S (S (S O))) with (S (S _)) => True | _ => False end).
239
ae.
240
Qed.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241
242


243
244
245
Goal
  forall a, forall (x: list (list a)), 
  1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2.
246
intros a x.
247
248
249
250
assert (x=nil \/ exists y: list a, exists z:list (list a),
                 x = cons y z).
destruct x; ae.
ae.
251
Qed.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
252
253


254
255
256
257
258
259
260
261
262
263
264
(* Polymorphic, Mutually inductive types *)

Inductive ptree (a:Set) : Set :=
  | PLeaf : ptree a
  | PNode : a -> pforest a -> ptree a

with pforest (a:Set) : Set :=
  | PNil : pforest a
  | PCons : ptree a -> pforest a -> pforest a.

Goal forall x : ptree Z, x=x.
265
ae.
266
Qed.
267

268
Definition a := 0+0.
269
Definition bb := a.
270

271
Goal bb=0.
272
273
274
ae.
Qed.

275
Goal bb=0.
276
ae.
277
Qed.
278

279
280
281
282
283
284
285
286
287
288
289
Fixpoint ptree_size (a:Set) (t:ptree a) : Z := match t with
  | PLeaf => 0
  | PNode _ f => 1 + pforest_size _ f end
with pforest_size (a:Set) (f:pforest a) : Z := match f with
  | PNil => 0
  | PCons t f => ptree_size _ t + pforest_size _ f end.

Goal ptree_size _ (@PLeaf Z) = 0.
ae.
Qed.

290
Goal forall (a:Set), ptree_size a (PLeaf a) = 0.
291
intros.
292
ae.
293
Qed.
294

295
296
297
298
299
300
301
302
303
304
305
(* the same, without parameters *)

Inductive ptree' : Type -> Type :=
  | PLeaf' : forall (a:Type), ptree' a
  | PNode' : forall (a:Type), a -> pforest' a -> ptree' a

with pforest' : Type -> Type :=
  | PNil' : forall  (a:Type), pforest' a
  | PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a.

Goal forall x : ptree' Z, x=x.
306
ae.
307
308
Qed.

309
310
311
312
313
314
315
316
317
318
319
(* order of type parameters matters *)

Definition wgt (k:(nat * Z)%type) := match k with
  | (_, p) => p
  end.
Implicit Arguments wgt.

Goal wgt (S O, 3) = 3.
ae.
Qed.

320
321
322
323
324
325
326
327
Require Import BuiltIn.
Require Import R_sqrt.
Require Import Rfunctions.
Require Import Rbasic_fun.

Goal forall (x:R), (0 <= x * x)%R.
ae.
Qed.