|
|
f0da5c97bb
|
Show that rpar preserves prov
|
2025-01-04 20:38:04 -05:00 |
|
|
|
ee7be7584c
|
Remove unnecessary usage of Equations
|
2025-01-04 16:56:21 -05:00 |
|
|
|
9a52ab334f
|
Finish all cases
|
2024-12-31 00:04:20 -05:00 |
|
|
|
a4682dedbe
|
Prove all except the proj2 case
|
2024-12-30 23:43:15 -05:00 |
|
|
|
708cac5d53
|
Finish all except the sigma case
|
2024-12-30 23:00:31 -05:00 |
|
|
|
2f68e6c87c
|
Finish structural rules
|
2024-12-30 22:07:35 -05:00 |
|
|
|
5347d573b5
|
Add semwt and its renaming lemmas
|
2024-12-30 21:43:41 -05:00 |
|
|
|
1a9cd6bda9
|
Start refactoring the logrel to include only closed terms
|
2024-12-30 20:46:43 -05:00 |
|
|
|
dd63ebf2e9
|
Prove that beta-eta equivalent types have the same meaning
|
2024-12-30 15:52:35 -05:00 |
|
|
|
86b8043215
|
Prove the pi case for interpext_join
|
2024-12-30 14:11:43 -05:00 |
|
|
|
d12de328b6
|
Generalize ProdSpace to BindSpace
|
2024-12-30 13:12:52 -05:00 |
|
Yiyun Liu
|
2fe0d33592
|
Minor
|
2024-12-29 22:36:15 -05:00 |
|
Yiyun Liu
|
6eba80ed70
|
Combine the different prov cases into one function
|
2024-12-29 22:33:37 -05:00 |
|
Yiyun Liu
|
8fc90f5935
|
Save
|
2024-12-27 14:32:41 -05:00 |
|
Yiyun Liu
|
1fd0ffe04d
|
Minor
|
2024-12-27 12:15:44 -05:00 |
|
Yiyun Liu
|
7f4c31b14e
|
Generalize Pi to TBind so we have both sigma and pi
|
2024-12-27 12:12:19 -05:00 |
|
Yiyun Liu
|
368c83dd8e
|
Add the statement that the logrel respects beta eta laws
|
2024-12-27 02:09:34 -05:00 |
|
Yiyun Liu
|
8e0f9a1e0a
|
Add the logical relation
|
2024-12-27 01:38:25 -05:00 |
|
Yiyun Liu
|
80d8b13e49
|
Prove join univ pi contra
|
2024-12-25 21:11:58 -05:00 |
|
Yiyun Liu
|
e2702ed277
|
Add join pi inj
|
2024-12-25 20:15:55 -05:00 |
|
Yiyun Liu
|
98a11fb7ac
|
Remove funext from Equations
|
2024-12-25 19:59:13 -05:00 |
|
Yiyun Liu
|
22c7eff954
|
No admits
|
2024-12-25 18:09:20 -05:00 |
|
Yiyun Liu
|
efc3662f31
|
Add erpars.picong
|
2024-12-25 18:05:49 -05:00 |
|
Yiyun Liu
|
a6f89ef7f7
|
Add abs and paircong
|
2024-12-25 17:55:47 -05:00 |
|
Yiyun Liu
|
ff0a54aaae
|
Add ERPars.AppCong
|
2024-12-25 17:48:37 -05:00 |
|
Yiyun Liu
|
2e49ff6667
|
Finish hindley rosen
|
2024-12-25 17:33:56 -05:00 |
|
Yiyun Liu
|
ce29464f08
|
Make progress on par epar
|
2024-12-25 13:49:45 -05:00 |
|
Yiyun Liu
|
a34afed3d5
|
Add ERPar
|
2024-12-25 13:40:51 -05:00 |
|
Yiyun Liu
|
2b26735fff
|
One admit left
|
2024-12-25 13:15:52 -05:00 |
|
Yiyun Liu
|
2d20d06fd2
|
Finish anti-renaming
|
2024-12-25 13:11:12 -05:00 |
|
Yiyun Liu
|
add8a62d85
|
Almost done!
|
2024-12-25 01:57:46 -05:00 |
|
Yiyun Liu
|
3de6dae199
|
Note: Changed the definition of extract!
|
2024-12-25 01:51:50 -05:00 |
|
Yiyun Liu
|
3cb40ccb9e
|
Minor
|
2024-12-25 01:24:56 -05:00 |
|
Yiyun Liu
|
c0faae5d8a
|
Proof the termination of extract
|
2024-12-25 01:22:28 -05:00 |
|
Yiyun Liu
|
9bba98d411
|
Finish most of the pi injectivity proof
|
2024-12-25 01:11:49 -05:00 |
|
Yiyun Liu
|
213d3f1d58
|
Prove prov_extract
|
2024-12-25 01:01:59 -05:00 |
|
Yiyun Liu
|
2050b08004
|
Finish (most of) prov_par
|
2024-12-25 00:16:26 -05:00 |
|
Yiyun Liu
|
2478c0f2e1
|
Add prov ren
|
2024-12-24 23:50:02 -05:00 |
|
Yiyun Liu
|
a1c4d5e6a8
|
Add induction principle
|
2024-12-24 22:57:28 -05:00 |
|
Yiyun Liu
|
cbe9941046
|
Need to tweak the definition of Prov
|
2024-12-24 15:31:50 -05:00 |
|
Yiyun Liu
|
c6edc1b0be
|
Add prov function (WIP)
|
2024-12-24 01:19:42 -05:00 |
|
Yiyun Liu
|
46ec21b763
|
Add pi type
|
2024-12-24 01:09:02 -05:00 |
|
Yiyun Liu
|
90b24b259b
|
Add confluence proof for EPar and RPar
|
2024-12-24 00:52:06 -05:00 |
|
Yiyun Liu
|
0407bc7bb9
|
Finish diamond property for RPar
|
2024-12-24 00:37:42 -05:00 |
|
Yiyun Liu
|
7b86311260
|
Prove diamond for EPar
|
2024-12-24 00:12:42 -05:00 |
|
Yiyun Liu
|
233f229b3f
|
Add Abs_EPar'
|
2024-12-23 23:44:57 -05:00 |
|
Yiyun Liu
|
86dab74384
|
Add outermost expansion and some related lemmas
|
2024-12-23 01:13:55 -05:00 |
|
Yiyun Liu
|
a38a6eb8e8
|
Stuck at diamodn property
|
2024-12-22 23:51:01 -05:00 |
|
Yiyun Liu
|
df9c91dad5
|
Start EPar_diamond
|
2024-12-22 16:06:36 -05:00 |
|
Yiyun Liu
|
6daef9c807
|
Finish full commutativity
|
2024-12-22 15:44:48 -05:00 |
|
