yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • fe5c16361a Add definition for algorithmic domain Yiyun Liu 2025-02-19 17:40:56 -05:00
  • df0b955e4e Add the stub for Equations but might give up later Yiyun Liu 2025-02-19 16:04:02 -05:00
  • d48d9db1b7 Finish the conversion proof completely Yiyun Liu 2025-02-17 23:31:12 -05:00
  • 9c5eb31edf Finish all cases of subtyping Yiyun Liu 2025-02-17 22:50:25 -05:00
  • 735c7f2046 Prove some simple soundness cases of subtyping Yiyun Liu 2025-02-17 21:43:21 -05:00
  • 067ae89b1d Finish soundness for subtyping Yiyun Liu 2025-02-17 18:34:48 -05:00
  • ef3de3af3d Add the specification for algorithmic subtyping Yiyun Liu 2025-02-16 23:53:14 -05:00
  • 8daaae9831 Minor Yiyun Liu 2025-02-16 23:39:56 -05:00
  • eaf59fc45e Finish all cases of algorithmic completeness Yiyun Liu 2025-02-16 23:25:32 -05:00
  • 21d9a2ce1b Add standardization_lo Yiyun Liu 2025-02-16 23:00:23 -05:00
  • bdba6f50e5 Finish the soundness proof completely Yiyun Liu 2025-02-16 22:43:56 -05:00
  • d24991e994 Finish most of the neu abs case Yiyun Liu 2025-02-16 20:41:57 -05:00
  • 49a254fbef Finish the pair pair case Yiyun Liu 2025-02-16 19:51:08 -05:00
  • 60a4eb886f Finish injectivity for pairs Yiyun Liu 2025-02-16 19:14:54 -05:00
  • 06d420aa7e Add stubs for lemmas needed for completeness Yiyun Liu 2025-02-16 01:22:15 -05:00
  • 0f48a485be Prove some impossible cases Yiyun Liu 2025-02-16 01:13:41 -05:00
  • 3fb6d411e7 Finish most of the pi pi case Yiyun Liu 2025-02-15 17:22:43 -05:00
  • 926c2284a5 Finish the pair pair case Yiyun Liu 2025-02-15 16:39:05 -05:00
  • 9d951a24c5 Add standardization theorem for djoin Yiyun Liu 2025-02-15 14:31:31 -05:00
  • 67f91970d6 Finish the admitted inversion lemmas that depend on SN Yiyun Liu 2025-02-15 14:04:04 -05:00
  • 9bd554b513 Add injectivity lemma for abs Yiyun Liu 2025-02-14 21:55:44 -05:00
  • 300530a93f Finish off some easy contradictory cases Yiyun Liu 2025-02-14 21:31:27 -05:00
  • f0c18fd77e Finish the neutral app case Yiyun Liu 2025-02-14 21:11:27 -05:00
  • 8d765c495d Add some more injection lemmas for neutrals Yiyun Liu 2025-02-14 20:41:56 -05:00
  • 186f2138e6 Finish the var base case Yiyun Liu 2025-02-14 19:08:41 -05:00
  • 8fd6919538 Make progress on coqeq_complete Yiyun Liu 2025-02-14 16:57:53 -05:00
  • ea14ba9602 Prove most of cases of AbsAbs Yiyun Liu 2025-02-14 16:17:02 -05:00
  • 5ed366f093 Prove some easy cases of completeness Yiyun Liu 2025-02-14 14:49:19 -05:00
  • 093fc8f9cb Finish algo_metric_case Yiyun Liu 2025-02-14 13:29:44 -05:00
  • 849169be7f Start coqeq_complete Yiyun Liu 2025-02-13 17:46:35 -05:00
  • 0a70be3e57 Define the size metric for the completeness proof Yiyun Liu 2025-02-13 17:09:58 -05:00
  • 1f1b8a83db Pull out some inversion lemmas to prove later Yiyun Liu 2025-02-12 22:00:44 -05:00
  • 1d3920fce1 Prove the case for pair and neutral Yiyun Liu 2025-02-12 21:13:47 -05:00
  • ba77752329 Add more cases to the soundness proof Yiyun Liu 2025-02-12 20:18:12 -05:00
  • 48adb34946 Add simplified projection lemma Yiyun Liu 2025-02-12 19:53:20 -05:00
  • d053f93100 Finish the app neutral case Yiyun Liu 2025-02-12 19:27:42 -05:00
  • fa80294c5d Minor Yiyun Liu 2025-02-12 16:40:51 -05:00
  • 761e96f414 Use the abstract tactic to finish off the symmetric casesa Yiyun Liu 2025-02-12 16:14:51 -05:00
  • 5ac2bf1c40 Minor Yiyun Liu 2025-02-12 15:56:35 -05:00
  • 823f61d89f Finish most cases of the soundness proof Yiyun Liu 2025-02-12 15:54:42 -05:00
  • 15f8a9c687 Try a few cases of soundness Yiyun Liu 2025-02-11 19:15:06 -05:00
  • c1a8e9d2e1 Add the top-level subject reduction theorem Yiyun Liu 2025-02-10 21:51:27 -05:00
  • c5de86339f Finish subject reduction Yiyun Liu 2025-02-10 21:50:23 -05:00
  • bccf6eb860 Add Coquand's algorithm Yiyun Liu 2025-02-10 18:40:42 -05:00
  • 8105b5c410 Add admissible simple rules Yiyun Liu 2025-02-10 17:01:40 -05:00
  • 8f8f428562 Finish preservation Yiyun Liu 2025-02-10 14:16:43 -05:00
  • 5918fdf47e Prove all but 5 cases of regularity Yiyun Liu 2025-02-10 13:51:35 -05:00
  • 26e3c1c42a Add some cases for regularity Yiyun Liu 2025-02-10 01:15:44 -05:00
  • c8e84ef93c Finish morphing Yiyun Liu 2025-02-10 00:17:01 -05:00
  • 2c47d78ad6 Add stub for morphing Yiyun Liu 2025-02-09 23:32:07 -05:00
  • ea1fba8ae9 Finish syntactic renaming Yiyun Liu 2025-02-09 20:41:27 -05:00
  • 881b2e3825 Add missing premise Yiyun Liu 2025-02-09 17:05:43 -05:00
  • df5c6bf0b1 Minor Yiyun Liu 2025-02-09 17:05:36 -05:00
  • 20bf38a3ca Fix the fundamental theorem yet again Yiyun Liu 2025-02-09 16:46:17 -05:00
  • 5b925e3fa1 Add beta and eta rules to syntactic typing Yiyun Liu 2025-02-09 16:33:43 -05:00
  • 133968dd23 Add semantic eta laws for pair Yiyun Liu 2025-02-09 16:25:34 -05:00
  • ab1bd8eef8 Add semantic rules for function beta and eta Yiyun Liu 2025-02-09 16:12:57 -05:00
  • 4396786701 Reformulate renaming Yiyun Liu 2025-02-08 22:56:45 -05:00
  • 932662d5d9 Finish soundness proof Yiyun Liu 2025-02-08 22:52:50 -05:00
  • 0c83044d72 Update the typing rules with projections Yiyun Liu 2025-02-08 22:45:07 -05:00
  • 5996c45526 Finish the semantic projection rules Yiyun Liu 2025-02-08 22:38:28 -05:00
  • 02e6c9e025 Add pi and sig subtyping semantic rules Yiyun Liu 2025-02-08 22:15:04 -05:00
  • 916e0bcd75 Change the conversion rules to use Sub instead of Eq Yiyun Liu 2025-02-08 21:06:51 -05:00
  • f483d63f01 Fix the definition of semleq Yiyun Liu 2025-02-08 20:37:46 -05:00
  • 0746e9a354 Finish subtyping semantics Yiyun Liu 2025-02-07 16:45:58 -05:00
  • 4bc08e1897 Add one interpuniv sub case Yiyun Liu 2025-02-07 01:19:19 -05:00
  • 707483d401 Add injectivity for subtyping Yiyun Liu 2025-02-07 00:43:12 -05:00
  • 2f4ea2c78b Add more noconfusion lemmas for untyped subtyping Yiyun Liu 2025-02-07 00:39:34 -05:00
  • cf2726be8d Add subtyping Yiyun Liu 2025-02-06 23:41:38 -05:00
  • 0e5b82b162 Move projection axioms to the subtyping relation Yiyun Liu 2025-02-06 21:40:26 -05:00
  • 2e2e41cbe6 Add missing Univ rule Yiyun Liu 2025-02-06 18:15:25 -05:00
  • 6daa275ac8 Prove the fundamental theorem Yiyun Liu 2025-02-06 18:09:19 -05:00
  • 399c97fa82 Add the semantic well-typedness rules to the hint db Yiyun Liu 2025-02-06 17:58:38 -05:00
  • 8d92f19d74 Add all(?) typing rules Yiyun Liu 2025-02-06 17:47:34 -05:00
  • 10f339c5b6 Add some syntactic typing rules Yiyun Liu 2025-02-06 17:00:04 -05:00
  • 82e21196c2 Minor Yiyun Liu 2025-02-06 16:31:50 -05:00
  • e7a26e6bd6 Finish all Bind proj lemmas Yiyun Liu 2025-02-06 16:20:56 -05:00
  • c25bac311c Add the first-component inversion lemma for pi and sigma Yiyun Liu 2025-02-06 16:02:03 -05:00
  • aca7ebaf1e Finish all the semantic theory for the system with type-directed eq Yiyun Liu 2025-02-06 15:42:35 -05:00
  • 733e86c611 Finish SE_Pair Yiyun Liu 2025-02-06 15:20:40 -05:00
  • 435c0e037e Finish (simplified) SE_Bind Yiyun Liu 2025-02-06 14:37:56 -05:00
  • 1258ac263c Add structural rule for ctx equivalence Yiyun Liu 2025-02-06 14:37:25 -05:00
  • db911cff36 Finish the context equality lemma Yiyun Liu 2025-02-06 14:31:42 -05:00
  • 286ceeed39 Need to extend the notion of semwt to cover arbitrarily scoped terms Yiyun Liu 2025-02-06 13:53:01 -05:00
  • fecac84977 Set up interpretation for typed equality Yiyun Liu 2025-02-06 13:21:30 -05:00
  • cd3b4981c7 Merge pull request 'logrelnew' (#1) from logrelnew into master Yiyun Liu 2025-02-06 00:26:45 -05:00
  • c24cc7c9b0 Finish ST Conv logrelnew Yiyun Liu 2025-02-06 00:08:02 -05:00
  • 64bcf8e9c1 Finish Proj case Yiyun Liu 2025-02-05 23:56:47 -05:00
  • d6a96430f0 Add semantic typing Yiyun Liu 2025-02-05 21:44:35 -05:00
  • 55ccc2bc1d Prove the enhanced interpuniv bind inversion principle Yiyun Liu 2025-02-05 21:28:39 -05:00
  • 4134fbdada Finish InterpUniv_Join Yiyun Liu 2025-02-05 21:20:37 -05:00
  • 76f8c32dad Finish the hard fun case for interpuniv_join Yiyun Liu 2025-02-05 21:14:31 -05:00
  • 1997e8bc12 Side step the need for join subst Yiyun Liu 2025-02-05 20:36:39 -05:00
  • 7cc6435ea3 Finish most of InterpUniv join Yiyun Liu 2025-02-05 20:06:03 -05:00
  • af224831e4 Finish the injectivity of bind and noconfusion Yiyun Liu 2025-02-05 18:56:47 -05:00
  • e444c8408f Show that sne and bind are not joinable Yiyun Liu 2025-02-05 16:52:25 -05:00
  • 0e254c5ac3 Start the proof that joinability preserves meaning Yiyun Liu 2025-02-05 15:47:51 -05:00
  • 7f29fe0347 Add induction principle for InterpUniv Yiyun Liu 2025-02-05 14:44:26 -05:00
  • 2393cc5103 Finish adequacy ext Yiyun Liu 2025-02-05 14:04:44 -05:00
  • f83af1241b Merge remote-tracking branch 'origin/logrel' into logrelnew Yiyun Liu 2025-02-05 13:46:08 -05:00