API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Nov 19th, 2019
115
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 8.65 KB | None | 0 0
raw download clone embed print report
  1. (*
  2. The "Tm" type and the previously defined transition and closedness judgements.
  3. Do not modify these!
  4.  
  5. The task starts at line 150.
  6. *)
  7.  
  8. (* Require Import String. *)
  9. Require Import Coq.Strings.String.
  10. Require Import Coq.Lists.List.
  11. Require Import Coq.Lists.ListSet.
  12.  
  13. Open Scope string_scope.
  14. (* Open Scope list_scope. *)
  15. Import ListNotations.
  16.  
  17.  
  18. (* -=- Var -=- *)
  19.  
  20. Definition Var := string.
  21. Definition Var_dec := string_dec.
  22.  
  23. Definition x := "x".
  24. Definition y := "y".
  25. Definition z := "z".
  26.  
  27.  
  28. (* -=- Tm -=- *)
  29.  
  30. Inductive Tm : Set :=
  31. | variable (v : Var) : Tm
  32. | lambda (v : Var) (t : Tm) : Tm
  33. | application (t t' : Tm) : Tm
  34. .
  35.  
  36. Notation "' v" := (variable v) (at level 3).
  37. Notation "\ v , t" := (lambda v t) (at level 5).
  38. Notation "t $ t'" := (application t t') (at level 4).
  39.  
  40.  
  41. (* -=- Rename -=- *)
  42.  
  43. Reserved Notation "t { x |-> y }" (at level 1).
  44.  
  45. Fixpoint rename (tm : Tm) (y z : Var) : Tm :=
  46. match tm with
  47. | ' x => if x =? y then 'z else 'x
  48. | \ x , t => if x =? y then \z,t{y|->z} else \x,t{y|->z}
  49. | t $ t' => t{y|->z} $ t'{y|->z}
  50. end
  51. where "t { y |-> z }" := (rename t y z).
  52.  
  53. Compute (rename (\x,'x) x y).
  54.  
  55.  
  56. (* -=- Substitute -=- *)
  57.  
  58. Reserved Notation "t [ x |-> t' ]" (at level 2).
  59.  
  60. Fixpoint substitute (tm : Tm) (x : Var) (tm' : Tm) : Tm :=
  61. match tm with
  62. | ' y => if x =? y then tm' else ' y
  63. | \ y , t => if x =? y then \y,t else \y,t[x|->tm']
  64. | t $ t' => t[x|->tm'] $ t'[x|->tm']
  65. end
  66. where "t [ x |-> t' ]" := (substitute t x t').
  67.  
  68. Compute (' x $ (\x, 'x $ ' x))[x |-> ' z].
  69. Compute (\y,'z)[z |-> 'y].
  70.  
  71.  
  72. (* -=- context -=- *)
  73.  
  74. Definition context := list Var.
  75. Definition empty : context := nil.
  76.  
  77.  
  78. (* -=- Closed -=- *)
  79.  
  80. Inductive Closed' : context -> Tm -> Prop :=
  81. | C_variable {c : context} {v : Var} : In v c -> Closed' c ('v)
  82. | C_lambda {c : context} {v : Var} {t : Tm} : Closed' (v :: c) t -> Closed' c (\v,t)
  83. | C_application {c : context} {t t' : Tm} : Closed' c t -> Closed' c t' -> Closed' c (t $ t')
  84. .
  85.  
  86. Definition Closed := Closed' empty.
  87.  
  88. Ltac proove_closed :=
  89. repeat (
  90. (
  91. eapply C_variable;
  92. simpl;
  93. repeat (
  94. (left; reflexivity) ||
  95. right
  96. )
  97. ) ||
  98. eapply C_lambda ||
  99. eapply C_application
  100. )
  101. .
  102.  
  103.  
  104. (* -=- One Step Transition Judgement -=- *)
  105.  
  106. Reserved Notation "t |--> t'" (at level 100).
  107.  
  108. Inductive OneStepTransitionJudgement : Tm -> Tm -> Prop :=
  109.  
  110. | OSTJ_beta {x : Var} {t t1 : Tm} :
  111. Closed t1 ->
  112. ((\x,t) $ t1) |--> t[x |-> t1]
  113.  
  114. | OSTJ_lambda {x : Var} {t t' : Tm} :
  115. (t |--> t') ->
  116. \x,t |--> \x,t'
  117.  
  118. | OSTJ_application_left {t1 t1' t2 : Tm} :
  119. (t1 |--> t1') ->
  120. t1 $ t2 |--> t1' $ t2
  121.  
  122. | OSTJ_application_right {t1 t2 t2' : Tm} :
  123. (t2 |--> t2') ->
  124. t1 $ t2 |--> t1 $ t2'
  125.  
  126. where "t |--> t'" := (OneStepTransitionJudgement t t').
  127.  
  128.  
  129. (* -=- Any Step Transition Judgement -=- *)
  130.  
  131. Reserved Notation "t |-->* t'" (at level 100).
  132.  
  133. Ltac beta_reduce := eapply OSTJ_beta; (proove_closed || assumption).
  134.  
  135. Inductive AnyStepTransitionJudgement : Tm -> Tm -> Prop :=
  136. | ASTJ_refl {t : Tm} :
  137. t |-->* t
  138. | ASTJ_trans {t t'' : Tm} (t' : Tm) :
  139. (t |--> t') -> (t' |-->* t'') ->
  140. t |-->* t''
  141. where "t |-->* t'" := (AnyStepTransitionJudgement t t').
  142.  
  143. Ltac prove_closed :=
  144. repeat(
  145. ( eapply C_variable; simpl; repeat((left; reflexivity) || right))||
  146. eapply C_lambda ||
  147. eapply C_application )
  148. .
  149. Ltac beta := (eapply OSTJ_beta; prove_closed).
  150.  
  151. (* -=- true, false -=- *)
  152.  
  153. Definition true := \x,\y,'x.
  154. Definition false := \x,\y,'y.
  155.  
  156. Definition not := \x,('x $ false $ true).
  157. Definition and := \x,\y,'x $ 'y $ false.
  158. Definition or := \x,\y,('x $ true $ 'y).
  159. Definition xor := \x,\y,('x $ ('y $ false $ true) $ 'y).
  160.  
  161. (* -------------------------------------------------------------- *)
  162. Theorem not1 : not $ true |-->* false.
  163. Proof.
  164. eapply ASTJ_trans.
  165. beta.
  166. eapply ASTJ_trans.
  167. simpl.
  168. eapply OSTJ_application_left.
  169. beta.
  170. eapply ASTJ_trans.
  171. simpl.
  172. beta.
  173. simpl.
  174. eapply ASTJ_refl.
  175. Qed.
  176.  
  177. Theorem not2 : not $ false |-->* true.
  178. Proof.
  179. eapply ASTJ_trans.
  180. beta.
  181. eapply ASTJ_trans.
  182. simpl.
  183. eapply OSTJ_application_left.
  184. beta.
  185. eapply ASTJ_trans.
  186. simpl.
  187. beta.
  188. simpl.
  189. eapply ASTJ_refl.
  190. Qed.
  191.  
  192.  
  193. (* -------------------------------------------------------------- *)
  194. Lemma and1 : and $ true $ true |-->* true.
  195. Proof.
  196. eapply ASTJ_trans.
  197. eapply OSTJ_application_left.
  198. beta.
  199. simpl.
  200. eapply ASTJ_trans.
  201. beta.
  202. simpl.
  203. eapply ASTJ_trans.
  204. eapply OSTJ_application_left.
  205. beta.
  206. simpl.
  207. eapply ASTJ_trans.
  208. beta.
  209. simpl. unfold true.
  210. eapply ASTJ_refl.
  211. Qed.
  212.  
  213. Lemma and2 : and $ true $ false |-->* false.
  214. Proof.
  215. eapply ASTJ_trans.
  216. eapply OSTJ_application_left.
  217. beta.
  218. simpl.
  219.  
  220. eapply ASTJ_trans.
  221. beta.
  222. simpl.
  223.  
  224. eapply ASTJ_trans.
  225. eapply OSTJ_application_left.
  226. beta.
  227. simpl.
  228.  
  229. eapply ASTJ_trans.
  230. beta.
  231. simpl.
  232.  
  233. unfold false.
  234. eapply ASTJ_refl.
  235. Qed.
  236.  
  237. Lemma and3 : and $ false $ true |-->* false.
  238. Proof.
  239. eapply ASTJ_trans.
  240. eapply OSTJ_application_left.
  241. beta.
  242. simpl.
  243.  
  244. eapply ASTJ_trans.
  245. beta.
  246. simpl.
  247.  
  248. eapply ASTJ_trans.
  249. eapply OSTJ_application_left.
  250. beta.
  251. simpl.
  252.  
  253. eapply ASTJ_trans.
  254. beta.
  255. simpl.
  256.  
  257. unfold false.
  258. eapply ASTJ_refl.
  259.  
  260. Qed.
  261.  
  262. Lemma and4 : and $ false $ false |-->* false.
  263. Proof.
  264. eapply ASTJ_trans.
  265. eapply OSTJ_application_left.
  266. beta.
  267. simpl.
  268.  
  269. eapply ASTJ_trans.
  270. beta.
  271. simpl.
  272.  
  273. eapply ASTJ_trans.
  274. eapply OSTJ_application_left.
  275. beta.
  276. simpl.
  277.  
  278. eapply ASTJ_trans.
  279. beta.
  280. simpl.
  281.  
  282. unfold false.
  283. eapply ASTJ_refl.
  284. Qed.
  285. (* -------------------------------------------------------------- *)
  286. Theorem or1 : or $ true $ true |-->* true.
  287. Proof.
  288. eapply ASTJ_trans.
  289. eapply OSTJ_application_left.
  290. beta.
  291. simpl.
  292. eapply ASTJ_trans.
  293. beta.
  294. simpl.
  295. eapply ASTJ_trans.
  296. eapply OSTJ_application_left.
  297. beta.
  298. simpl.
  299. eapply ASTJ_trans.
  300. beta.
  301. simpl. unfold true.
  302. eapply ASTJ_refl.
  303. Qed.
  304.  
  305. Theorem or2 : or $ true $ false |-->* true.
  306. Proof.
  307. eapply ASTJ_trans.
  308. eapply OSTJ_application_left.
  309. beta.
  310.  
  311. eapply ASTJ_trans.
  312. simpl.
  313. beta.
  314.  
  315. eapply ASTJ_trans.
  316. simpl.
  317. eapply OSTJ_application_left.
  318. beta.
  319.  
  320. simpl.
  321. eapply ASTJ_trans.
  322. beta.
  323. simpl.
  324. eapply ASTJ_refl.
  325. Qed.
  326.  
  327. Theorem or3 : or $ false $ true |-->* true.
  328. Proof.
  329. eapply ASTJ_trans.
  330. eapply OSTJ_application_left.
  331. beta.
  332.  
  333. eapply ASTJ_trans.
  334. simpl.
  335. beta.
  336.  
  337. eapply ASTJ_trans.
  338. simpl.
  339. eapply OSTJ_application_left.
  340. beta.
  341.  
  342. simpl.
  343. eapply ASTJ_trans.
  344. beta.
  345. simpl.
  346. eapply ASTJ_refl.
  347. Qed.
  348.  
  349. Theorem or4 : or $ false $ false |-->* false.
  350. Proof.
  351. eapply ASTJ_trans.
  352. eapply OSTJ_application_left.
  353. beta.
  354.  
  355. eapply ASTJ_trans.
  356. simpl.
  357. beta.
  358.  
  359. eapply ASTJ_trans.
  360. simpl.
  361. eapply OSTJ_application_left.
  362. beta.
  363.  
  364. simpl.
  365. eapply ASTJ_trans.
  366. beta.
  367. simpl.
  368. eapply ASTJ_refl.
  369. Qed.
  370.  
  371. (* -------------------------------------------------------------- *)
  372. Theorem xor1 : xor $ true $ true |-->* false.
  373. Proof.
  374. eapply ASTJ_trans.
  375. eapply OSTJ_application_left.
  376. beta.
  377. simpl.
  378. eapply ASTJ_trans.
  379. beta.
  380. simpl.
  381. eapply ASTJ_trans.
  382. eapply OSTJ_application_left.
  383. beta.
  384. simpl.
  385. eapply ASTJ_trans.
  386. beta.
  387. simpl.
  388. eapply ASTJ_trans.
  389. eapply OSTJ_application_left.
  390. beta.
  391. simpl.
  392. eapply ASTJ_trans.
  393. beta.
  394. simpl.
  395. eapply ASTJ_refl.
  396. Qed.
  397.  
  398. Theorem xor2 : xor $ true $ false |-->* true.
  399. Proof.
  400. eapply ASTJ_trans.
  401. eapply OSTJ_application_left.
  402. beta.
  403. simpl.
  404. eapply ASTJ_trans.
  405. beta.
  406. simpl.
  407. eapply ASTJ_trans.
  408. eapply OSTJ_application_left.
  409. beta.
  410. simpl.
  411. eapply ASTJ_trans.
  412. beta.
  413. simpl.
  414. eapply ASTJ_trans.
  415. eapply OSTJ_application_left.
  416. beta.
  417. simpl.
  418. eapply ASTJ_trans.
  419. beta.
  420. simpl.
  421. eapply ASTJ_refl.
  422. Qed.
  423.  
  424. Theorem xor3 : xor $ false $ true |-->* true.
  425. Proof.
  426. eapply ASTJ_trans.
  427. eapply OSTJ_application_left.
  428. beta.
  429. simpl.
  430. eapply ASTJ_trans.
  431. beta.
  432. simpl.
  433. eapply ASTJ_trans.
  434. eapply OSTJ_application_left.
  435. beta.
  436. simpl.
  437. eapply ASTJ_trans.
  438. beta.
  439. simpl.
  440. eapply ASTJ_refl.
  441. Qed.
  442.  
  443. Theorem xor4 : xor $ false $ false |-->* false.
  444. Proof.
  445. eapply ASTJ_trans.
  446. eapply OSTJ_application_left.
  447. beta.
  448. simpl.
  449. eapply ASTJ_trans.
  450. beta.
  451. simpl.
  452. eapply ASTJ_trans.
  453. eapply OSTJ_application_left.
  454. beta.
  455. simpl.
  456. eapply ASTJ_trans.
  457. beta.
  458. simpl.
  459. eapply ASTJ_refl.
  460. 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!