test.v 4.61 KB
Newer Older
1
Require Import Why3.
2
Require Export ZArith.
3
Open Scope Z_scope.
4
Require Export List.
5

6
Ltac ae := why3 "alt-ergo".
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

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


48
Definition t (a:Type) := list a.
49

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

57 58
Goal p O.
ae.
59
*)
60 61 62 63 64 65

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

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

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

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

83
(*
84 85 86 87
Parameter f : (nat -> nat) -> nat.

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

Parameter f: nat -> nat.

Axiom f_def: f O = O.

Goal f (f O) = O.
ae.
96 97
Qed.

98
Variable b:Set.
99 100 101

Section S.

102 103
Variable b:Set->Set.

104 105 106
Variable a:Set.

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

Variable f : a -> a.

112 113 114 115
Goal True.
ae.
Qed.

116 117 118 119 120 121 122 123 124 125 126
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.

127 128 129 130
Goal True.
ae.
Qed.

131
Goal sorted _ (@nil nat).
132
ae.
133
Qed.
134 135 136 137 138 139 140 141 142 143

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.
144
Qed.
145 146 147 148 149 150 151

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


154 155
(* type definitions *)

156 157
Inductive foobar : Set :=
  C : list nat -> foobar.
158

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

164 165
(* predicate definition *)

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

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

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

176

177 178 179 180
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
181
ae.
182
(*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183
why "z3".  (* BUG encoding decorate ici ? *)
184
Qed.
185 186
*)
Admitted.
187

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193 194
Goal pred (S O) = O.
ae.
195
Qed.
196 197

(* function definition *)
198

199
Definition ff (x:Z) (y:Z) := x+y.
200

201
Goal ff 1 2 = 3.
202
ae.
203 204
Qed.

205 206 207
Definition id A (x:A) := x.

Goal id nat O = O.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
208
ae.
209 210
Qed.

211 212 213 214 215 216
(* recursive function definition *)

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

217 218 219
(* recursive predicate definition *)

Goal In 0 (cons 1 (cons 0 nil)).
220
ae.
221
Qed.
222

223
(* inductive types *)
224

225 226 227 228 229
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
230
ae.
231
Qed.
232 233 234

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

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

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


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


259 260 261 262 263 264 265 266 267 268 269
(* 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.
270
ae.
271
Qed.
272

273
Definition a := 0+0.
274
Definition bb := a.
275

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

280
Goal bb=0.
281
ae.
282
Qed.
283

284 285 286 287 288 289 290 291 292 293 294
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.

295
Goal forall (a:Set), ptree_size a (PLeaf a) = 0.
296
intros.
297
ae.
298
Qed.
299

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

314 315 316 317 318 319 320 321 322 323 324
(* 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.