Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 16:58:07 -05:00
8fd6919538 Make progress on coqeq_complete
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 16:17:21 -05:00
ea14ba9602 Prove most of cases of AbsAbs
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 14:49:36 -05:00
5ed366f093 Prove some easy cases of completeness
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-14 13:29:53 -05:00
093fc8f9cb Finish algo_metric_case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-13 17:46:45 -05:00
849169be7f Start coqeq_complete
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-13 17:10:33 -05:00
0a70be3e57 Define the size metric for the completeness proof
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-12 22:02:20 -05:00
1f1b8a83db Pull out some inversion lemmas to prove later
1d3920fce1 Prove the case for pair and neutral
ba77752329 Add more cases to the soundness proof
48adb34946 Add simplified projection lemma
d053f93100 Finish the app neutral case
Compare 39 commits »
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 22:00:55 -05:00
1f1b8a83db Pull out some inversion lemmas to prove later
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 21:36:35 -05:00
1d3920fce1 Prove the case for pair and neutral
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 20:19:24 -05:00
ba77752329 Add more cases to the soundness proof
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 19:53:32 -05:00
48adb34946 Add simplified projection lemma
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 19:27:48 -05:00
d053f93100 Finish the app neutral case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 16:40:55 -05:00
fa80294c5d Minor
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 16:18:24 -05:00
761e96f414 Use the abstract tactic to finish off the symmetric casesa
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 15:56:38 -05:00
5ac2bf1c40 Minor
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-12 15:54:51 -05:00
823f61d89f Finish most cases of the soundness proof
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-11 19:19:00 -05:00
15f8a9c687 Try a few cases of soundness
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 21:51:38 -05:00
c1a8e9d2e1 Add the top-level subject reduction theorem
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 21:50:29 -05:00
c5de86339f Finish subject reduction
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 18:40:47 -05:00
bccf6eb860 Add Coquand's algorithm