Commit graph

Select branches

Hide pull requests

boolean

boolean-nojunk

commute-rules

cred

erase

main

master

norm

norm-take2

norm-take3

normalization

normalization-2

sigma-type

Mono Color

• 2de1e5fa74 Recover diamond property cred Yiyun Liu 2025-01-12 23:49:31 -05:00
• 4d40dcf8d4 Finish proving commutativity Yiyun Liu 2025-01-12 23:38:15 -05:00
• 433eef83ae Two cases left! Yiyun Liu 2025-01-12 23:20:52 -05:00
• 5bd998872a Four cases left for bool Yiyun Liu 2025-01-12 22:45:06 -05:00
• f68efaf938 Add Abs EPar If Yiyun Liu 2025-01-12 22:02:19 -05:00
• 764606cf2d Prove the commutativity of cred and rred Yiyun Liu 2025-01-12 19:46:32 -05:00
• 3732757abe Parallelize cred Yiyun Liu 2025-01-12 19:22:06 -05:00
• b12872abf9 Stuck because cred is not parallel enough Yiyun Liu 2025-01-12 19:13:52 -05:00
• 95a48a380d Add RRed Yiyun Liu 2025-01-12 18:55:08 -05:00
• b48734ab12 Recover confluence for rpar and cred Yiyun Liu 2025-01-12 18:51:08 -05:00
• dd8b316a87 Prove the confluence of cred Yiyun Liu 2025-01-12 18:41:17 -05:00
• 7178a50026 bad commute-rules Yiyun Liu 2025-01-12 18:21:26 -05:00
• 76050bc511 Need to change the ifproj rules Yiyun Liu 2025-01-12 17:35:34 -05:00
• bc848e91ea Modify the definition of tstar to evaluate more aggressively Yiyun Liu 2025-01-12 16:42:09 -05:00
• c9fcafb47f Add commutativity rules for eliminators Yiyun Liu 2025-01-12 16:08:56 -05:00
• 6d9ed23de9 Add the boolean extension without junk rules boolean-nojunk Yiyun Liu 2025-01-11 00:17:04 -05:00
• d0760cd9db Stuck at commutativity (trouble with if pair) boolean Yiyun Liu 2025-01-11 00:07:30 -05:00
• 53bef034ad Add the "junk" rules for boolean Yiyun Liu 2025-01-10 22:28:53 -05:00
• bec803949f Finish Par and RPar lemmas Yiyun Liu 2025-01-10 20:51:59 -05:00
• b750ea4095 Initial commit (still tweaking the rules) Yiyun Liu 2025-01-10 16:51:49 -05:00
• 0f1e85c853 Prove injectivity of Pair and Lambdas main norm Yiyun Liu 2025-01-10 13:31:58 -05:00
• fd8335a803 Add injectivity for pairs Yiyun Liu 2025-01-10 12:39:47 -05:00
• 34a0c2856e Prove most of the confluence results for eta reduction Yiyun Liu 2025-01-09 20:21:38 -05:00
• e75d7745fe Finish normalization Yiyun Liu 2025-01-09 16:17:38 -05:00
• 0d3b751a33 . Yiyun Liu 2025-01-09 15:16:05 -05:00
• 7021497615 Finish adequacy Yiyun Liu 2025-01-09 15:15:11 -05:00
• bf2a369824 Generalize the model to talk about termination Yiyun Liu 2025-01-09 00:35:33 -05:00
• ec03826083 Add beta without the junk rules Yiyun Liu 2025-01-08 19:47:54 -05:00
• 9ab338c9e1 Add wn Yiyun Liu 2025-01-08 15:31:40 -05:00
• 602fe929bc Add pars_var_inv Yiyun Liu 2025-01-05 00:20:39 -05:00
• 489021c3e3 Add provs_par_inv norm-take3 Yiyun Liu 2025-01-05 00:20:39 -05:00
• 05d330254e Fix ERed Yiyun Liu 2025-01-04 23:59:21 -05:00
• a6fd48c009 Finish prov_extract Yiyun Liu 2025-01-04 23:38:44 -05:00
• 919f1513ce Show that prov is preserved by beta red and eta exp Yiyun Liu 2025-01-04 23:02:12 -05:00
• f0da5c97bb Show that rpar preserves prov Yiyun Liu 2025-01-04 20:38:04 -05:00
• 36e5bb5add doesn't work erase Yiyun Liu 2025-01-04 19:55:23 -05:00
• d8e040b2a6 Save normalization-2 Yiyun Liu 2025-01-04 19:26:18 -05:00
• ee7be7584c Remove unnecessary usage of Equations norm-take2 Yiyun Liu 2025-01-04 16:56:21 -05:00
• 7ffb8a912d Add some todos normalization Yiyun Liu 2025-01-04 01:48:31 -05:00
• 68207eb3bd Add a possible fix Yiyun Liu 2025-01-04 01:40:38 -05:00
• 162db5296f Stuck Yiyun Liu 2025-01-04 01:31:02 -05:00
• f699ce2d4f Add prov_antiren Yiyun Liu 2025-01-04 00:45:42 -05:00
• 9a52ab334f Finish all cases sigma-type Yiyun Liu 2024-12-31 00:04:20 -05:00
• a4682dedbe Prove all except the proj2 case Yiyun Liu 2024-12-30 23:43:15 -05:00
• 708cac5d53 Finish all except the sigma case Yiyun Liu 2024-12-30 23:00:31 -05:00
• 2f68e6c87c Finish structural rules Yiyun Liu 2024-12-30 22:07:35 -05:00
• 5347d573b5 Add semwt and its renaming lemmas Yiyun Liu 2024-12-30 21:43:41 -05:00
• 1a9cd6bda9 Start refactoring the logrel to include only closed terms Yiyun Liu 2024-12-30 20:46:43 -05:00
• dd63ebf2e9 Prove that beta-eta equivalent types have the same meaning Yiyun Liu 2024-12-30 15:52:35 -05:00
• 86b8043215 Prove the pi case for interpext_join Yiyun Liu 2024-12-30 14:11:43 -05:00
• d12de328b6 Generalize ProdSpace to BindSpace Yiyun Liu 2024-12-30 13:12:52 -05:00
• 2fe0d33592 Minor Yiyun Liu 2024-12-29 22:36:15 -05:00
• 6eba80ed70 Combine the different prov cases into one function Yiyun Liu 2024-12-29 22:33:37 -05:00
• 8fc90f5935 Save Yiyun Liu 2024-12-27 14:32:41 -05:00
• 1fd0ffe04d Minor Yiyun Liu 2024-12-27 12:15:44 -05:00
• 7f4c31b14e Generalize Pi to TBind so we have both sigma and pi Yiyun Liu 2024-12-27 12:12:19 -05:00
• 368c83dd8e Add the statement that the logrel respects beta eta laws Yiyun Liu 2024-12-27 02:09:34 -05:00
• 8e0f9a1e0a Add the logical relation Yiyun Liu 2024-12-27 01:38:25 -05:00
• 1bd6a8508e
  Create README.md Yiyun Liu 2024-12-25 21:15:48 -05:00
