list.why 4.07 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 2 3 `````` theory List `````` Andrei Paskevich committed Jun 24, 2010 4 `````` type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 5 6 7 8 9 10 11 `````` end theory Length use import int.Int use import List `````` Andrei Paskevich committed Jun 24, 2010 12 `````` logic length (l : list 'a) : int = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 13 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 14 15 `````` | Nil -> 0 | Cons _ r -> 1 + length(r) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 16 17 `````` end `````` Andrei Paskevich committed Jun 24, 2010 18 `````` lemma Length_nonnegative : forall l:list 'a. length(l) >= 0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 19 `````` `````` Jean-Christophe Filliâtre committed Nov 10, 2010 20 21 `````` lemma Length_nil : forall l:list 'a. length l = 0 <-> l = Nil `````` Jean-Christophe Filliâtre committed Mar 23, 2010 22 23 24 25 26 ``````end theory Mem use export List `````` Andrei Paskevich committed Jun 24, 2010 27 `````` logic mem (x: 'a) (l : list 'a) = match l with `````` Andrei Paskevich committed Jun 17, 2010 28 `````` | Nil -> false `````` Andrei Paskevich committed Jun 21, 2010 29 `````` | Cons y r -> x = y or mem x r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 30 31 32 33 `````` end end `````` 34 35 ``````theory Nth use export List `````` Jean-Christophe Filliâtre committed Nov 10, 2010 36 `````` use export option.Option `````` 37 38 `````` use import int.Int `````` Jean-Christophe Filliâtre committed Nov 10, 2010 39 `````` logic nth (n : int) (l : list 'a) : option 'a = match l with `````` Jean-Christophe Filliâtre committed Nov 10, 2010 40 41 `````` | Nil -> None | Cons x r -> if n = 0 then Some x else nth (n - 1) r `````` 42 43 44 45 `````` end end `````` Jean-Christophe Filliâtre committed Nov 15, 2010 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 ``````theory HdTl "head and tail" use export List use export option.Option logic hd (l : list 'a) : option 'a = match l with | Nil -> None | Cons h _ -> Some h end logic tl (l : list 'a) : option (list 'a) = match l with | Nil -> None | Cons _ t -> Some t end (* TODO: move these lemmas into another theory? *) use import Nth use import int.Int lemma Nth_tl : forall l1 l2 : list 'a. tl l1 = Some l2 -> forall i : int. nth i l2 = nth (i+1) l1 lemma Nth0_head: forall l : list 'a. nth 0 l = hd l end `````` Jean-Christophe Filliâtre committed Nov 10, 2010 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 ``````theory Append use export List logic append (l1 l2 : list 'a) : list 'a = match l1 with | Nil -> l2 | Cons x1 r1 -> Cons x1 (append r1 l2) end lemma Append_assoc : forall l1 l2 l3 : list 'a. append l1 (append l2 l3) = append (append l1 l2) l3 lemma Append_l_nil : forall l : list 'a. append l Nil = l use import Length use import int.Int lemma Append_length : forall l1 l2 : list 'a. length (append l1 l2) = length l1 + length l2 end theory Reverse use export List use import Append logic reverse (l : list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> append (reverse r) (Cons x Nil) end use import Length lemma Reverse_length : forall l : list 'a. length (reverse l) = length l end `````` Jean-Christophe Filliâtre committed Jul 07, 2010 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 ``````theory Sorted use export List use import int.Int inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) use import Mem lemma Sorted_mem : forall x : int, l : list int. (forall y : int. mem y l -> x <= y) and sorted l <-> sorted (Cons x l) end theory NumOcc use import int.Int use import List (* number of occurence of x in l *) logic num_occ (x : 'a) (l : list 'a) : int = match l with | Nil -> 0 | Cons y r -> (if x = y then 1 else 0) + num_occ x r end use import Mem lemma Mem_Num_Occ : forall x:'a, l:list 'a. mem x l <-> num_occ x l > 0 end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 156 ``````theory Permut `````` Jean-Christophe Filliâtre committed Jul 07, 2010 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 `````` use import NumOcc use import List logic permut (l1 : list 'a) (l2 : list 'a) = forall x : 'a. num_occ x l1 = num_occ x l2 lemma Permut_refl : forall l : list 'a. permut l l lemma Permut_sym : forall l1 l2 : list 'a. permut l1 l2 -> permut l2 l1 lemma Permut_trans : forall l1 l2 l3 : list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3 lemma Permut_cons : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> permut (Cons x l1) (Cons x l2) lemma Permut_swap : forall x y : 'a, l : list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) use import Mem lemma Permut_mem : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> mem x l1 -> mem x l2 use import Length lemma Permut_length : forall l1 l2 : list 'a. permut l1 l2 -> length l1 = length l2 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 188 189 190 191 192 ``````end theory Induction use import List `````` Jean-Christophe Filliâtre committed Jul 07, 2010 193 194 195 `````` type elt logic p (list elt) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 196 197 `````` axiom Induction : `````` Jean-Christophe Filliâtre committed Jul 07, 2010 198 199 200 `````` p (Nil : list elt) -> (forall x:elt. forall l:list elt. p l -> p (Cons x l)) -> forall l:list elt. p l `````` Jean-Christophe Filliâtre committed Mar 23, 2010 201 202 203 204 205 206 207 208 `````` end theory Map use import List type a type b `````` Andrei Paskevich committed Jun 24, 2010 209 `````` logic f a : b `````` Jean-Christophe Filliâtre committed Mar 23, 2010 210 `````` `````` Andrei Paskevich committed Jun 24, 2010 211 `````` logic map(l : list a) : list b = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 212 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 213 `````` | Nil -> Nil `````` Andrei Paskevich committed Jun 21, 2010 214 `````` | Cons x r -> Cons (f x) (map r) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 215 216 217 218 219 220 221 `````` end end theory Fold (* TODO (a la Map) *) end``````