Yiyun Liu
|
0e04a7076b
|
Prove PairEta
|
2025-04-19 00:24:09 -04:00 |
|
|
|
2b92845e3e
|
Add E_AppEta
|
2025-04-18 16:38:34 -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 |
|
|
|
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 |
|
|
|
96b3139726
|
Prove termination
|
2025-03-06 15:39:27 -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 |
|
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 |
|
Yiyun Liu
|
687d1be03f
|
Finish preservation
|
2025-02-25 22:35:59 -05:00 |
|
Yiyun Liu
|
d48d9db1b7
|
Finish the conversion proof completely
|
2025-02-17 23:31:12 -05:00 |
|
Yiyun Liu
|
9c5eb31edf
|
Finish all cases of subtyping
|
2025-02-17 22:50:25 -05:00 |
|
Yiyun Liu
|
735c7f2046
|
Prove some simple soundness cases of subtyping
|
2025-02-17 21:43:21 -05:00 |
|
Yiyun Liu
|
067ae89b1d
|
Finish soundness for subtyping
|
2025-02-17 18:34:48 -05:00 |
|
Yiyun Liu
|
ef3de3af3d
|
Add the specification for algorithmic subtyping
|
2025-02-16 23:53:14 -05:00 |
|
Yiyun Liu
|
8daaae9831
|
Minor
|
2025-02-16 23:39:56 -05:00 |
|
Yiyun Liu
|
eaf59fc45e
|
Finish all cases of algorithmic completeness
|
2025-02-16 23:25:32 -05:00 |
|
Yiyun Liu
|
21d9a2ce1b
|
Add standardization_lo
|
2025-02-16 23:00:23 -05:00 |
|
Yiyun Liu
|
bdba6f50e5
|
Finish the soundness proof completely
|
2025-02-16 22:43:56 -05:00 |
|
Yiyun Liu
|
d24991e994
|
Finish most of the neu abs case
|
2025-02-16 20:43:04 -05:00 |
|
Yiyun Liu
|
49a254fbef
|
Finish the pair pair case
|
2025-02-16 19:51:08 -05:00 |
|
Yiyun Liu
|
60a4eb886f
|
Finish injectivity for pairs
|
2025-02-16 19:14:54 -05:00 |
|
Yiyun Liu
|
06d420aa7e
|
Add stubs for lemmas needed for completeness
|
2025-02-16 01:22:15 -05:00 |
|
Yiyun Liu
|
0f48a485be
|
Prove some impossible cases
|
2025-02-16 01:13:41 -05:00 |
|
Yiyun Liu
|
3fb6d411e7
|
Finish most of the pi pi case
|
2025-02-15 17:22:43 -05:00 |
|
Yiyun Liu
|
926c2284a5
|
Finish the pair pair case
|
2025-02-15 16:39:05 -05:00 |
|
Yiyun Liu
|
67f91970d6
|
Finish the admitted inversion lemmas that depend on SN
|
2025-02-15 14:04:04 -05:00 |
|
Yiyun Liu
|
9bd554b513
|
Add injectivity lemma for abs
|
2025-02-14 21:55:44 -05:00 |
|
Yiyun Liu
|
300530a93f
|
Finish off some easy contradictory cases
|
2025-02-14 21:31:27 -05:00 |
|
Yiyun Liu
|
f0c18fd77e
|
Finish the neutral app case
|
2025-02-14 21:11:27 -05:00 |
|
Yiyun Liu
|
8d765c495d
|
Add some more injection lemmas for neutrals
|
2025-02-14 20:41:56 -05:00 |
|
|
|
186f2138e6
|
Finish the var base case
|
2025-02-14 19:08:41 -05:00 |
|
|
|
8fd6919538
|
Make progress on coqeq_complete
|
2025-02-14 16:57:53 -05:00 |
|
|
|
ea14ba9602
|
Prove most of cases of AbsAbs
|
2025-02-14 16:17:02 -05:00 |
|
