Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
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
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 17:01:54 -05:00
8105b5c410 Add admissible simple rules
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 14:16:47 -05:00
8f8f428562 Finish preservation
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 13:51:43 -05:00
5918fdf47e Prove all but 5 cases of regularity