| 008d109 | Yannick Forster | 06 July 2019, 15:31:42 UTC | Annotation for admits | 06 July 2019, 19:57:23 UTC |
| 397d95e | Yannick Forster | 06 July 2019, 15:22:27 UTC | cleanup | 06 July 2019, 19:57:23 UTC |
| a1b74ce | Yannick Forster | 06 July 2019, 15:12:18 UTC | Refactored a lot, most files are admit free, apart from EArities | 06 July 2019, 19:57:23 UTC |
| e9b1ad1 | Yannick Forster | 06 July 2019, 10:53:32 UTC | Closed main proofs, missing auxiliary stuff + termination of is_arity | 06 July 2019, 19:57:23 UTC |
| be36603 | Yannick Forster | 06 July 2019, 10:36:59 UTC | add assumption on Prop <= Type | 06 July 2019, 19:57:23 UTC |
| 272b476 | Yannick Forster | 06 July 2019, 10:09:29 UTC | Progress using inversions | 06 July 2019, 19:57:23 UTC |
| e06c594 | Yannick Forster | 06 July 2019, 10:09:21 UTC | Make merge compile | 06 July 2019, 19:57:23 UTC |
| 1770dfd | Yannick Forster | 06 July 2019, 07:26:33 UTC | Progress | 06 July 2019, 19:55:13 UTC |
| c603634 | Yannick Forster | 05 July 2019, 20:49:08 UTC | Progress | 06 July 2019, 19:55:13 UTC |
| e494db0 | Yannick Forster | 05 July 2019, 09:19:06 UTC | Cleanup | 06 July 2019, 19:55:13 UTC |
| aeb6baa | Yannick Forster | 05 July 2019, 08:47:45 UTC | axiomatise checker only | 06 July 2019, 19:55:13 UTC |
| 9925af9 | Yannick Forster | 05 July 2019, 08:34:25 UTC | Added new extraction files | 06 July 2019, 19:55:13 UTC |
| 30ef5a5 | Matthieu Sozeau | 06 July 2019, 17:59:07 UTC | Merge pull request #196 from MetaCoq/principality Principality | 06 July 2019, 17:59:07 UTC |
| cd7e68b | Théo Winterhalter | 06 July 2019, 16:51:24 UTC | Refactoring to place red1_eq_context_upto_l in the right place | 06 July 2019, 17:38:59 UTC |
| 89be771 | Théo Winterhalter | 06 July 2019, 16:33:11 UTC | Prove red1_eq_context_upto_l | 06 July 2019, 16:33:11 UTC |
| adf7b34 | Théo Winterhalter | 06 July 2019, 16:28:42 UTC | Success with OnOne2_ind_l! | 06 July 2019, 16:28:42 UTC |
| d63bbd1 | Théo Winterhalter | 06 July 2019, 16:15:25 UTC | New attempt with OnOne2 | 06 July 2019, 16:15:25 UTC |
| 7b17869 | Théo Winterhalter | 06 July 2019, 13:12:53 UTC | Try to provide a new induction principle on OnOne2 but fail to use it | 06 July 2019, 13:12:53 UTC |
| 428aaf9 | Théo Winterhalter | 06 July 2019, 11:28:18 UTC | Use term_forall_list_rec for principality | 06 July 2019, 11:28:18 UTC |
| c5ffd97 | Théo Winterhalter | 06 July 2019, 11:19:53 UTC | Fix compilation by importing Principality | 06 July 2019, 11:19:53 UTC |
| 0a9ced1 | Théo Winterhalter | 06 July 2019, 11:15:44 UTC | cumul_confluence is probably not the right lemma | 06 July 2019, 11:15:44 UTC |
| 97b915c | Théo Winterhalter | 06 July 2019, 11:11:12 UTC | Add missing Derive | 06 July 2019, 11:11:12 UTC |
| 4a4085c | Matthieu Sozeau | 06 July 2019, 06:15:42 UTC | Proven a lot of the principality cases. | 06 July 2019, 06:15:42 UTC |
| 5ff32e9 | Matthieu Sozeau | 06 July 2019, 02:02:34 UTC | WIP on principality | 06 July 2019, 02:03:06 UTC |
| ebd608c | Théo Winterhalter | 05 July 2019, 21:57:25 UTC | Merge pull request #195 from yforster/extend-utils More lemmas for utils | 05 July 2019, 21:57:25 UTC |
| 8bb2466 | Matthieu Sozeau | 05 July 2019, 21:30:10 UTC | Completing the proof of validity. (#177) * WIP fixing validity proof * Move eq_term_upto_univ to Type, fix and simplify proofs * WIP fixing validity proof Lots of additional lemmas on context_subst/subslet needed. Not being paranoid in the typing relation renders this a bit harder than strictly necessary. | 05 July 2019, 21:30:10 UTC |
| 8f0836a | Yannick Forster | 05 July 2019, 21:00:14 UTC | fix compilation | 05 July 2019, 21:00:14 UTC |
| c2ba01b | Yannick Forster | 05 July 2019, 20:58:49 UTC | more utils lemmas | 05 July 2019, 20:58:49 UTC |
| 89bc1fd | Yannick Forster | 05 July 2019, 20:51:05 UTC | re-add DestArity | 05 July 2019, 20:51:05 UTC |
| 748c2c6 | Yannick Forster | 05 July 2019, 08:31:51 UTC | Fix compilation | 05 July 2019, 20:49:37 UTC |
| 723968a | Yannick Forster | 05 July 2019, 08:14:23 UTC | Some more auxiliary lemmas | 05 July 2019, 20:49:37 UTC |
| 6104e17 | Matthieu Sozeau | 05 July 2019, 16:25:57 UTC | Merge pull request #193 from TheoWinterhalter/red-cong Proving reduction lemmata | 05 July 2019, 16:25:57 UTC |
| 6d2c244 | Théo Winterhalter | 05 July 2019, 15:16:29 UTC | Merge remote-tracking branch 'Template-Coq/coq-8.8' into red-cong | 05 July 2019, 15:16:29 UTC |
| a1b5269 | Théo Winterhalter | 05 July 2019, 14:58:48 UTC | Prove red_evar | 05 July 2019, 14:58:48 UTC |
| dee540a | Théo Winterhalter | 05 July 2019, 14:57:37 UTC | Prove red_one_evar | 05 July 2019, 14:57:37 UTC |
| b19e020 | SimonBoulier | 05 July 2019, 14:36:35 UTC | fix compilation | 05 July 2019, 14:50:38 UTC |
| f844677 | SimonBoulier | 04 April 2019, 08:04:56 UTC | WIP Safe Checker | 05 July 2019, 14:50:38 UTC |
| 27cee59 | SimonBoulier | 26 June 2019, 07:52:28 UTC | gitignore | 05 July 2019, 14:50:38 UTC |
| 12bc29d | Théo Winterhalter | 05 July 2019, 14:04:23 UTC | Prove red_prod | 05 July 2019, 14:04:23 UTC |
| dd42a1c | Théo Winterhalter | 05 July 2019, 13:54:00 UTC | Attempt at red_fix_congr, but technique need to be adapted | 05 July 2019, 13:54:00 UTC |
| f1f4047 | Théo Winterhalter | 05 July 2019, 13:37:08 UTC | red_fix_body is harder because of fix_context | 05 July 2019, 13:37:08 UTC |
| 46cb46b | Théo Winterhalter | 05 July 2019, 13:32:10 UTC | Prove red_fix_ty | 05 July 2019, 13:32:10 UTC |
| 5eeb3c2 | Théo Winterhalter | 05 July 2019, 12:45:09 UTC | Replaced admitted red_proj_congr with proven red_proj_c | 05 July 2019, 13:00:12 UTC |
| ceeba38 | Théo Winterhalter | 05 July 2019, 12:37:54 UTC | Remove duplicate red_trans | 05 July 2019, 12:37:54 UTC |
| 714025d | Théo Winterhalter | 05 July 2019, 12:26:31 UTC | Move PCUICPosition.red_mkApps | 05 July 2019, 12:32:07 UTC |
| 89d7e08 | Théo Winterhalter | 05 July 2019, 12:13:36 UTC | Move red_it_mkLambda_or_LetIn | 05 July 2019, 12:24:16 UTC |
| b840bea | Théo Winterhalter | 05 July 2019, 11:46:31 UTC | Prove reds_case (renamed to avoid clash) | 05 July 2019, 12:06:37 UTC |
| 6bd6adb | Théo Winterhalter | 05 July 2019, 11:43:50 UTC | Prove red_case_brs | 05 July 2019, 11:43:50 UTC |
| ab031d9 | Théo Winterhalter | 05 July 2019, 10:15:09 UTC | Prove red_case_one_brs | 05 July 2019, 10:15:09 UTC |
| eacbbd5 | Théo Winterhalter | 05 July 2019, 09:49:18 UTC | Minor progress | 05 July 2019, 09:49:18 UTC |
| b14aa1f | Théo Winterhalter | 05 July 2019, 09:31:46 UTC | Import PCUICReduction to fix compilation | 05 July 2019, 09:31:46 UTC |
| 75df7bd | Théo Winterhalter | 05 July 2019, 08:42:11 UTC | [WIP] Yet another unfruitful approach to red_case_one_brs in a nice way | 05 July 2019, 08:42:11 UTC |
| 095fea8 | Théo Winterhalter | 04 July 2019, 21:28:02 UTC | [WIP] New way to prove red_case | 04 July 2019, 21:28:02 UTC |
| 1c5e5e9 | Théo Winterhalter | 04 July 2019, 18:14:27 UTC | Merge pull request #192 from TheoWinterhalter/liftsubst-rename-ok Liftsubst rename ok | 04 July 2019, 18:14:27 UTC |
| 366f661 | Théo Winterhalter | 04 July 2019, 15:57:54 UTC | Fix compilation | 04 July 2019, 16:46:45 UTC |
| faaadcb | Matthieu Sozeau | 04 July 2019, 05:42:28 UTC | Fix admitted lemma with wrong assumption (missing an equality check on annotations) | 04 July 2019, 05:42:28 UTC |
| 93fa065 | Matthieu Sozeau | 04 July 2019, 05:33:57 UTC | Finished confluence: only remaining admits are in PCUICReduction: congruence for red | 04 July 2019, 05:36:48 UTC |
| 8ecaae7 | Matthieu Sozeau | 04 July 2019, 01:47:46 UTC | pred1_red1 can actually choose the left or right context | 04 July 2019, 01:47:46 UTC |
| aabcf5f | Matthieu Sozeau | 03 July 2019, 23:26:00 UTC | Finish proof of confluence for red1 without context fixing. | 03 July 2019, 23:26:18 UTC |
| 3132183 | Théo Winterhalter | 03 July 2019, 11:44:06 UTC | Add allow_cofix and prop_sub_type flags (#190) | 03 July 2019, 11:44:06 UTC |
| 57c0e40 | Matthieu Sozeau | 02 July 2019, 20:12:08 UTC | Finish proof of red -> pred1 using a kind of pred1 context conversion lemma. Separated the derived facts from parallel reduction confluence from reduction confluence. | 02 July 2019, 20:14:18 UTC |
| f1e61d3 | Matthieu Sozeau | 02 July 2019, 16:30:22 UTC | Move Confluence to ParallelReductionConfluence | 02 July 2019, 16:31:00 UTC |
| b037b12 | Théo Winterhalter | 02 July 2019, 14:47:46 UTC | Merge pull request #189 from TheoWinterhalter/squash-wf Squash wf in reduction and conversion so that it gets erased | 02 July 2019, 14:47:46 UTC |
| 93114bd | Théo Winterhalter | 02 July 2019, 12:23:38 UTC | Squash wf so that it gets erased | 02 July 2019, 12:53:06 UTC |
| 4ea7801 | Matthieu Sozeau | 02 July 2019, 02:30:10 UTC | Rebased on coq-8.8 | 02 July 2019, 02:35:24 UTC |
| a074105 | Matthieu Sozeau | 02 July 2019, 02:00:34 UTC | Updated everything to a new `unfold_fix` definition that requires fix bodies to be lambdas This is true of well-typed terms, and actually necessary to prove confluence! | 02 July 2019, 02:06:59 UTC |
| 45c5fcc | Matthieu Sozeau | 01 July 2019, 22:39:32 UTC | Confluence finished, finally! Fixpoints were real tricky! | 02 July 2019, 02:05:32 UTC |
| 6d65065 | Matthieu Sozeau | 30 June 2019, 22:50:33 UTC | Finished cofix/constructor reduction, rho_rename is proven | 02 July 2019, 02:05:32 UTC |
| 400849d | Matthieu Sozeau | 30 June 2019, 20:55:40 UTC | Finished Fix/Beta critical pair! | 02 July 2019, 02:05:32 UTC |
| d4e00ad | Matthieu Sozeau | 28 June 2019, 23:35:37 UTC | Yay, proven simplification lemma for app redexes, only remaining a good way to apply it. | 02 July 2019, 02:05:32 UTC |
| e14911b | Matthieu Sozeau | 28 June 2019, 04:17:58 UTC | Cleanup, make it compile. Only well-formedness hypotheses to finish | 02 July 2019, 02:05:32 UTC |
| 3df4bb8 | Matthieu Sozeau | 27 June 2019, 21:33:52 UTC | WIP finishing rho_rename: difficult because of the critical pairs due to n-ary fixpoints and co | 02 July 2019, 02:04:46 UTC |
| 11c5fce | Matthieu Sozeau | 27 June 2019, 07:15:33 UTC | Checked the rho_rename can be proven, cleanup a little bit | 02 July 2019, 02:04:46 UTC |
| 2d2cf01 | Matthieu Sozeau | 27 June 2019, 06:46:46 UTC | Strong substitutivity proven. Dealing with fixpoints almost finished Remains to finish the rho_rename proof too, otherwise, we have confluence! | 02 July 2019, 02:03:22 UTC |
| 2867d41 | Matthieu Sozeau | 26 June 2019, 23:22:47 UTC | Strong substitutivity proven up two delta and proj-cofix cases! | 02 July 2019, 02:03:22 UTC |
| 93971df | Matthieu Sozeau | 25 June 2019, 00:12:23 UTC | WIP proving strong substitutivity of parallel reduction | 02 July 2019, 02:03:22 UTC |
| d7a5e9b | Matthieu Sozeau | 22 June 2019, 02:50:47 UTC | WIP stating and proving renaming property of rho for variables | 02 July 2019, 02:03:22 UTC |
| 553157e | Matthieu Sozeau | 28 May 2019, 09:40:11 UTC | WIP improving notations/reasoning with \sigma-calculus, and proving confluence | 02 July 2019, 02:03:22 UTC |
| 54e05fe | Matthieu Sozeau | 26 May 2019, 14:33:27 UTC | Rename [cons/consn] to [subst_cons/consn] to avoid conflict with list [cons] | 02 July 2019, 02:03:22 UTC |
| 39e0c62 | Matthieu Sozeau | 26 May 2019, 14:28:43 UTC | Fix compilation | 02 July 2019, 02:03:22 UTC |
| 8393a21 | Matthieu Sozeau | 25 May 2019, 15:58:43 UTC | Proving all \sigma-calculus equations for `inst` version of substitution | 02 July 2019, 02:03:22 UTC |
| 2111aef | Matthieu Sozeau | 24 May 2019, 18:11:08 UTC | Show that lift/subst can also be implemented using renamings and instantiations. Idea suggested by Y. Forster. This brings \sigma-calculus primitives in, with which we can hopefully prove the lifting property of the rho function in PCUICConfluence more easily. Due to the `nat -> nat`/`nat -> term` encoding of renamings/substitutions in this presentation, we will however need to prove boring extensionality lemmas. | 02 July 2019, 02:03:22 UTC |
| cfcd181 | Matthieu Sozeau | 02 July 2019, 02:00:02 UTC | Merge pull request #188 from TheoWinterhalter/use-flags Make PCUICCumulativity generic in checker_flags | 02 July 2019, 02:00:02 UTC |
| fff27dc | Matthieu Sozeau | 01 July 2019, 19:46:44 UTC | Merge pull request #187 from TheoWinterhalter/let-lemmata Let lemmata | 01 July 2019, 19:46:44 UTC |
| ff81734 | Matthieu Sozeau | 01 July 2019, 19:04:18 UTC | Merge pull request #186 from TheoWinterhalter/fix-let Update wf_local to match LetIn | 01 July 2019, 19:04:18 UTC |
| b4a0e33 | Théo Winterhalter | 30 June 2019, 17:24:13 UTC | Make PCUICCumulativity generic in checker_flags | 30 June 2019, 17:25:17 UTC |
| 66f156f | Théo Winterhalter | 30 June 2019, 17:07:29 UTC | Prove inversion_it_mkLambda_or_LetIn Modulo checker_flags general cumulativity lemmata | 30 June 2019, 17:07:48 UTC |
| 7cbd105 | Théo Winterhalter | 30 June 2019, 17:07:02 UTC | Prove cumul_it_mkProd_or_LetIn | 30 June 2019, 17:07:48 UTC |
| 15083ba | Théo Winterhalter | 30 June 2019, 16:39:15 UTC | Derive it_mkLambda_or_LetIn_welltyped instead of proving it from scratch | 30 June 2019, 16:39:15 UTC |
| 66ad56a | Théo Winterhalter | 30 June 2019, 16:20:30 UTC | Move type_it_mkLambda_or_LetIn in PCUICGeneration Is it the right place? | 30 June 2019, 16:33:55 UTC |
| 33d74a3 | Théo Winterhalter | 29 June 2019, 18:54:03 UTC | Now prove typing lemmata for it_mkLambda_or_LetIn | 29 June 2019, 18:54:03 UTC |
| 6528d2d | Théo Winterhalter | 29 June 2019, 18:28:45 UTC | Update PCUICSR to new wf_local | 29 June 2019, 18:28:45 UTC |
| 496a726 | Théo Winterhalter | 29 June 2019, 18:17:16 UTC | Update PCUICConfluence to new wf_local | 29 June 2019, 18:24:40 UTC |
| d7994c5 | Théo Winterhalter | 29 June 2019, 18:13:16 UTC | Update PCUICParallelReduction to new wf_local | 29 June 2019, 18:13:16 UTC |
| 1747402 | Théo Winterhalter | 29 June 2019, 18:03:55 UTC | Update PCUICValidity to new wf_local | 29 June 2019, 18:03:55 UTC |
| af3b75c | Théo Winterhalter | 29 June 2019, 17:50:52 UTC | Update TemplateToPUICCorrectness to new wf_local | 29 June 2019, 17:50:52 UTC |
| 561a241 | Théo Winterhalter | 29 June 2019, 17:45:54 UTC | Update PCUICSubstitution with new wf_local | 29 June 2019, 17:45:58 UTC |
| 41c8bd0 | Théo Winterhalter | 29 June 2019, 17:18:44 UTC | Update WeakeningEnv with new wf_local | 29 June 2019, 17:18:44 UTC |
| c44df48 | Théo Winterhalter | 29 June 2019, 16:55:19 UTC | Update WeakeningEnv with new wf_local | 29 June 2019, 16:55:19 UTC |
| 5ce9648 | Théo Winterhalter | 29 June 2019, 16:28:43 UTC | Update PCUICTyping with new wf_local | 29 June 2019, 16:47:39 UTC |
