Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 22:20:24 -05:00
5087b8c6ce Add new definition of eq_view
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 21:48:08 -05:00
dcd4465310 Finish the proof of completeness for the algorithm
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 00:40:14 -05:00
b9b6899764 Half way done with check_equal_complete
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 00:27:53 -05:00
0060d3fb86 Factor out the rewriting lemmas
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 23:46:55 -05:00
87f6dcd870 Prove the soundness of the computable equality
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 21:16:59 -05:00
36d1f95d65 Move HRed to the common .v file
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 21:09:25 -05:00
5ac3b21331 Refactor the correctness proof of coquand's algorithm
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 16:01:31 -05:00
3a17548a7d Minor
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:50:18 -05:00
3e8ad2c5bc Work on the refactoring proof
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:30:04 -05:00
fe418c2a78 Fix preservation and broken cases in logrel
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:23:11 -05:00
d68adf85f4 Finish refactoring substitution lemmas
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:40:15 -05:00
896d22ac9b minor
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:38:28 -05:00
b3bd75ad42 Fix the typing rules
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:15:32 -05:00
47e21df801 Finish refactoring logical relations
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 22:41:22 -05:00
7f38544a1e Finish refactoring fp_red
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 20:19:20 -05:00
551dd5c17c Fix the fv proof
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 17:35:59 -05:00
226b196d15 Refactor half of fp_red
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 16:40:55 -05:00
657c1325c9 Add unscoped syntax
yiyunliu created branch unscoped in yiyunliu/sp-eta-postpone 2025-03-02 16:40:54 -05:00
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 16:39:24 -05:00
3efca4160b Add noconf check