API tools faq
paste
Advertisement
staffehn

Untitled

staffehn
May 24th, 2017
291
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 12.14 KB | None | 0 0
raw download clone embed print report
  1. Section EValF.
  2. Fixpoint evalF (E : Env) (e : Exp) : option Val :=
  3. match e with
  4. | Error => Some VError
  5. | TryWith e1 e2 => match evalF E e1 with
  6. | Some VError => evalF E e2
  7. | other => other
  8. end
  9. | Num n => Some (VInt n)
  10. | BoolE b => Some (VBool b)
  11. | Var x => E |-l x
  12. | Plus e1 e2 => match evalF E e1, evalF E e2 with
  13. | Some (VInt v1), Some (VInt v2) => Some (VInt (v1 + v2))
  14. | Some VError, _ => Some VError
  15. | _, Some VError => Some VError
  16. | _, _ => None
  17. end
  18. | Div e1 e2 => match evalF E e1, evalF E e2 with
  19. | _, Some (VInt 0) => Some VError
  20. | Some (VInt v1), Some (VInt v2) => Some (VInt (v1 / v2))
  21. | Some VError, _ => Some VError
  22. | _, Some VError => Some VError
  23. | _, _ => None
  24. end
  25. | Less e1 e2 => match evalF E e1, evalF E e2 with
  26. | Some (VInt v1), Some (VInt v2) => Some (VBool (leb v1 v2))
  27. | Some VError, _ => Some VError
  28. | _, Some VError => Some VError
  29. | _, _ => None
  30. end
  31. | If b e1 e2 => match evalF E b with
  32. | Some (VBool true) => evalF E e1
  33. | Some (VBool false) => evalF E e2
  34. | Some VError => Some VError
  35. | _ => None
  36. end
  37. end.
  38.  
  39.  
  40.  
  41.  
  42.  
  43.  
  44.  
  45.  
  46.  
  47.  
  48. (* Längste Fallunterscheidung ever.. aber das wollte ich doch mal probieren: *)
  49. (* dafür erstmal ohne Aufgaben 3 und 4 ^^ *)
  50.  
  51. Lemma evalRAsAFunction: forall E e v,
  52. (E |-R e ⇓ v) <-> evalF E e = Some v.
  53. Proof.
  54. split; cycle 1.
  55. - generalize v as w.
  56. induction e.
  57. all: intros w H.
  58. + inversion H.
  59. constructor.
  60. + inversion H.
  61. destruct (evalF E e5) eqn:I.
  62. ++ destruct v0 eqn: J.
  63. +++ apply EvTryWithError.
  64. ++++ apply IHe1. trivial.
  65. ++++ apply IHe2. trivial.
  66. +++ apply EvTryWith.
  67. ++++ apply IHe1. trivial.
  68. ++++ inversion H1. intro. inversion H0.
  69. +++ apply EvTryWith.
  70. ++++ apply IHe1. trivial.
  71. ++++ inversion H1. intro. inversion H0.
  72. ++ inversion H1.
  73. + inversion H.
  74. constructor.
  75. + inversion H.
  76. constructor.
  77. + inversion H.
  78. constructor.
  79. trivial.
  80.  
  81.  
  82. + inversion H.
  83. destruct (evalF E e5) eqn:I.
  84. ++ destruct (v0) eqn:J.
  85. +++ inversion H1.
  86. apply EvErrorOp.
  87. ++++ left. trivial.
  88. ++++ left.
  89. apply IHe1.
  90. trivial.
  91. +++ destruct (evalF E e7) eqn:K.
  92. ++++ destruct v1 eqn:L.
  93. +++++ inversion H1.
  94. apply EvErrorOp.
  95. ++++++ left. trivial.
  96. ++++++ right.
  97. apply IHe2.
  98. trivial.
  99. +++++ inversion H1.
  100. eapply EvPlus.
  101. * apply IHe1.
  102. trivial.
  103. * apply IHe2.
  104. trivial.
  105. * trivial.
  106. +++++ inversion H1.
  107. ++++ inversion H1.
  108. +++ destruct (evalF E e7) eqn:K.
  109. ++++ destruct v1 eqn:L.
  110. +++++ inversion H1.
  111. apply EvErrorOp.
  112. ++++++ left. trivial.
  113. ++++++ right.
  114. apply IHe2.
  115. trivial.
  116. +++++ inversion H1.
  117. +++++ inversion H1.
  118. ++++ inversion H1.
  119. ++ destruct (evalF E e7) eqn:K.
  120. +++ destruct v0 eqn:L.
  121. ++++ inversion H1.
  122. apply EvErrorOp.
  123. +++++ left. trivial.
  124. +++++ right.
  125. apply IHe2.
  126. trivial.
  127. ++++ inversion H1.
  128. ++++ inversion H1.
  129. +++ inversion H1.
  130.  
  131.  
  132. + inversion H.
  133. destruct (evalF E e5) eqn:I.
  134. ++ destruct (v0) eqn:J.
  135. +++ destruct (evalF E e7) eqn:K.
  136. ++++ destruct v1 eqn:L.
  137. +++++ inversion H1.
  138. apply EvErrorOp.
  139. ++++++ right. left. trivial.
  140. ++++++ left.
  141. apply IHe1.
  142. trivial.
  143. +++++ destruct n.
  144. ++++++ inversion H1.
  145. apply EvErrorOp.
  146. +++++++ right. left. trivial.
  147. +++++++ left.
  148. apply IHe1.
  149. trivial.
  150. ++++++ inversion H1.
  151. apply EvErrorOp.
  152. +++++++ right. left. trivial.
  153. +++++++ left.
  154. apply IHe1.
  155. trivial.
  156. +++++ inversion H1.
  157. apply EvErrorOp.
  158. ++++++ right. left. trivial.
  159. ++++++ left.
  160. apply IHe1.
  161. trivial.
  162. ++++ inversion H1.
  163. apply EvErrorOp.
  164. +++++ right. left. trivial.
  165. +++++ left.
  166. apply IHe1.
  167. trivial.
  168. +++ destruct (evalF E e7) eqn:K.
  169. ++++ destruct v1 eqn:L.
  170. +++++ inversion H1.
  171. apply EvErrorOp.
  172. ++++++ right. left. trivial.
  173. ++++++ right.
  174. apply IHe2.
  175. trivial.
  176. +++++ destruct n0.
  177. ++++++ inversion H1.
  178. eapply EvDivError.
  179. * apply IHe2.
  180. trivial.
  181. ++++++ inversion H1.
  182. eapply EvDiv.
  183. * apply IHe1.
  184. trivial.
  185. * apply IHe2.
  186. trivial.
  187. * intro.
  188. inversion H0.
  189. * trivial.
  190. +++++ inversion H1.
  191. ++++ inversion H1.
  192. +++ destruct (evalF E e7) eqn:K.
  193. ++++ destruct v1 eqn:L.
  194. +++++ inversion H1.
  195. apply EvErrorOp.
  196. ++++++ right. left. trivial.
  197. ++++++ right.
  198. apply IHe2.
  199. trivial.
  200. +++++ destruct n.
  201. * inversion H1.
  202. apply EvDivError.
  203. apply IHe2.
  204. trivial.
  205. * inversion H1.
  206. +++++ inversion H1.
  207. ++++ inversion H1.
  208. ++ destruct (evalF E e7) eqn:K.
  209. +++ destruct v0 eqn:L.
  210. ++++ inversion H1.
  211. apply EvErrorOp.
  212. +++++ right. left. trivial.
  213. +++++ right.
  214. apply IHe2.
  215. trivial.
  216. ++++ destruct n.
  217. * inversion H1.
  218. apply EvDivError.
  219. apply IHe2.
  220. trivial.
  221. * inversion H1.
  222. ++++ inversion H1.
  223. +++ inversion H1.
  224.  
  225.  
  226. + inversion H.
  227. destruct (evalF E e5) eqn:I.
  228. ++ destruct (v0) eqn:J.
  229. +++ inversion H1.
  230. apply EvErrorOp.
  231. ++++ right. right. trivial.
  232. ++++ left.
  233. apply IHe1.
  234. trivial.
  235. +++ destruct (evalF E e7) eqn:K.
  236. ++++ destruct v1 eqn:L.
  237. +++++ inversion H1.
  238. apply EvErrorOp.
  239. ++++++ right. right. trivial.
  240. ++++++ right.
  241. apply IHe2.
  242. trivial.
  243. +++++ inversion H1.
  244. eapply EvLess.
  245. * apply IHe1.
  246. trivial.
  247. * apply IHe2.
  248. trivial.
  249. * trivial.
  250. +++++ inversion H1.
  251. ++++ inversion H1.
  252. +++ destruct (evalF E e7) eqn:K.
  253. ++++ destruct v1 eqn:L.
  254. +++++ inversion H1.
  255. apply EvErrorOp.
  256. ++++++ right. right. trivial.
  257. ++++++ right.
  258. apply IHe2.
  259. trivial.
  260. +++++ inversion H1.
  261. +++++ inversion H1.
  262. ++++ inversion H1.
  263. ++ destruct (evalF E e7) eqn:K.
  264. +++ destruct v0 eqn:L.
  265. ++++ inversion H1.
  266. apply EvErrorOp.
  267. +++++ right. right. trivial.
  268. +++++ right.
  269. apply IHe2.
  270. trivial.
  271. ++++ inversion H1.
  272. ++++ inversion H1.
  273. +++ inversion H1.
  274.  
  275.  
  276. + inversion H.
  277. destruct (evalF E e5) eqn:I.
  278. ++ destruct v0.
  279. * inversion H1.
  280. apply EvIfError.
  281. apply IHe1.
  282. trivial.
  283. * inversion H1.
  284. * destruct b.
  285. ** apply EvIfTrue.
  286. *** apply IHe1.
  287. trivial.
  288. *** apply IHe2.
  289. trivial.
  290. ** apply EvIfFalse.
  291. *** apply IHe1.
  292. trivial.
  293. *** apply IHe3.
  294. trivial.
  295. ++ inversion H1.
  296.  
  297.  
  298.  
  299.  
  300.  
  301. - generalize v as w.
  302. induction e.
  303. all: intros w H; inversion H.
  304. -- simpl.
  305. trivial.
  306. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  307. all: rewrite I in H0; inversion H0.
  308. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  309. all: rewrite I in H0; inversion H0.
  310. -- apply IHe1 in H3.
  311. apply IHe2 in H5.
  312. simpl.
  313. rewrite H3.
  314. rewrite H5.
  315. trivial.
  316. -- apply IHe1 in H3.
  317. simpl.
  318. rewrite H3.
  319. destruct w; tauto.
  320. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  321. all: rewrite I in H0; inversion H0.
  322. -- simpl.
  323. trivial.
  324. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  325. all: rewrite I in H0; inversion H0.
  326. -- simpl.
  327. trivial.
  328. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  329. all: rewrite I in H0; inversion H0.
  330. -- simpl.
  331. apply H2.
  332. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  333. all: rewrite I in H0; inversion H0.
  334. + rewrite H6 in *.
  335. rewrite H7 in *.
  336. rewrite I.
  337. simpl.
  338. destruct H3.
  339. ++ apply IHe1 in H3.
  340. rewrite H3.
  341. trivial.
  342. ++ apply IHe2 in H3.
  343. rewrite H3.
  344. destruct (evalF E e5); try destruct v0; trivial.
  345. -- apply IHe1 in H2.
  346. apply IHe2 in H4.
  347. simpl.
  348. rewrite H2.
  349. rewrite H4.
  350. rewrite H6.
  351. trivial.
  352. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  353. all: rewrite I in H0; inversion H0.
  354. + rewrite H6 in *.
  355. rewrite H7 in *.
  356. rewrite I.
  357. simpl.
  358. destruct H3.
  359. ++ apply IHe1 in H3.
  360. rewrite H3.
  361. destruct (evalF E e7); try destruct v0; try destruct n; trivial.
  362. ++ apply IHe2 in H3.
  363. rewrite H3.
  364. destruct (evalF E e5); try destruct v0; trivial.
  365. -- apply IHe1 in H2.
  366. apply IHe2 in H3.
  367. simpl.
  368. rewrite H2.
  369. rewrite H3.
  370. destruct v2. 1: tauto.
  371. rewrite H7.
  372. trivial.
  373. -- apply IHe2 in H4.
  374. simpl.
  375. rewrite H4.
  376. destruct (evalF E e5); try destruct v0; trivial.
  377. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  378. all: rewrite I in H0; inversion H0.
  379. + rewrite H6 in *.
  380. rewrite H7 in *.
  381. rewrite I.
  382. simpl.
  383. destruct H3.
  384. ++ apply IHe1 in H3.
  385. rewrite H3.
  386. destruct (evalF E e7); trivial.
  387. ++ apply IHe2 in H3.
  388. rewrite H3.
  389. destruct (evalF E e5); try destruct v0; trivial.
  390. -- apply IHe1 in H2.
  391. apply IHe2 in H4.
  392. simpl.
  393. rewrite H2.
  394. rewrite H4.
  395. rewrite H6.
  396. trivial.
  397. -- inversion H1 as [I|H1']. 2: inversion H1' as [I|I].
  398. all: rewrite I in H0; inversion H0.
  399. -- apply IHe1 in H5.
  400. apply IHe2 in H6.
  401. simpl.
  402. rewrite H5.
  403. rewrite H6.
  404. trivial.
  405. -- apply IHe1 in H5.
  406. apply IHe3 in H6.
  407. simpl.
  408. rewrite H5.
  409. rewrite H6.
  410. trivial.
  411. -- apply IHe1 in H5.
  412. simpl.
  413. rewrite H5.
  414. trivial.
  415.  
  416. Qed.
  417.  
  418. End EValF.
  419.  
  420. Lemma inj_R: forall E e v1 v2,
  421. ((E |-R e ⇓ v1) /\ (E |-R e ⇓ v2)) -> v1 = v2.
  422. Proof.
  423. intros.
  424. destruct H as [H1 H2].
  425. apply evalRAsAFunction in H1.
  426. apply evalRAsAFunction in H2.
  427. rewrite H2 in H1.
  428. inversion H1.
  429. reflexivity.
  430. Qed.
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!