test.v 4.95 KB
Newer Older
1
Require Import Why3.
MARCHE Claude's avatar
MARCHE Claude committed
2 3 4 5 6 7

Inductive Why3Unhabited : Prop := .
Axiom letUsTrustWhy3 : Why3Unhabited.

Ltac ae := why3 "alt-ergo" timelimit 5 ; case letUsTrustWhy3.
Ltac z3 := why3 "z3" timelimit 5; case letUsTrustWhy3.
8

9
Require Export ZArith.
10
Open Scope Z_scope.
11
Require Export Lists.List.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12

13 14 15 16 17 18 19 20 21 22 23 24 25
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.
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51

(* 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.

52 53 54 55 56
Inductive foo : Set :=
  | OO : foo
  | SS : forall x:nat, p x -> foo
with p : nat -> Prop :=
  | cc : p O.
57

58
Goal p O.
MARCHE Claude's avatar
MARCHE Claude committed
59 60
(* not a first order goal *)
try ae.
61 62
exact cc.
Qed.
63

64 65
Inductive fooo : nat -> Prop :=
  c : bar O -> fooo O
66 67 68
with bar : nat -> Prop :=
  d : forall f:nat->nat, bar (f O).

69
Goal fooo O.
MARCHE Claude's avatar
MARCHE Claude committed
70 71
(* Don't know *)
try ae.
72 73
exact (c (d (fun x => O))).
Qed.
74 75 76 77 78 79 80 81 82 83

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

Goal forall f: nat ->tree, True.
intros.
ae.
84
Qed.
85 86 87 88

Parameter f : (nat -> nat) -> nat.

Goal f (plus O) = f (plus O).
MARCHE Claude's avatar
MARCHE Claude committed
89 90
(* not a first order goal *)
try ae.
91 92
trivial.
Qed.
93

94
Parameter f' : nat -> nat.
95

96
Axiom f'_def: f' O = O.
97

98
Goal f' (f' O) = O.
99
ae.
100 101
Qed.

102
Variable b:Set.
103 104 105

Section S.

106 107
Variable b:Set->Set.

108 109 110
Variable a:Set.

Inductive sorted : list a -> Prop :=
111 112
  ccc: sorted (@nil a)
| ddd: forall x: a, sorted (cons x nil).
113 114 115

Variable f : a -> a.

116 117 118 119
Goal True.
ae.
Qed.

120 121 122 123 124 125 126 127 128 129 130
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.

131 132 133 134
Goal True.
ae.
Qed.

135
Parameter par: Z -> Prop.
136 137 138 139

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

(* cast *)
Goal
  (
149
  (forall x:Z, par x -> par (x+1)) -> par (0 : Z) -> par 1 : Prop).
150 151
ae.
Qed.
152

153 154
(* type definitions *)

155 156
Parameter t : Set -> Set.

157
Inductive foobar : Set :=
158
  C : t nat -> foobar.
159

160
Goal forall x:foobar, x=x.
161
intros.
162
ae.
163 164
Qed.

165 166
(* predicate definition *)

167
Definition p' (x:nat) := x=O.
168

169
Goal p' O.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
170
ae.
171 172
Qed.

173 174 175 176
Goal plus O O = O.
ae.
Qed.

177

178 179 180 181
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
182
ae.
183
Qed.
184

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

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

(* function definition *)
195

196
Definition ff (x:Z) (y:Z) := x+y.
197

198
Goal ff 1 2 = 3.
199
ae.
200 201
Qed.

202 203 204
Definition id A (x:A) := x.

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

208 209 210 211 212 213
(* recursive function definition *)

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

214 215 216
(* recursive predicate definition *)

Goal In 0 (cons 1 (cons 0 nil)).
217
ae.
218
Qed.
219

220
(* inductive types *)
221

222 223 224 225 226
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
227
ae.
228
Qed.
229 230 231

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

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

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


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


256 257
(* Polymorphic, Mutually inductive types *)

258 259 260
Inductive ptree {a:Set} : Set :=
  | PLeaf : ptree
  | PNode : a -> pforest -> ptree
261

262 263 264
with pforest {a:Set} : Set :=
  | PNil : pforest
  | PCons : ptree -> pforest -> pforest.
265

266
Goal forall x : @ptree Z, x=x.
267
ae.
268
Qed.
269

270
Definition a := 0+0.
271
Definition bb := a.
272

273
Goal bb=0.
274 275 276
ae.
Qed.

277
Goal bb=0.
278
ae.
279
Qed.
280

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

288
Goal ptree_size (@PLeaf Z) = 0.
289 290 291
ae.
Qed.

292
Goal forall (a:Set), ptree_size (@PLeaf a) = 0.
293
intros.
294
ae.
295
Qed.
296

297 298 299 300 301 302 303 304 305 306 307
(* 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.
308
ae.
309 310
Qed.

311 312 313 314 315 316 317 318 319 320 321
(* 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.

322
Require Import Rbase.
323 324 325 326 327
Require Import R_sqrt.
Require Import Rfunctions.
Require Import Rbasic_fun.

Goal forall (x:R), (0 <= x * x)%R.
MARCHE Claude's avatar
MARCHE Claude committed
328 329
ae.
Qed.