sp-eta-postpone

yiyunliu/sp-eta-postpone

Fork 0

Commit graph

0e04a7076b Prove PairEta ext-rep Yiyun Liu 2025-04-19 00:24:09 -04:00
8e083aad4b Add renaming_comp Yiyun Liu 2025-04-19 00:07:48 -04:00
2b92845e3e Add E_AppEta Yiyun Liu 2025-04-18 16:38:34 -04:00
43daff1b27 Fix soundness Yiyun Liu 2025-04-18 15:46:07 -04:00
d9282fb815 Finish preservation Yiyun Liu 2025-04-18 15:42:40 -04:00
87b84794b4 Fix structural rules Yiyun Liu 2025-04-18 14:13:46 -04:00
7c985fa58e Minor Yiyun Liu 2025-04-17 16:42:57 -04:00
e1fc6b609d Add the extensional representation of pair&abs equality rules Yiyun Liu 2025-04-17 15:22:45 -04:00
a367591e9a Add extensional version of pair equality rules master Yiyun Liu 2025-04-17 15:15:58 -04:00
ef8feb63c3 Redefine semantic context well-formedness as an inductive Yiyun Liu 2025-04-17 15:07:14 -04:00
4b2bbeea6f Add SE_FunExt Yiyun Liu 2025-04-16 23:57:00 -04:00
f9d3a620f4 Remove itauto dependency as it introduces weird axioms cleanup Yiyun Liu 2025-03-11 16:27:31 -04:00
8dbef3e29e Finish refactoring Yiyun Liu 2025-03-11 16:24:57 -04:00
96ad0a4740 Add stub for the new coqleq_complete' Yiyun Liu 2025-03-11 00:14:43 -04:00
181e06ae01 Finish the completeness proof for equality Yiyun Liu 2025-03-10 23:45:19 -04:00
9d68e5d6c9 Finish the conf case Yiyun Liu 2025-03-10 23:22:09 -04:00
d1771adc48 Use hne and hf instead HRed.nf Yiyun Liu 2025-03-10 22:44:42 -04:00
30caf75002 Make progress on the refactored lemma Yiyun Liu 2025-03-10 19:58:19 -04:00
030dccb326 Finish the refactored executable_correct Yiyun Liu 2025-03-10 19:02:51 -04:00
4021d05d99 Update executable to use salgo_dom for subtyping Yiyun Liu 2025-03-10 18:18:42 -04:00
e278c6eaef Define salgo_dom Yiyun Liu 2025-03-10 16:22:37 -04:00
4cbd2ac0fd Save Yiyun Liu 2025-03-10 15:35:43 -04:00
849d19708e Add new definition of algo_dom Yiyun Liu 2025-03-10 14:30:36 -04:00
437c97455e Finish the soundness and completeness proof of the subtyping algorithm unscoped Yiyun Liu 2025-03-06 20:42:08 -05:00
fe52d78ec5 Start the soundness proof for check_sub Yiyun Liu 2025-03-06 19:20:54 -05:00
6f154cc9c6 Add stub for check_sub Yiyun Liu 2025-03-06 16:20:32 -05:00
96b3139726 Prove termination Yiyun Liu 2025-03-06 15:39:27 -05:00
b29d567ef0 Add termination Yiyun Liu 2025-03-05 00:18:28 -05:00
c4f01d7dfc Update the correctness proof of the computable function Yiyun Liu 2025-03-04 23:48:42 -05:00
c1ff0ae145 Add check_equal_conf case Yiyun Liu 2025-03-04 23:22:41 -05:00
c05bd10016 Turn off auto equations generation because it produces poor lemmas Yiyun Liu 2025-03-04 22:43:30 -05:00
68cc482479 Fix the correctness proof Yiyun Liu 2025-03-04 22:30:21 -05:00
a23be7f9b5 Simplify the definition of algo_dom Yiyun Liu 2025-03-04 22:28:18 -05:00
5087b8c6ce Add new definition of eq_view Yiyun Liu 2025-03-04 22:20:12 -05:00
dcd4465310 Finish the proof of completeness for the algorithm Yiyun Liu 2025-03-04 21:47:57 -05:00
b9b6899764 Half way done with check_equal_complete Yiyun Liu 2025-03-04 00:39:59 -05:00
0060d3fb86 Factor out the rewriting lemmas Yiyun Liu 2025-03-04 00:27:42 -05:00
87f6dcd870 Prove the soundness of the computable equality Yiyun Liu 2025-03-03 23:46:41 -05:00
36d1f95d65 Move HRed to the common .v file Yiyun Liu 2025-03-03 21:16:42 -05:00
5ac3b21331 Refactor the correctness proof of coquand's algorithm Yiyun Liu 2025-03-03 21:09:03 -05:00
3a17548a7d Minor Yiyun Liu 2025-03-03 16:01:28 -05:00
3e8ad2c5bc Work on the refactoring proof Yiyun Liu 2025-03-03 15:50:08 -05:00
fe418c2a78 Fix preservation and broken cases in logrel Yiyun Liu 2025-03-03 15:29:50 -05:00
d68adf85f4 Finish refactoring substitution lemmas Yiyun Liu 2025-03-03 15:22:59 -05:00
896d22ac9b minor Yiyun Liu 2025-03-03 01:40:12 -05:00
b3bd75ad42 Fix the typing rules Yiyun Liu 2025-03-03 01:38:22 -05:00
47e21df801 Finish refactoring logical relations Yiyun Liu 2025-03-03 01:15:21 -05:00
7f38544a1e Finish refactoring fp_red Yiyun Liu 2025-03-02 22:41:15 -05:00
551dd5c17c Fix the fv proof Yiyun Liu 2025-03-02 20:19:11 -05:00
226b196d15 Refactor half of fp_red Yiyun Liu 2025-03-02 17:35:51 -05:00
657c1325c9 Add unscoped syntax Yiyun Liu 2025-03-02 16:40:39 -05:00
3efca4160b Add noconf check bove-capretta Yiyun Liu 2025-02-28 16:39:10 -05:00
7b5e9f2562 view needs more information Yiyun Liu 2025-02-28 15:56:37 -05:00
816c73cb71 Switch to view pattern Yiyun Liu 2025-02-28 14:50:42 -05:00
ca73b5eac6 Add more cases to tm_to_eq Yiyun Liu 2025-02-28 14:42:40 -05:00
44ba3e6575 Add view Yiyun Liu 2025-02-28 14:05:26 -05:00
11bfed2d17 Finish defining the algorithm Yiyun Liu 2025-02-28 00:30:02 -05:00
757f050d92 The definition is semi-working Yiyun Liu 2025-02-27 22:27:16 -05:00
7503dea251 Seems to work but takes a million years to type check Yiyun Liu 2025-02-27 21:33:25 -05:00
6c11f5560d Need noconfusion? Yiyun Liu 2025-02-27 20:56:01 -05:00
875db75955 Add equations for check_equal Yiyun Liu 2025-02-27 20:39:55 -05:00
4509a64bf5 Finish the soundness and completeness proof with nat nat Yiyun Liu 2025-02-27 15:30:55 -05:00
e663a1a596 Finish most of the completeness proof Yiyun Liu 2025-02-27 15:06:55 -05:00
aaec928902 Make progress on the completeness proof Yiyun Liu 2025-02-27 00:07:57 -05:00
af0cac15e6 Prove some simple impossible cases Yiyun Liu 2025-02-26 19:46:00 -05:00
f8943e3a9c Finish some cases of the soundness proof Yiyun Liu 2025-02-26 16:49:02 -05:00
49bb2cca13 Finish the completeness proof Yiyun Liu 2025-02-26 15:45:40 -05:00
2a492a67de Add algorithmic rules for nat Yiyun Liu 2025-02-26 00:46:11 -05:00
687d1be03f Finish preservation Yiyun Liu 2025-02-25 22:35:59 -05:00
bb39f157ba Finish regularity Yiyun Liu 2025-02-25 21:04:32 -05:00
96bc223b0a Finish renaming and preservation Yiyun Liu 2025-02-25 20:18:40 -05:00
cc0e9219c4 Finish two cases of renaming Yiyun Liu 2025-02-25 16:50:12 -05:00
291d821d94 Add some admits to work on later Yiyun Liu 2025-02-25 16:12:44 -05:00
b2aec9c6ce Add syntactic typing rules Yiyun Liu 2025-02-25 16:06:04 -05:00
4dd2cd7cd8 Finish indzero and indsuc rules Yiyun Liu 2025-02-25 15:46:22 -05:00
890f97365c Finish the indcong rule Yiyun Liu 2025-02-25 15:29:25 -05:00
e89aaf14a0 Define cleaned up version of gamma eq Yiyun Liu 2025-02-25 15:05:08 -05:00
133bcd55c2 Need to fix gamma eq Yiyun Liu 2025-02-25 12:48:42 -05:00
1effbd3d85 Finish morphing_SemWt Yiyun Liu 2025-02-24 15:20:30 -05:00
9cb7f31cdb Finish ST_Ind Yiyun Liu 2025-02-24 13:51:13 -05:00
2a24700f9a One case left for nat Yiyun Liu 2025-02-24 01:25:10 -05:00
5544e401a2 Make some progress on the ST_Ind case Yiyun Liu 2025-02-24 01:06:47 -05:00
8df64ef989 Write down the statement for ST_Ind Yiyun Liu 2025-02-23 16:01:45 -05:00
4e9a5582d2 Fix InterpUniv Sub Yiyun Liu 2025-02-23 15:18:57 -05:00
fabc39b92a Add no confusion lemmas Yiyun Liu 2025-02-23 14:58:26 -05:00
92e418666f Add the case for SNat Yiyun Liu 2025-02-23 14:33:56 -05:00
bf6d7db877 Add definition for snat Yiyun Liu 2025-02-23 14:07:16 -05:00
ffb57a91f4 Update the syntactic reduction lemmas Yiyun Liu 2025-02-23 13:58:35 -05:00
f8da81ad74 Work on local confluence Yiyun Liu 2025-02-23 01:13:44 -05:00
6b8120848b Minor Yiyun Liu 2025-02-22 01:33:47 -05:00
2ab47ac883 Finish eta postponement Yiyun Liu 2025-02-22 01:29:24 -05:00
f44c8ef425 Only the indsucc case remaining for postponement Yiyun Liu 2025-02-22 01:20:35 -05:00
d9d0e9cdd4 One remaining case for eta postponement Yiyun Liu 2025-02-22 00:10:18 -05:00
29d05befe9 Seemingly redundant nonelim cases Yiyun Liu 2025-02-21 23:43:43 -05:00
9f3b04d041 Finish sn red preservation Yiyun Liu 2025-02-21 22:23:38 -05:00
fc0e096c04 Add two cases for red sn preservation Yiyun Liu 2025-02-21 17:27:50 -05:00
2af49373e3 Repair epar sn preservation Yiyun Liu 2025-02-21 15:11:12 -05:00
396bddc8b3 Finish unmorphing Yiyun Liu 2025-02-21 14:35:34 -05:00
fd0b48073d Add nat type definition Yiyun Liu 2025-02-21 13:23:38 -05:00
0e0d9b20e5 Try making the cases mutually recursive? subtyping Yiyun Liu 2025-02-19 18:03:32 -05:00