[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Hints_declaration |
---|
| 4 | |
---|
| 5 | open Core_notation |
---|
| 6 | |
---|
| 7 | open Pts |
---|
| 8 | |
---|
| 9 | open Logic |
---|
| 10 | |
---|
| 11 | open Types |
---|
| 12 | |
---|
| 13 | open Bool |
---|
| 14 | |
---|
| 15 | open Relations |
---|
| 16 | |
---|
| 17 | open Nat |
---|
| 18 | |
---|
| 19 | type 'a list = |
---|
| 20 | | Nil |
---|
| 21 | | Cons of 'a * 'a list |
---|
| 22 | |
---|
| 23 | (** val list_rect_Type4 : |
---|
| 24 | 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **) |
---|
| 25 | let rec list_rect_Type4 h_nil h_cons = function |
---|
| 26 | | Nil -> h_nil |
---|
| 27 | | Cons (x_801, x_800) -> |
---|
| 28 | h_cons x_801 x_800 (list_rect_Type4 h_nil h_cons x_800) |
---|
| 29 | |
---|
| 30 | (** val list_rect_Type3 : |
---|
| 31 | 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **) |
---|
| 32 | let rec list_rect_Type3 h_nil h_cons = function |
---|
| 33 | | Nil -> h_nil |
---|
| 34 | | Cons (x_811, x_810) -> |
---|
| 35 | h_cons x_811 x_810 (list_rect_Type3 h_nil h_cons x_810) |
---|
| 36 | |
---|
| 37 | (** val list_rect_Type2 : |
---|
| 38 | 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **) |
---|
| 39 | let rec list_rect_Type2 h_nil h_cons = function |
---|
| 40 | | Nil -> h_nil |
---|
| 41 | | Cons (x_816, x_815) -> |
---|
| 42 | h_cons x_816 x_815 (list_rect_Type2 h_nil h_cons x_815) |
---|
| 43 | |
---|
| 44 | (** val list_rect_Type1 : |
---|
| 45 | 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **) |
---|
| 46 | let rec list_rect_Type1 h_nil h_cons = function |
---|
| 47 | | Nil -> h_nil |
---|
| 48 | | Cons (x_821, x_820) -> |
---|
| 49 | h_cons x_821 x_820 (list_rect_Type1 h_nil h_cons x_820) |
---|
| 50 | |
---|
| 51 | (** val list_rect_Type0 : |
---|
| 52 | 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **) |
---|
| 53 | let rec list_rect_Type0 h_nil h_cons = function |
---|
| 54 | | Nil -> h_nil |
---|
| 55 | | Cons (x_826, x_825) -> |
---|
| 56 | h_cons x_826 x_825 (list_rect_Type0 h_nil h_cons x_825) |
---|
| 57 | |
---|
| 58 | (** val list_inv_rect_Type4 : |
---|
| 59 | 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) |
---|
| 60 | -> 'a2 **) |
---|
| 61 | let list_inv_rect_Type4 hterm h1 h2 = |
---|
| 62 | let hcut = list_rect_Type4 h1 h2 hterm in hcut __ |
---|
| 63 | |
---|
| 64 | (** val list_inv_rect_Type3 : |
---|
| 65 | 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) |
---|
| 66 | -> 'a2 **) |
---|
| 67 | let list_inv_rect_Type3 hterm h1 h2 = |
---|
| 68 | let hcut = list_rect_Type3 h1 h2 hterm in hcut __ |
---|
| 69 | |
---|
| 70 | (** val list_inv_rect_Type2 : |
---|
| 71 | 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) |
---|
| 72 | -> 'a2 **) |
---|
| 73 | let list_inv_rect_Type2 hterm h1 h2 = |
---|
| 74 | let hcut = list_rect_Type2 h1 h2 hterm in hcut __ |
---|
| 75 | |
---|
| 76 | (** val list_inv_rect_Type1 : |
---|
| 77 | 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) |
---|
| 78 | -> 'a2 **) |
---|
| 79 | let list_inv_rect_Type1 hterm h1 h2 = |
---|
| 80 | let hcut = list_rect_Type1 h1 h2 hterm in hcut __ |
---|
| 81 | |
---|
| 82 | (** val list_inv_rect_Type0 : |
---|
| 83 | 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) |
---|
| 84 | -> 'a2 **) |
---|
| 85 | let list_inv_rect_Type0 hterm h1 h2 = |
---|
| 86 | let hcut = list_rect_Type0 h1 h2 hterm in hcut __ |
---|
| 87 | |
---|
| 88 | (** val list_discr : 'a1 list -> 'a1 list -> __ **) |
---|
| 89 | let list_discr x y = |
---|
| 90 | Logic.eq_rect_Type2 x |
---|
| 91 | (match x with |
---|
| 92 | | Nil -> Obj.magic (fun _ dH -> dH) |
---|
| 93 | | Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 94 | |
---|
| 95 | (** val append : 'a1 list -> 'a1 list -> 'a1 list **) |
---|
| 96 | let rec append l1 l2 = |
---|
| 97 | match l1 with |
---|
| 98 | | Nil -> l2 |
---|
| 99 | | Cons (hd, tl) -> Cons (hd, (append tl l2)) |
---|
| 100 | |
---|
| 101 | (** val hd : 'a1 list -> 'a1 -> 'a1 **) |
---|
| 102 | let hd l d = |
---|
| 103 | match l with |
---|
| 104 | | Nil -> d |
---|
| 105 | | Cons (a, x) -> a |
---|
| 106 | |
---|
| 107 | (** val tail : 'a1 list -> 'a1 list **) |
---|
| 108 | let tail = function |
---|
| 109 | | Nil -> Nil |
---|
| 110 | | Cons (hd0, tl) -> tl |
---|
| 111 | |
---|
| 112 | (** val option_hd : 'a1 list -> 'a1 Types.option **) |
---|
| 113 | let option_hd = function |
---|
| 114 | | Nil -> Types.None |
---|
| 115 | | Cons (a, x) -> Types.Some a |
---|
| 116 | |
---|
[2649] | 117 | (** val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list **) |
---|
| 118 | let option_cons c l = |
---|
| 119 | match c with |
---|
| 120 | | Types.None -> l |
---|
| 121 | | Types.Some c0 -> Cons (c0, l) |
---|
| 122 | |
---|
[2601] | 123 | (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) |
---|
| 124 | let rec map f = function |
---|
| 125 | | Nil -> Nil |
---|
| 126 | | Cons (x, tl) -> Cons ((f x), (map f tl)) |
---|
| 127 | |
---|
| 128 | (** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **) |
---|
| 129 | let rec foldr f b = function |
---|
| 130 | | Nil -> b |
---|
| 131 | | Cons (a, l0) -> f a (foldr f b l0) |
---|
| 132 | |
---|
| 133 | (** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **) |
---|
| 134 | let filter p = |
---|
| 135 | foldr (fun x l0 -> |
---|
| 136 | match p x with |
---|
| 137 | | Bool.True -> Cons (x, l0) |
---|
| 138 | | Bool.False -> l0) Nil |
---|
| 139 | |
---|
| 140 | (** val compose0 : |
---|
| 141 | ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **) |
---|
| 142 | let compose0 f l1 l2 = |
---|
| 143 | foldr (fun i acc -> append (map (f i) l2) acc) Nil l1 |
---|
| 144 | |
---|
| 145 | (** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **) |
---|
| 146 | let rec rev_append l1 l2 = |
---|
| 147 | match l1 with |
---|
| 148 | | Nil -> l2 |
---|
| 149 | | Cons (a, tl) -> rev_append tl (Cons (a, l2)) |
---|
| 150 | |
---|
| 151 | (** val reverse : 'a1 list -> 'a1 list **) |
---|
| 152 | let reverse l = |
---|
| 153 | rev_append l Nil |
---|
| 154 | |
---|
| 155 | (** val length : 'a1 list -> Nat.nat **) |
---|
| 156 | let rec length = function |
---|
| 157 | | Nil -> Nat.O |
---|
| 158 | | Cons (a, tl) -> Nat.S (length tl) |
---|
| 159 | |
---|
| 160 | type mem = __ |
---|
| 161 | |
---|
| 162 | (** val split_rev : |
---|
| 163 | 'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **) |
---|
| 164 | let rec split_rev l acc = function |
---|
| 165 | | Nat.O -> { Types.fst = acc; Types.snd = l } |
---|
| 166 | | Nat.S m -> |
---|
| 167 | (match l with |
---|
| 168 | | Nil -> { Types.fst = acc; Types.snd = Nil } |
---|
| 169 | | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m) |
---|
| 170 | |
---|
| 171 | (** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **) |
---|
| 172 | let split l n = |
---|
| 173 | let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in |
---|
| 174 | { Types.fst = (reverse l1); Types.snd = l2 } |
---|
| 175 | |
---|
| 176 | (** val flatten : 'a1 list list -> 'a1 list **) |
---|
| 177 | let flatten l = |
---|
| 178 | foldr append Nil l |
---|
| 179 | |
---|
| 180 | (** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **) |
---|
| 181 | let rec nth n l d = |
---|
| 182 | match n with |
---|
| 183 | | Nat.O -> hd l d |
---|
| 184 | | Nat.S m -> nth m (tail l) d |
---|
| 185 | |
---|
| 186 | (** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **) |
---|
| 187 | let rec nth_opt n = function |
---|
| 188 | | Nil -> Types.None |
---|
| 189 | | Cons (h, t) -> |
---|
| 190 | (match n with |
---|
| 191 | | Nat.O -> Types.Some h |
---|
| 192 | | Nat.S m -> nth_opt m t) |
---|
| 193 | |
---|
| 194 | type all = __ |
---|
| 195 | |
---|
| 196 | type allr = __ |
---|
| 197 | |
---|
| 198 | type exists = __ |
---|
| 199 | |
---|
| 200 | (** val fold : |
---|
| 201 | ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1 |
---|
| 202 | list -> 'a2 **) |
---|
| 203 | let rec fold op b p f = function |
---|
| 204 | | Nil -> b |
---|
| 205 | | Cons (a, l0) -> |
---|
| 206 | (match p a with |
---|
| 207 | | Bool.True -> op (f a) (fold op b p f l0) |
---|
| 208 | | Bool.False -> fold op b p f l0) |
---|
| 209 | |
---|
| 210 | type 'a aop = |
---|
| 211 | 'a -> 'a -> 'a |
---|
| 212 | (* singleton inductive, whose constructor was mk_Aop *) |
---|
| 213 | |
---|
| 214 | (** val aop_rect_Type4 : |
---|
| 215 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 216 | let rec aop_rect_Type4 nil h_mk_Aop x_861 = |
---|
| 217 | let op = x_861 in h_mk_Aop op __ __ __ |
---|
| 218 | |
---|
| 219 | (** val aop_rect_Type5 : |
---|
| 220 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 221 | let rec aop_rect_Type5 nil h_mk_Aop x_863 = |
---|
| 222 | let op = x_863 in h_mk_Aop op __ __ __ |
---|
| 223 | |
---|
| 224 | (** val aop_rect_Type3 : |
---|
| 225 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 226 | let rec aop_rect_Type3 nil h_mk_Aop x_865 = |
---|
| 227 | let op = x_865 in h_mk_Aop op __ __ __ |
---|
| 228 | |
---|
| 229 | (** val aop_rect_Type2 : |
---|
| 230 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 231 | let rec aop_rect_Type2 nil h_mk_Aop x_867 = |
---|
| 232 | let op = x_867 in h_mk_Aop op __ __ __ |
---|
| 233 | |
---|
| 234 | (** val aop_rect_Type1 : |
---|
| 235 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 236 | let rec aop_rect_Type1 nil h_mk_Aop x_869 = |
---|
| 237 | let op = x_869 in h_mk_Aop op __ __ __ |
---|
| 238 | |
---|
| 239 | (** val aop_rect_Type0 : |
---|
| 240 | 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **) |
---|
| 241 | let rec aop_rect_Type0 nil h_mk_Aop x_871 = |
---|
| 242 | let op = x_871 in h_mk_Aop op __ __ __ |
---|
| 243 | |
---|
| 244 | (** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **) |
---|
| 245 | let rec op nil xxx = |
---|
| 246 | let yyy = xxx in yyy |
---|
| 247 | |
---|
| 248 | (** val aop_inv_rect_Type4 : |
---|
| 249 | 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) -> |
---|
| 250 | 'a2 **) |
---|
| 251 | let aop_inv_rect_Type4 x2 hterm h1 = |
---|
| 252 | let hcut = aop_rect_Type4 x2 h1 hterm in hcut __ |
---|
| 253 | |
---|
| 254 | (** val aop_inv_rect_Type3 : |
---|
| 255 | 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) -> |
---|
| 256 | 'a2 **) |
---|
| 257 | let aop_inv_rect_Type3 x2 hterm h1 = |
---|
| 258 | let hcut = aop_rect_Type3 x2 h1 hterm in hcut __ |
---|
| 259 | |
---|
| 260 | (** val aop_inv_rect_Type2 : |
---|
| 261 | 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) -> |
---|
| 262 | 'a2 **) |
---|
| 263 | let aop_inv_rect_Type2 x2 hterm h1 = |
---|
| 264 | let hcut = aop_rect_Type2 x2 h1 hterm in hcut __ |
---|
| 265 | |
---|
| 266 | (** val aop_inv_rect_Type1 : |
---|
| 267 | 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) -> |
---|
| 268 | 'a2 **) |
---|
| 269 | let aop_inv_rect_Type1 x2 hterm h1 = |
---|
| 270 | let hcut = aop_rect_Type1 x2 h1 hterm in hcut __ |
---|
| 271 | |
---|
| 272 | (** val aop_inv_rect_Type0 : |
---|
| 273 | 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) -> |
---|
| 274 | 'a2 **) |
---|
| 275 | let aop_inv_rect_Type0 x2 hterm h1 = |
---|
| 276 | let hcut = aop_rect_Type0 x2 h1 hterm in hcut __ |
---|
| 277 | |
---|
| 278 | (** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **) |
---|
| 279 | let aop_discr a2 x y = |
---|
| 280 | Logic.eq_rect_Type2 x |
---|
| 281 | (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y |
---|
| 282 | |
---|
| 283 | (** val dpi1__o__op : |
---|
| 284 | 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **) |
---|
| 285 | let dpi1__o__op x1 x3 = |
---|
| 286 | op x1 x3.Types.dpi1 |
---|
| 287 | |
---|
| 288 | (** val lhd : 'a1 list -> Nat.nat -> 'a1 list **) |
---|
| 289 | let rec lhd l = function |
---|
| 290 | | Nat.O -> Nil |
---|
| 291 | | Nat.S n0 -> |
---|
| 292 | (match l with |
---|
| 293 | | Nil -> Nil |
---|
| 294 | | Cons (a, l0) -> Cons (a, (lhd l0 n0))) |
---|
| 295 | |
---|
| 296 | (** val ltl : 'a1 list -> Nat.nat -> 'a1 list **) |
---|
| 297 | let rec ltl l = function |
---|
| 298 | | Nat.O -> l |
---|
| 299 | | Nat.S n0 -> ltl (tail l) n0 |
---|
| 300 | |
---|
| 301 | (** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **) |
---|
| 302 | let rec find f = function |
---|
| 303 | | Nil -> Types.None |
---|
| 304 | | Cons (h, t) -> |
---|
| 305 | (match f h with |
---|
| 306 | | Types.None -> find f t |
---|
| 307 | | Types.Some b -> Types.Some b) |
---|
| 308 | |
---|
| 309 | (** val position_of_aux : |
---|
| 310 | ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **) |
---|
| 311 | let rec position_of_aux found l acc = |
---|
| 312 | match l with |
---|
| 313 | | Nil -> Types.None |
---|
| 314 | | Cons (h, t) -> |
---|
| 315 | (match found h with |
---|
| 316 | | Bool.True -> Types.Some acc |
---|
| 317 | | Bool.False -> position_of_aux found t (Nat.S acc)) |
---|
| 318 | |
---|
| 319 | (** val position_of : |
---|
| 320 | ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **) |
---|
| 321 | let position_of found l = |
---|
| 322 | position_of_aux found l Nat.O |
---|
| 323 | |
---|
| 324 | (** val make_list : 'a1 -> Nat.nat -> 'a1 list **) |
---|
| 325 | let rec make_list a = function |
---|
| 326 | | Nat.O -> Nil |
---|
| 327 | | Nat.S m -> Cons (a, (make_list a m)) |
---|
| 328 | |
---|