API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Aug 17th, 2017
74
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 20.10 KB | None | 0 0
raw download clone embed print report
  1. ascii_dec =
  2. fun a b : ascii =>
  3. let H :=
  4. ascii_rec (fun a0 : ascii => forall b0 : ascii, {a0 = b0} + {a0 <> b0})
  5. (fun (b0 b1 b2 b3 b4 b5 b6 b7 : bool) (b8 : ascii) =>
  6. match
  7. b8 as a0
  8. return
  9. ({Ascii b0 b1 b2 b3 b4 b5 b6 b7 = a0} +
  10. {Ascii b0 b1 b2 b3 b4 b5 b6 b7 <> a0})
  11. with
  12. | Ascii b9 b10 b11 b12 b13 b14 b15 b16 =>
  13. sumbool_rec
  14. (fun _ : {b0 = b9} + {b0 <> b9} =>
  15. {Ascii b0 b1 b2 b3 b4 b5 b6 b7 =
  16. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  17. {Ascii b0 b1 b2 b3 b4 b5 b6 b7 <>
  18. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  19. (fun a0 : b0 = b9 =>
  20. eq_rec_r
  21. (fun b17 : bool =>
  22. {Ascii b17 b1 b2 b3 b4 b5 b6 b7 =
  23. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  24. {Ascii b17 b1 b2 b3 b4 b5 b6 b7 <>
  25. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  26. (sumbool_rec
  27. (fun _ : {b1 = b10} + {b1 <> b10} =>
  28. {Ascii b9 b1 b2 b3 b4 b5 b6 b7 =
  29. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  30. {Ascii b9 b1 b2 b3 b4 b5 b6 b7 <>
  31. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  32. (fun a1 : b1 = b10 =>
  33. eq_rec_r
  34. (fun b17 : bool =>
  35. {Ascii b9 b17 b2 b3 b4 b5 b6 b7 =
  36. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  37. {Ascii b9 b17 b2 b3 b4 b5 b6 b7 <>
  38. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  39. (sumbool_rec
  40. (fun _ : {b2 = b11} + {b2 <> b11} =>
  41. {Ascii b9 b10 b2 b3 b4 b5 b6 b7 =
  42. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  43. {Ascii b9 b10 b2 b3 b4 b5 b6 b7 <>
  44. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  45. (fun a2 : b2 = b11 =>
  46. eq_rec_r
  47. (fun b17 : bool =>
  48. {Ascii b9 b10 b17 b3 b4 b5 b6 b7 =
  49. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  50. {Ascii b9 b10 b17 b3 b4 b5 b6 b7 <>
  51. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  52. (sumbool_rec
  53. (fun _ : {b3 = b12} + {b3 <> b12} =>
  54. {Ascii b9 b10 b11 b3 b4 b5 b6 b7 =
  55. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  56. {Ascii b9 b10 b11 b3 b4 b5 b6 b7 <>
  57. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  58. (fun a3 : b3 = b12 =>
  59. eq_rec_r
  60. (fun b17 : bool =>
  61. {Ascii b9 b10 b11 b17 b4 b5 b6 b7 =
  62. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  63. {Ascii b9 b10 b11 b17 b4 b5 b6 b7 <>
  64. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  65. (sumbool_rec
  66. (fun _ : {b4 = b13} + {b4 <> b13} =>
  67. {Ascii b9 b10 b11 b12 b4 b5 b6 b7 =
  68. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  69. {Ascii b9 b10 b11 b12 b4 b5 b6 b7 <>
  70. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  71. (fun a4 : b4 = b13 =>
  72. eq_rec_r
  73. (fun b17 : bool =>
  74. {Ascii b9 b10 b11 b12 b17 b5 b6 b7 =
  75. Ascii b9 b10 b11 b12 b13 b14 b15 b16} +
  76. {Ascii b9 b10 b11 b12 b17 b5 b6 b7 <>
  77. Ascii b9 b10 b11 b12 b13 b14 b15 b16})
  78. (sumbool_rec
  79. (fun _ : {b5 = b14} + {b5 <> b14} =>
  80. {Ascii b9 b10 b11 b12 b13 b5 b6 b7 =
  81. Ascii b9 b10 b11 b12 b13 b14 b15
  82. b16} +
  83. {Ascii b9 b10 b11 b12 b13 b5 b6 b7 <>
  84. Ascii b9 b10 b11 b12 b13 b14 b15
  85. b16})
  86. (fun a5 : b5 = b14 =>
  87. eq_rec_r
  88. (fun b17 : bool =>
  89. {Ascii b9 b10 b11 b12 b13 b17 b6
  90. b7 =
  91. Ascii b9 b10 b11 b12 b13 b14
  92. b15 b16} +
  93. {Ascii b9 b10 b11 b12 b13 b17 b6
  94. b7 <>
  95. Ascii b9 b10 b11 b12 b13 b14
  96. b15 b16})
  97. (sumbool_rec
  98. (fun
  99. _ : {b6 = b15} +
  100. {b6 <> b15} =>
  101. {Ascii b9 b10 b11 b12 b13 b14
  102. b6 b7 =
  103. Ascii b9 b10 b11 b12 b13 b14
  104. b15 b16} +
  105. {Ascii b9 b10 b11 b12 b13 b14
  106. b6 b7 <>
  107. Ascii b9 b10 b11 b12 b13 b14
  108. b15 b16})
  109. (fun a6 : b6 = b15 =>
  110. eq_rec_r
  111. (fun b17 : bool =>
  112. {. = .} + {. <> .})
  113. (sumbool_rec
  114. (fun . => . + .)
  115. (fun . =>
  116. eq_rec_r . . a7)
  117. (fun . => right . .)
  118. (bool_dec b7 b16)) a6)
  119. (fun diseq : b6 <> b15 =>
  120. right
  121. (Ascii b9 b10 b11 b12 b13
  122. b14 b6 b7 =
  123. Ascii b9 b10 b11 b12 b13
  124. b14 b15 b16)
  125. (fun absurd : . = . =>
  126. diseq (. .)))
  127. (bool_dec b6 b15)) a5)
  128. (fun diseq : b5 <> b14 =>
  129. right
  130. (Ascii b9 b10 b11 b12 b13 b5 b6
  131. b7 =
  132. Ascii b9 b10 b11 b12 b13 b14 b15
  133. b16)
  134. (fun
  135. absurd : Ascii b9 b10 b11 b12
  136. b13 b5 b6 b7 =
  137. Ascii b9 b10 b11 b12
  138. b13 b14 b15 b16 =>
  139. diseq
  140. (let H :=
  141. f_equal (fun . => .
  142. .
  143. end)
  144. absurd in
  145. (let H0 :=
  146. f_equal . absurd in
  147. (.) H0) H)))
  148. (bool_dec b5 b14)) a4)
  149. (fun diseq : b4 <> b13 =>
  150. right
  151. (Ascii b9 b10 b11 b12 b4 b5 b6 b7 =
  152. Ascii b9 b10 b11 b12 b13 b14 b15 b16)
  153. (fun
  154. absurd : Ascii b9 b10 b11 b12 b4 b5
  155. b6 b7 =
  156. Ascii b9 b10 b11 b12 b13
  157. b14 b15 b16 =>
  158. diseq
  159. (let H :=
  160. f_equal
  161. (fun e : ascii =>
  162. match e with
  163. | Ascii _ _ _ _ b21 _ _ _ =>
  164. b21
  165. end) absurd in
  166. (let H0 :=
  167. f_equal
  168. (fun e : ascii =>
  169. match . with
  170. | Ascii _ _ _ _ _ b22 _ _ =>
  171. b22
  172. end) absurd in
  173. (let H1 :=
  174. f_equal (. => .) absurd in
  175. (let H2 := . in . => H5) H1) H0)
  176. H))) (bool_dec b4 b13)) a3)
  177. (fun diseq : b3 <> b12 =>
  178. right
  179. (Ascii b9 b10 b11 b3 b4 b5 b6 b7 =
  180. Ascii b9 b10 b11 b12 b13 b14 b15 b16)
  181. (fun
  182. absurd : Ascii b9 b10 b11 b3 b4 b5 b6 b7 =
  183. Ascii b9 b10 b11 b12 b13 b14 b15
  184. b16 =>
  185. diseq
  186. (let H :=
  187. f_equal
  188. (fun e : ascii =>
  189. match e with
  190. | Ascii _ _ _ b20 _ _ _ _ => b20
  191. end) absurd in
  192. (let H0 :=
  193. f_equal
  194. (fun e : ascii =>
  195. match e with
  196. | Ascii _ _ _ _ b21 _ _ _ => b21
  197. end) absurd in
  198. (let H1 :=
  199. f_equal
  200. (fun e : ascii =>
  201. match e with
  202. | Ascii _ _ _ _ _ b22 _ _ => b22
  203. end) absurd in
  204. (let H2 :=
  205. f_equal
  206. (fun e : ascii =>
  207. match . with
  208. | . b23
  209. end) absurd in
  210. (let H3 := f_equal (.) absurd in
  211. fun . . . . => H7) H2) H1) H0) H)))
  212. (bool_dec b3 b12)) a2)
  213. (fun diseq : b2 <> b11 =>
  214. right
  215. (Ascii b9 b10 b2 b3 b4 b5 b6 b7 =
  216. Ascii b9 b10 b11 b12 b13 b14 b15 b16)
  217. (fun
  218. absurd : Ascii b9 b10 b2 b3 b4 b5 b6 b7 =
  219. Ascii b9 b10 b11 b12 b13 b14 b15 b16 =>
  220. diseq
  221. (let H :=
  222. f_equal
  223. (fun e : ascii =>
  224. match e with
  225. | Ascii _ _ b19 _ _ _ _ _ => b19
  226. end) absurd in
  227. (let H0 :=
  228. f_equal
  229. (fun e : ascii =>
  230. match e with
  231. | Ascii _ _ _ b20 _ _ _ _ => b20
  232. end) absurd in
  233. (let H1 :=
  234. f_equal
  235. (fun e : ascii =>
  236. match e with
  237. | Ascii _ _ _ _ b21 _ _ _ => b21
  238. end) absurd in
  239. (let H2 :=
  240. f_equal
  241. (fun e : ascii =>
  242. match e with
  243. | Ascii _ _ _ _ _ b22 _ _ => b22
  244. end) absurd in
  245. (let H3 :=
  246. f_equal
  247. (fun e : ascii =>
  248. match e with
  249. | Ascii _ _ _ _ _ _ b23 _ => b23
  250. end) absurd in
  251. (let H4 :=
  252. f_equal (fun . => .
  253. .
  254. end) absurd in
  255. fun (_ : b6 = b15) (_ : b5 = b14)
  256. (_ : b4 = b13) (_ : b3 = b12)
  257. (H9 : b2 = b11) => H9) H3) H2) H1) H0) H)))
  258. (bool_dec b2 b11)) a1)
  259. (fun diseq : b1 <> b10 =>
  260. right
  261. (Ascii b9 b1 b2 b3 b4 b5 b6 b7 =
  262. Ascii b9 b10 b11 b12 b13 b14 b15 b16)
  263. (fun
  264. absurd : Ascii b9 b1 b2 b3 b4 b5 b6 b7 =
  265. Ascii b9 b10 b11 b12 b13 b14 b15 b16 =>
  266. diseq
  267. (let H :=
  268. f_equal
  269. (fun e : ascii =>
  270. match e with
  271. | Ascii _ b18 _ _ _ _ _ _ => b18
  272. end) absurd in
  273. (let H0 :=
  274. f_equal
  275. (fun e : ascii =>
  276. match e with
  277. | Ascii _ _ b19 _ _ _ _ _ => b19
  278. end) absurd in
  279. (let H1 :=
  280. f_equal
  281. (fun e : ascii =>
  282. match e with
  283. | Ascii _ _ _ b20 _ _ _ _ => b20
  284. end) absurd in
  285. (let H2 :=
  286. f_equal
  287. (fun e : ascii =>
  288. match e with
  289. | Ascii _ _ _ _ b21 _ _ _ => b21
  290. end) absurd in
  291. (let H3 :=
  292. f_equal
  293. (fun e : ascii =>
  294. match e with
  295. | Ascii _ _ _ _ _ b22 _ _ => b22
  296. end) absurd in
  297. (let H4 :=
  298. f_equal
  299. (fun e : ascii =>
  300. match e with
  301. | Ascii _ _ _ _ _ _ b23 _ => b23
  302. end) absurd in
  303. (let H5 :=
  304. f_equal
  305. (fun e : ascii =>
  306. match . with
  307. | Ascii _ _ _ _ _ _ _ b24 => b24
  308. end) absurd in
  309. fun (_ : b6 = b15) (_ : b5 = b14)
  310. (_ : b4 = b13) (_ : b3 = b12) (_ : b2 = b11)
  311. (H11 : b1 = b10) => H11) H4) H3) H2) H1) H0)
  312. H))) (bool_dec b1 b10)) a0)
  313. (fun diseq : b0 <> b9 =>
  314. right
  315. (Ascii b0 b1 b2 b3 b4 b5 b6 b7 =
  316. Ascii b9 b10 b11 b12 b13 b14 b15 b16)
  317. (fun
  318. absurd : Ascii b0 b1 b2 b3 b4 b5 b6 b7 =
  319. Ascii b9 b10 b11 b12 b13 b14 b15 b16 =>
  320. diseq
  321. (let H :=
  322. f_equal
  323. (fun e : ascii =>
  324. match e with
  325. | Ascii b17 _ _ _ _ _ _ _ => b17
  326. end) absurd in
  327. (let H0 :=
  328. f_equal
  329. (fun e : ascii =>
  330. match e with
  331. | Ascii _ b18 _ _ _ _ _ _ => b18
  332. end) absurd in
  333. (let H1 :=
  334. f_equal
  335. (fun e : ascii =>
  336. match e with
  337. | Ascii _ _ b19 _ _ _ _ _ => b19
  338. end) absurd in
  339. (let H2 :=
  340. f_equal
  341. (fun e : ascii =>
  342. match e with
  343. | Ascii _ _ _ b20 _ _ _ _ => b20
  344. end) absurd in
  345. (let H3 :=
  346. f_equal
  347. (fun e : ascii =>
  348. match e with
  349. | Ascii _ _ _ _ b21 _ _ _ => b21
  350. end) absurd in
  351. (let H4 :=
  352. f_equal
  353. (fun e : ascii =>
  354. match e with
  355. | Ascii _ _ _ _ _ b22 _ _ => b22
  356. end) absurd in
  357. (let H5 :=
  358. f_equal
  359. (fun e : ascii =>
  360. match e with
  361. | Ascii _ _ _ _ _ _ b23 _ => b23
  362. end) absurd in
  363. (let H6 :=
  364. f_equal
  365. (fun e : ascii =>
  366. match e with
  367. | Ascii _ _ _ _ _ _ _ b24 => b24
  368. end) absurd in
  369. fun (_ : b6 = b15) (_ : b5 = b14) (_ : b4 = b13)
  370. (_ : b3 = b12) (_ : b2 = b11) (_ : b1 = b10)
  371. (H13 : b0 = b9) => H13) H5) H4) H3) H2) H1) H0) H)))
  372. (bool_dec b0 b9)
  373. end) a in
  374. H b
  375. : forall a b : ascii, {a = b} + {a <> b}
  376.  
  377. Argument scopes are [char_scope char_scope]
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!