|
|
a367591e9a
|
Add extensional version of pair equality rules
|
2025-04-17 15:15:58 -04:00 |
|
|
|
ef8feb63c3
|
Redefine semantic context well-formedness as an inductive
|
2025-04-17 15:07:14 -04:00 |
|
|
|
4b2bbeea6f
|
Add SE_FunExt
|
2025-04-16 23:57:00 -04:00 |
|
|
|
f9d3a620f4
|
Remove itauto dependency as it introduces weird axioms
|
2025-03-11 16:27:31 -04:00 |
|
|
|
8dbef3e29e
|
Finish refactoring
|
2025-03-11 16:24:57 -04:00 |
|
|
|
96ad0a4740
|
Add stub for the new coqleq_complete'
|
2025-03-11 00:14:43 -04:00 |
|
|
|
181e06ae01
|
Finish the completeness proof for equality
|
2025-03-10 23:45:19 -04:00 |
|
|
|
9d68e5d6c9
|
Finish the conf case
|
2025-03-10 23:22:09 -04:00 |
|
|
|
d1771adc48
|
Use hne and hf instead HRed.nf
|
2025-03-10 22:44:42 -04:00 |
|
|
|
30caf75002
|
Make progress on the refactored lemma
|
2025-03-10 19:58:19 -04:00 |
|
|
|
030dccb326
|
Finish the refactored executable_correct
|
2025-03-10 19:02:51 -04:00 |
|
|
|
4021d05d99
|
Update executable to use salgo_dom for subtyping
|
2025-03-10 18:18:42 -04:00 |
|
|
|
e278c6eaef
|
Define salgo_dom
|
2025-03-10 16:22:37 -04:00 |
|
|
|
4cbd2ac0fd
|
Save
|
2025-03-10 15:35:43 -04:00 |
|
|
|
849d19708e
|
Add new definition of algo_dom
|
2025-03-10 14:30:36 -04:00 |
|
|
|
437c97455e
|
Finish the soundness and completeness proof of the subtyping algorithm
|
2025-03-06 20:42:08 -05:00 |
|
|
|
fe52d78ec5
|
Start the soundness proof for check_sub
|
2025-03-06 19:20:54 -05:00 |
|
|
|
6f154cc9c6
|
Add stub for check_sub
|
2025-03-06 16:20:32 -05:00 |
|
|
|
96b3139726
|
Prove termination
|
2025-03-06 15:39:27 -05:00 |
|
Yiyun Liu
|
b29d567ef0
|
Add termination
|
2025-03-05 00:18:28 -05:00 |
|
Yiyun Liu
|
c4f01d7dfc
|
Update the correctness proof of the computable function
|
2025-03-04 23:48:42 -05:00 |
|
Yiyun Liu
|
c1ff0ae145
|
Add check_equal_conf case
|
2025-03-04 23:22:41 -05:00 |
|
Yiyun Liu
|
c05bd10016
|
Turn off auto equations generation because it produces poor lemmas
|
2025-03-04 22:43:30 -05:00 |
|
Yiyun Liu
|
68cc482479
|
Fix the correctness proof
|
2025-03-04 22:30:21 -05:00 |
|
Yiyun Liu
|
a23be7f9b5
|
Simplify the definition of algo_dom
|
2025-03-04 22:28:18 -05:00 |
|
Yiyun Liu
|
5087b8c6ce
|
Add new definition of eq_view
|
2025-03-04 22:20:12 -05:00 |
|
Yiyun Liu
|
dcd4465310
|
Finish the proof of completeness for the algorithm
|
2025-03-04 21:47:57 -05:00 |
|
|
|
b9b6899764
|
Half way done with check_equal_complete
|
2025-03-04 00:39:59 -05:00 |
|
|
|
0060d3fb86
|
Factor out the rewriting lemmas
|
2025-03-04 00:27:42 -05:00 |
|
|
|
87f6dcd870
|
Prove the soundness of the computable equality
|
2025-03-03 23:46:41 -05:00 |
|
|
|
36d1f95d65
|
Move HRed to the common .v file
|
2025-03-03 21:16:42 -05:00 |
|
|
|
5ac3b21331
|
Refactor the correctness proof of coquand's algorithm
|
2025-03-03 21:09:03 -05:00 |
|
|
|
3a17548a7d
|
Minor
|
2025-03-03 16:01:28 -05:00 |
|
|
|
3e8ad2c5bc
|
Work on the refactoring proof
|
2025-03-03 15:50:08 -05:00 |
|
|
|
fe418c2a78
|
Fix preservation and broken cases in logrel
|
2025-03-03 15:29:50 -05:00 |
|
|
|
d68adf85f4
|
Finish refactoring substitution lemmas
|
2025-03-03 15:22:59 -05:00 |
|
Yiyun Liu
|
896d22ac9b
|
minor
|
2025-03-03 01:40:12 -05:00 |
|
Yiyun Liu
|
b3bd75ad42
|
Fix the typing rules
|
2025-03-03 01:38:22 -05:00 |
|
Yiyun Liu
|
47e21df801
|
Finish refactoring logical relations
|
2025-03-03 01:15:21 -05:00 |
|
Yiyun Liu
|
7f38544a1e
|
Finish refactoring fp_red
|
2025-03-02 22:41:15 -05:00 |
|
Yiyun Liu
|
551dd5c17c
|
Fix the fv proof
|
2025-03-02 20:19:11 -05:00 |
|
|
|
226b196d15
|
Refactor half of fp_red
|
2025-03-02 17:35:51 -05:00 |
|
|
|
657c1325c9
|
Add unscoped syntax
|
2025-03-02 16:40:39 -05:00 |
|
Yiyun Liu
|
4509a64bf5
|
Finish the soundness and completeness proof with nat
|
2025-02-27 15:30:55 -05:00 |
|
Yiyun Liu
|
e663a1a596
|
Finish most of the completeness proof
|
2025-02-27 15:06:55 -05:00 |
|
Yiyun Liu
|
aaec928902
|
Make progress on the completeness proof
|
2025-02-27 00:07:57 -05:00 |
|
Yiyun Liu
|
af0cac15e6
|
Prove some simple impossible cases
|
2025-02-26 19:46:00 -05:00 |
|
|
|
f8943e3a9c
|
Finish some cases of the soundness proof
|
2025-02-26 16:49:02 -05:00 |
|
|
|
49bb2cca13
|
Finish the completeness proof
|
2025-02-26 15:45:40 -05:00 |
|
Yiyun Liu
|
2a492a67de
|
Add algorithmic rules for nat
|
2025-02-26 00:46:11 -05:00 |
|
