sp-eta-postpone

yiyunliu/sp-eta-postpone

Fork 0

Commit graph

38a0416b2c Add a constant to avoid kripke LR logrel Yiyun Liu 2025-02-04 22:14:27 -05:00
ee24f8093e Add logical relation for SN Yiyun Liu 2025-02-04 16:05:02 -05:00
e923194e3d Finish adding pi and sigma types Yiyun Liu 2025-02-04 15:29:47 -05:00
d9b5ef1267 Refactor the impossible case proof Yiyun Liu 2025-02-04 15:06:17 -05:00
bd7af7b297 Add README file Yiyun Liu 2025-02-03 22:47:49 -05:00
84cd0715c7 Prove structural properties of DJoin antirenaming Yiyun Liu 2025-02-03 14:55:31 -05:00
3d42581bbe Finish the confluence proof Yiyun Liu 2025-02-03 14:23:12 -05:00
f3f3991b02 Finish rred standardization Yiyun Liu 2025-02-03 12:16:56 -05:00
a0c20851fe Prove confluence of beta Yiyun Liu 2025-02-02 21:57:41 -05:00
cf31e6d285 Finish the confluence proof of ered Yiyun Liu 2025-02-02 20:48:39 -05:00
376fce619c Save progress Yiyun Liu 2025-02-02 20:21:06 -05:00
5624415bc9 Finish antirenaming for injective rens Yiyun Liu 2025-02-02 20:08:37 -05:00
6cc3a65163 Discharge one case of antirenaming using injective renaming Yiyun Liu 2025-02-02 19:42:42 -05:00
ecb50f1ab7 Add comment about the antirenaming proof Yiyun Liu 2025-01-31 21:56:58 -05:00
d2cd3105c7 stuck on antirenaming because of scoped syntax Yiyun Liu 2025-01-31 21:45:55 -05:00
580e3a8251 Prove that ered is strongly normalizing Yiyun Liu 2025-01-31 20:54:33 -05:00
f57e10be93 Finish extracting leftmost-outermost red from sn Yiyun Liu 2025-01-31 20:10:56 -05:00
571779a4dd Fix name change errors for EPar Yiyun Liu 2025-01-31 17:32:35 -05:00
5dd3428e2b Merge remote-tracking branch 'forgejo/nonessential' Yiyun Liu 2025-01-31 17:31:21 -05:00
47473fd3cd Minor nonessential Yiyun Liu 2025-01-31 16:30:06 -05:00
5a7f46a8a1 Finish the enhanced eta postponement Yiyun Liu 2025-01-30 23:29:25 -05:00
51ac5ffbd6 Finish eta postponement Yiyun Liu 2025-01-30 23:10:11 -05:00
9134cfec8a Finish a few cases of eta postponement Yiyun Liu 2025-01-30 22:18:58 -05:00
d925a8bcaa Minor cleanup Yiyun Liu 2025-01-30 20:23:57 -05:00
fc666956e2 Finish off the SN proof Yiyun Liu 2025-01-30 20:23:25 -05:00
64e558f09e Finish sn unsubst Yiyun Liu 2025-01-30 20:17:00 -05:00
c83be03230 Finish antirenaming Yiyun Liu 2025-01-30 16:14:03 -05:00
e4c2bd39db Finish the eta split proof without any admits Yiyun Liu 2025-01-29 23:41:38 -05:00
20eef78014 Finish one example case of violate sn Yiyun Liu 2025-01-29 22:59:57 -05:00
aa2c2ca151 Add lemmas that bad forms are impossible Yiyun Liu 2025-01-29 22:25:14 -05:00
a47d69f427 More no forbid Yiyun Liu 2025-01-29 22:14:01 -05:00
99b5e87ea3 Finish red sn preservation Yiyun Liu 2025-01-29 22:09:08 -05:00
369bd55932 Add red sn preservation Yiyun Liu 2025-01-29 21:27:49 -05:00
5f619c0980 Finish the split lemma up to strong normalization Yiyun Liu 2025-01-29 15:52:05 -05:00
710b59fd8f Prove all application cases Yiyun Liu 2025-01-29 14:01:35 -05:00
08b9395acb Push some important cases of the split lemma Yiyun Liu 2025-01-29 13:37:54 -05:00
a27c41c5d1 Add lemmas that bad forms are impossible tstar Yiyun Liu 2025-01-29 12:19:45 -05:00
3f3703990d Save progress Yiyun Liu 2025-01-28 16:37:23 -05:00
24693b8928 Add "beta-free" eta contraction Yiyun Liu 2025-01-28 16:07:52 -05:00
61e743ee74 Add ne ered Yiyun Liu 2025-01-28 15:13:41 -05:00
5ea75052a5 Show that eta expansion can be immediately be removed by beta Yiyun Liu 2025-01-27 22:47:10 -05:00
b8d7ebfaa2 Fix the broken pair eta rule Yiyun Liu 2025-01-27 16:48:38 -05:00
9f80013df6 Add tstar to preserve eta normal forms Yiyun Liu 2025-01-27 16:44:48 -05:00
11d23afa45 Remove the typed postponement theorem Yiyun Liu 2025-01-26 14:51:47 -05:00
263fbf7fb6 Finish most of the preservation proof Yiyun Liu 2025-01-25 23:10:29 -05:00
8463b4067f Figured out Yiyun Liu 2025-01-25 23:06:38 -05:00
df62e3691c Need to parallelize eta Yiyun Liu 2025-01-25 16:53:48 -07:00
8fcfa5dbf9 "Finish" eta postponement proof Yiyun Liu 2025-01-25 16:26:55 -07:00
2f04bcc75c Add a mostly finished eta postponement proof Yiyun Liu 2025-01-25 16:08:21 -07:00