test.v 4.61 KB
 Jean-Christophe Filliâtre committed Apr 04, 2012 1 ``````Require Import Why3. `````` Jean-Christophe Filliâtre committed Apr 13, 2010 2 ``````Require Export ZArith. `````` Jean-Christophe Filliâtre committed Apr 14, 2010 3 ``````Open Scope Z_scope. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 4 ``````Require Export List. `````` Jean-Christophe Filliâtre committed Apr 13, 2010 5 `````` `````` François Bobot committed Jul 23, 2012 6 ``````Ltac ae := why3 "alt-ergo". `````` Jean-Christophe Filliâtre committed Apr 10, 2012 7 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 48 ``````Definition t (a:Type) := list a. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 49 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 50 ``````(* `````` Jean-Christophe Filliâtre committed Mar 28, 2012 51 52 53 54 55 ``````Inductive foo : Set := | OO : foo | SS : forall x:nat, p x -> foo with p : nat -> Prop := | cc : p O. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 56 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 57 58 ``````Goal p O. ae. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 59 ``````*) `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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). `````` Jean-Christophe Filliâtre committed Mar 28, 2012 66 ``````(* `````` Jean-Christophe Filliâtre committed Mar 28, 2012 67 68 ``````Goal foo O. ae. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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. *) `````` Jean-Christophe Filliâtre committed Mar 28, 2012 82 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 83 ``````(* `````` Jean-Christophe Filliâtre committed Mar 28, 2012 84 85 86 87 ``````Parameter f : (nat -> nat) -> nat. Goal f (plus O) = f (plus O). ae. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 96 97 ``````Qed. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 98 ``````Variable b:Set. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 99 100 101 `````` Section S. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 102 103 ``````Variable b:Set->Set. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 104 105 106 ``````Variable a:Set. Inductive sorted : list a -> Prop := `````` Jean-Christophe Filliâtre committed Mar 28, 2012 107 108 `````` cc: sorted (@nil a) | dd: forall x: a, sorted (cons x nil). `````` Jean-Christophe Filliâtre committed Mar 28, 2012 109 110 111 `````` Variable f : a -> a. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 112 113 114 115 ``````Goal True. ae. Qed. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 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. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 127 128 129 130 ``````Goal True. ae. Qed. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 131 ``````Goal sorted _ (@nil nat). `````` Jean-Christophe Filliâtre committed Mar 16, 2012 132 ``````ae. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 133 ``````Qed. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 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. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 144 ``````Qed. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 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. `````` Jean-Christophe Filliâtre committed May 21, 2010 152 153 `````` `````` 154 155 ``````(* type definitions *) `````` Jean-Christophe Filliâtre committed Mar 28, 2012 156 157 ``````Inductive foobar : Set := C : list nat -> foobar. `````` 158 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 159 ``````Goal forall x:foobar, x=x. `````` 160 ``````intros. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 161 ``````ae. `````` 162 163 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 164 165 ``````(* predicate definition *) `````` Jean-Christophe Filliâtre committed Mar 16, 2012 166 ``````Definition p' (x:nat) := x=O. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 167 `````` `````` Jean-Christophe Filliâtre committed Mar 16, 2012 168 ``````Goal p' O. `````` Jean-Christophe Filliâtre committed May 18, 2010 169 ``````ae. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 170 171 ``````Qed. `````` Jean-Christophe Filliâtre committed May 19, 2010 172 173 174 175 ``````Goal plus O O = O. ae. Qed. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 176 `````` `````` Jean-Christophe Filliâtre committed Mar 16, 2012 177 178 179 180 ``````Definition eq' (A:Set) (x y : A) := x=y. Goal eq' nat O O. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 181 ``````ae. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 182 ``````(* `````` Jean-Christophe Filliâtre committed Apr 30, 2010 183 ``````why "z3". (* BUG encoding decorate ici ? *) `````` Jean-Christophe Filliâtre committed Apr 30, 2010 184 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 185 186 ``````*) Admitted. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 187 `````` `````` Jean-Christophe Filliâtre committed May 18, 2010 188 189 190 191 ``````Definition pred (n:nat) := match n with | O => O | S p => p end. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 192 `````` `````` Jean-Christophe Filliâtre committed May 18, 2010 193 194 ``````Goal pred (S O) = O. ae. `````` Jean-Christophe Filliâtre committed May 19, 2010 195 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 196 197 `````` (* function definition *) `````` 198 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 199 ``````Definition ff (x:Z) (y:Z) := x+y. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 200 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 201 ``````Goal ff 1 2 = 3. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 202 ``````ae. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 203 204 ``````Qed. `````` 205 206 207 ``````Definition id A (x:A) := x. Goal id nat O = O. `````` Jean-Christophe Filliâtre committed May 18, 2010 208 ``````ae. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 209 210 ``````Qed. `````` Jean-Christophe Filliâtre committed May 21, 2010 211 212 213 214 215 216 ``````(* recursive function definition *) Goal length (cons 1 (cons 2 nil)) = S (S O). ae. Qed. `````` Jean-Christophe Filliâtre committed May 19, 2010 217 218 219 ``````(* recursive predicate definition *) Goal In 0 (cons 1 (cons 0 nil)). `````` Jean-Christophe Filliâtre committed Mar 16, 2012 220 ``````ae. `````` Jean-Christophe Filliâtre committed May 28, 2010 221 ``````Qed. `````` Jean-Christophe Filliâtre committed May 19, 2010 222 `````` `````` Jean-Christophe Filliâtre committed Apr 30, 2010 223 ``````(* inductive types *) `````` 224 `````` `````` Jean-Christophe Filliâtre committed Apr 15, 2010 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 committed May 18, 2010 230 ``````ae. `````` 231 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 232 233 234 `````` Goal forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y. intros. `````` Jean-Christophe Filliâtre committed Apr 30, 2010 235 ``````ae. `````` 236 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 237 `````` `````` Jean-Christophe Filliâtre committed Apr 15, 2010 238 ``````Goal forall x: list nat, x=x. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 239 ``````intros. `````` Jean-Christophe Filliâtre committed May 18, 2010 240 ``````ae. `````` 241 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 242 `````` `````` Jean-Christophe Filliâtre committed May 28, 2010 243 ``````Goal (match (S (S (S O))) with (S (S _)) => True | _ => False end). `````` Jean-Christophe Filliâtre committed Mar 16, 2012 244 ``````ae. `````` Jean-Christophe Filliâtre committed May 28, 2010 245 ``````Qed. `````` Jean-Christophe Filliâtre committed May 18, 2010 246 247 `````` `````` Jean-Christophe Filliâtre committed Mar 16, 2012 248 249 250 ``````Goal forall a, forall (x: list (list a)), 1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2. `````` Jean-Christophe Filliâtre committed May 28, 2010 251 ``````intros a x. `````` Jean-Christophe Filliâtre committed Mar 23, 2012 252 253 254 255 ``````assert (x=nil \/ exists y: list a, exists z:list (list a), x = cons y z). destruct x; ae. ae. `````` Jean-Christophe Filliâtre committed May 28, 2010 256 ``````Qed. `````` Jean-Christophe Filliâtre committed May 18, 2010 257 258 `````` `````` Jean-Christophe Filliâtre committed Apr 15, 2010 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. `````` Jean-Christophe Filliâtre committed May 19, 2010 270 ``````ae. `````` 271 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 15, 2010 272 `````` `````` Jean-Christophe Filliâtre committed Mar 16, 2012 273 ``````Definition a := 0+0. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 274 ``````Definition bb := a. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 275 `````` `````` Jean-Christophe Filliâtre committed Mar 28, 2012 276 ``````Goal bb=0. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 277 278 279 ``````ae. Qed. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 280 ``````Goal bb=0. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 281 ``````ae. `````` Jean-Christophe Filliâtre committed Mar 28, 2012 282 ``````Qed. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 283 `````` `````` Jean-Christophe Filliâtre committed May 21, 2010 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. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 295 ``````Goal forall (a:Set), ptree_size a (PLeaf a) = 0. `````` Jean-Christophe Filliâtre committed May 28, 2010 296 ``````intros. `````` Jean-Christophe Filliâtre committed Mar 16, 2012 297 ``````ae. `````` Jean-Christophe Filliâtre committed Mar 23, 2012 298 ``````Qed. `````` Jean-Christophe Filliâtre committed May 21, 2010 299 `````` `````` Jean-Christophe Filliâtre committed Apr 15, 2010 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. `````` Jean-Christophe Filliâtre committed May 19, 2010 311 ``````ae. `````` 312 313 ``````Qed. `````` Jean-Christophe Filliâtre committed Apr 18, 2012 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. ``````