|
|
96ad0a4740
|
Add stub for the new coqleq_complete'
|
2025-03-11 00:14:43 -04:00 |
|
|
|
d1771adc48
|
Use hne and hf instead HRed.nf
|
2025-03-10 22:44:42 -04:00 |
|
|
|
4021d05d99
|
Update executable to use salgo_dom for subtyping
|
2025-03-10 18:18:42 -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
|
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
|
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 |
|
|
|
87f6dcd870
|
Prove the soundness of the computable equality
|
2025-03-03 23:46:41 -05:00 |
|
Yiyun Liu
|
0e0d9b20e5
|
Try making the cases mutually recursive?
|
2025-02-19 18:03:32 -05:00 |
|
Yiyun Liu
|
fe5c16361a
|
Add definition for algorithmic domain
|
2025-02-19 17:40:56 -05:00 |
|
Yiyun Liu
|
df0b955e4e
|
Add the stub for Equations but might give up later
|
2025-02-19 16:04:02 -05:00 |
|