• 80d8b13e49 Prove join univ pi contra Yiyun Liu 2024-12-25 21:11:58 -05:00
• e2702ed277 Add join pi inj Yiyun Liu 2024-12-25 20:15:55 -05:00
• 98a11fb7ac Remove funext from Equations Yiyun Liu 2024-12-25 19:59:13 -05:00
• 22c7eff954 No admits Yiyun Liu 2024-12-25 18:09:20 -05:00
• efc3662f31 Add erpars.picong Yiyun Liu 2024-12-25 18:05:49 -05:00
• a6f89ef7f7 Add abs and paircong Yiyun Liu 2024-12-25 17:55:47 -05:00
• ff0a54aaae Add ERPars.AppCong Yiyun Liu 2024-12-25 17:48:37 -05:00
• 2e49ff6667 Finish hindley rosen Yiyun Liu 2024-12-25 17:33:56 -05:00
• ce29464f08 Make progress on par epar Yiyun Liu 2024-12-25 13:49:45 -05:00
• a34afed3d5 Add ERPar Yiyun Liu 2024-12-25 13:40:51 -05:00
• 2b26735fff One admit left Yiyun Liu 2024-12-25 13:15:52 -05:00
• 2d20d06fd2 Finish anti-renaming Yiyun Liu 2024-12-25 13:11:12 -05:00
• add8a62d85 Almost done! Yiyun Liu 2024-12-25 01:57:46 -05:00
• 3de6dae199 Note: Changed the definition of extract! Yiyun Liu 2024-12-25 01:51:50 -05:00
• 3cb40ccb9e Minor Yiyun Liu 2024-12-25 01:24:56 -05:00
• c0faae5d8a Proof the termination of extract Yiyun Liu 2024-12-25 01:22:28 -05:00
• 9bba98d411 Finish most of the pi injectivity proof Yiyun Liu 2024-12-25 01:11:49 -05:00
• 213d3f1d58 Prove prov_extract Yiyun Liu 2024-12-25 01:01:59 -05:00
• 2050b08004 Finish (most of) prov_par Yiyun Liu 2024-12-25 00:16:26 -05:00
• 2478c0f2e1 Add prov ren Yiyun Liu 2024-12-24 23:50:02 -05:00
• a1c4d5e6a8 Add induction principle Yiyun Liu 2024-12-24 22:57:28 -05:00
• cbe9941046 Need to tweak the definition of Prov Yiyun Liu 2024-12-24 15:31:50 -05:00
• c6edc1b0be Add prov function (WIP) Yiyun Liu 2024-12-24 01:19:42 -05:00
• 46ec21b763 Add pi type Yiyun Liu 2024-12-24 01:09:02 -05:00
• 90b24b259b Add confluence proof for EPar and RPar Yiyun Liu 2024-12-24 00:52:06 -05:00
• 0407bc7bb9 Finish diamond property for RPar Yiyun Liu 2024-12-24 00:37:42 -05:00
• 7b86311260 Prove diamond for EPar Yiyun Liu 2024-12-24 00:12:42 -05:00
• 233f229b3f Add Abs_EPar' Yiyun Liu 2024-12-23 23:44:57 -05:00
• 86dab74384 Add outermost expansion and some related lemmas Yiyun Liu 2024-12-23 01:13:55 -05:00
• a38a6eb8e8 Stuck at diamodn property Yiyun Liu 2024-12-22 23:51:01 -05:00
• df9c91dad5 Start EPar_diamond Yiyun Liu 2024-12-22 16:06:36 -05:00
• 6daef9c807 Finish full commutativity Yiyun Liu 2024-12-22 15:44:48 -05:00
• 4599c1d65d Finish commutativity proof Yiyun Liu 2024-12-22 15:22:41 -05:00
• fbe0bc4acc Finish Pair EPar Yiyun Liu 2024-12-22 15:08:01 -05:00
• 086e68f43e Prove one Pair EPar case Yiyun Liu 2024-12-22 12:40:20 -05:00
• ecee278d04 Write down the statement of pair_epar Yiyun Liu 2024-12-22 12:12:25 -05:00
• ccbb9a1395 Simplify the syntax by combining proj1 and proj2 Yiyun Liu 2024-12-22 10:38:58 -05:00
• e8ec23a3e7 Add the substitution lemmas for RPars Yiyun Liu 2024-12-21 22:36:14 -05:00
• 2bffbcaf0c Work on RPar morphing Yiyun Liu 2024-12-21 00:57:00 -05:00
• 7e4b0f3e81 Minor Yiyun Liu 2024-12-21 00:05:42 -05:00
• ec19e91a47 Finish Abs_EPar Yiyun Liu 2024-12-20 23:58:44 -05:00