| e0f3026 | Meven | 31 May 2021, 11:05:35 UTC | congruence closure with conv_pb to handle co-/equivariance | 31 May 2021, 11:05:35 UTC |
| 53891af | Meven | 31 May 2021, 11:04:56 UTC | nits on dependency graphs | 31 May 2021, 11:04:56 UTC |
| c0b0b61 | Meven | 31 May 2021, 11:04:18 UTC | removing dependency of position on equality | 31 May 2021, 11:04:18 UTC |
| 2267a80 | Meven | 31 May 2021, 10:59:53 UTC | moving this coercion in a sensible place | 31 May 2021, 10:59:53 UTC |
| 1f11263 | Meven | 28 May 2021, 16:40:43 UTC | now Reduction is mostly a consequence of CongrClosure | 28 May 2021, 16:40:43 UTC |
| 36be5f7 | Meven | 28 May 2021, 08:53:34 UTC | some easy corollaries | 28 May 2021, 16:39:53 UTC |
| c9ae950 | Meven | 27 May 2021, 17:01:00 UTC | proven congr_all closure of rt-closure of congr1 closure | 27 May 2021, 17:02:19 UTC |
| 643fa10 | Meven | 26 May 2021, 16:27:05 UTC | early work on one-hole congruence | 26 May 2021, 16:27:05 UTC |
| 5e61a8a | Meven | 10 May 2021, 13:36:57 UTC | pre-work of beta-eta commutation | 10 May 2021, 13:36:57 UTC |
| 2bbc380 | Meven | 03 May 2021, 14:52:39 UTC | getting to the end of EtaEquality left parts of decidability aside for now | 03 May 2021, 14:52:39 UTC |
| ec54796 | Meven | 30 April 2021, 13:47:56 UTC | made EtaEquality.v buildable | 30 April 2021, 13:47:56 UTC |
| 1934ee4 | Meven | 30 April 2021, 10:25:31 UTC | transitive, substitutive eq_term, finally | 30 April 2021, 10:25:31 UTC |
| 3b8ce12 | Meven | 29 April 2021, 14:47:35 UTC | transitivity goes through, but non-substitutive relation | 29 April 2021, 14:47:35 UTC |
| becb33c | Meven | 29 April 2021, 08:20:39 UTC | adding contexts, not solving anything | 29 April 2021, 08:21:43 UTC |
| 633fed9 | Meven | 28 April 2021, 15:48:13 UTC | removing napp | 28 April 2021, 15:48:13 UTC |
| d7ea375 | Meven | 22 April 2021, 07:51:31 UTC | transitivity counter-example | 23 April 2021, 08:21:31 UTC |
| 7ac21a2 | Meven | 21 April 2021, 14:31:36 UTC | unlift_eq | 23 April 2021, 08:21:31 UTC |
| 1e9f4d9 | Meven | 21 April 2021, 09:39:30 UTC | eta equality, induction principle and symmetry the end of the file is copy-pasted garbage to be updated | 23 April 2021, 08:21:31 UTC |
| 0f7d22f | Matthieu Sozeau | 22 April 2021, 17:22:59 UTC | Progress in subject reduction, iota case closed | 22 April 2021, 17:22:59 UTC |
| a9163f5 | Matthieu Sozeau | 21 April 2021, 17:58:38 UTC | Progress in SR proof, at case | 21 April 2021, 17:58:38 UTC |
| b280775 | Matthieu Sozeau | 11 April 2021, 15:25:33 UTC | Fix implicits of `env_prop_*` | 11 April 2021, 15:25:33 UTC |
| fb06aac | Matthieu Sozeau | 10 April 2021, 16:47:43 UTC | Updated alpha-conversion proof, minor change in PCUICTyping | 10 April 2021, 16:47:43 UTC |
| e33ce67 | Matthieu Sozeau | 25 March 2021, 19:15:08 UTC | Some cleaning up | 30 March 2021, 00:33:55 UTC |
| 9bde3ae | Matthieu Sozeau | 25 March 2021, 16:57:22 UTC | Completed Inductive Inversion! | 25 March 2021, 16:57:22 UTC |
| 7af55a9 | Matthieu Sozeau | 24 March 2021, 23:55:33 UTC | Almost finished with Inductive Inversion: only an alpha-equivalence remains! | 24 March 2021, 23:55:33 UTC |
| 7795007 | Matthieu Sozeau | 24 March 2021, 11:53:03 UTC | WIP in positivity | 24 March 2021, 11:53:03 UTC |
| 608a915 | Matthieu Sozeau | 23 March 2021, 09:49:24 UTC | WIP in inductive inversion | 23 March 2021, 09:49:24 UTC |
| 8d9bc33 | Matthieu Sozeau | 23 March 2021, 01:59:29 UTC | WIP updating cumulativity proofs in inductive inversion | 23 March 2021, 01:59:29 UTC |
| e57be4d | Matthieu Sozeau | 22 March 2021, 22:40:28 UTC | Updated Validity ! | 22 March 2021, 22:40:28 UTC |
| 1f44455 | Matthieu Sozeau | 22 March 2021, 15:39:00 UTC | Finished updating PCUICSpine | 22 March 2021, 15:39:00 UTC |
| 0d15803 | Matthieu Sozeau | 18 March 2021, 22:02:35 UTC | WIP in PCUICSpine | 18 March 2021, 22:02:35 UTC |
| c849ae7 | Matthieu Sozeau | 18 March 2021, 02:50:34 UTC | WIP in Spines... | 18 March 2021, 02:50:34 UTC |
| f03ebaa | Matthieu Sozeau | 18 March 2021, 01:33:11 UTC | More cleanups and renamings | 18 March 2021, 01:33:11 UTC |
| f6404aa | Matthieu Sozeau | 18 March 2021, 00:16:48 UTC | WIP in Arities | 18 March 2021, 00:16:48 UTC |
| c6f9184 | Matthieu Sozeau | 17 March 2021, 12:39:47 UTC | Comment in conversion | 17 March 2021, 12:39:47 UTC |
| d27cf37 | Matthieu Sozeau | 17 March 2021, 12:34:35 UTC | Uniform naming scheme for conversion/cumulativity lemmas | 17 March 2021, 12:34:35 UTC |
| d72b8b2 | Matthieu Sozeau | 17 March 2021, 10:49:22 UTC | Updated PCUICContexts | 17 March 2021, 10:49:22 UTC |
| 4c3a453 | Matthieu Sozeau | 17 March 2021, 00:14:31 UTC | Moved inversion lemmas to well-scoped conversion | 17 March 2021, 00:14:31 UTC |
| 7dc4836 | Matthieu Sozeau | 16 March 2021, 19:51:15 UTC | Finished updating conversion lemmas! Now for the more interesting stuff :) | 16 March 2021, 23:04:14 UTC |
| b9bfecf | Matthieu Sozeau | 16 March 2021, 02:05:15 UTC | Higher-level lemmas of conversion | 16 March 2021, 02:05:15 UTC |
| 2d81b05 | Matthieu Sozeau | 16 March 2021, 01:39:18 UTC | Finally finished inversion lemmas on conv/cumulativity | 16 March 2021, 01:39:18 UTC |
| c7fb7ea | Matthieu Sozeau | 12 March 2021, 21:38:43 UTC | WIP in conversion | 12 March 2021, 21:38:43 UTC |
| 7072eec | Matthieu Sozeau | 12 March 2021, 14:38:02 UTC | Changing notations | 12 March 2021, 14:46:28 UTC |
| daacfdb | Matthieu Sozeau | 12 March 2021, 14:28:28 UTC | Updating Conversion | 12 March 2021, 14:28:28 UTC |
| acc8fad | Matthieu Sozeau | 12 March 2021, 12:21:47 UTC | Finished updating context conversion | 12 March 2021, 12:21:47 UTC |
| 06e7637 | Matthieu Sozeau | 11 March 2021, 20:54:13 UTC | WIP updating context conversion, with much cleaner proofs | 11 March 2021, 20:54:13 UTC |
| 3fb2d72 | Matthieu Sozeau | 10 March 2021, 22:58:19 UTC | Finished context conversion proof | 10 March 2021, 22:58:19 UTC |
| a3aa142 | Matthieu Sozeau | 09 March 2021, 15:30:44 UTC | Convext conversion proof | 09 March 2021, 15:30:44 UTC |
| 2bc7c32 | Matthieu Sozeau | 08 March 2021, 19:14:19 UTC | Completed confluence proofs | 08 March 2021, 19:14:19 UTC |
| e009d9f | Matthieu Sozeau | 08 March 2021, 10:44:44 UTC | Almost finished with confluence... | 08 March 2021, 10:44:44 UTC |
| eefe8e8 | Matthieu Sozeau | 08 March 2021, 00:19:59 UTC | WIP adapting confluence: now applies on well-scoped terms only | 08 March 2021, 00:19:59 UTC |
| 6abad1e | Matthieu Sozeau | 06 March 2021, 18:44:27 UTC | Refactorings | 06 March 2021, 18:44:27 UTC |
| b65c047 | Matthieu Sozeau | 06 March 2021, 17:49:16 UTC | pred1_ctx_pred1 needs well-scopedness assumptions | 06 March 2021, 17:49:16 UTC |
| aca5e2f | Matthieu Sozeau | 06 March 2021, 10:20:06 UTC | Updated Confluence | 06 March 2021, 10:20:06 UTC |
| 3fbc918 | Matthieu Sozeau | 05 March 2021, 19:05:02 UTC | todo-free confluence proof | 05 March 2021, 19:05:02 UTC |
| fc8a89b | Matthieu Sozeau | 04 March 2021, 12:36:07 UTC | WIP proving that pred1 preserves free variables | 04 March 2021, 12:36:07 UTC |
| 97d5e17 | Matthieu Sozeau | 04 March 2021, 11:57:19 UTC | Finished proof of confluence with "fixed" contexts | 04 March 2021, 11:57:19 UTC |
| cbc00cd | Matthieu Sozeau | 04 March 2021, 01:40:55 UTC | Generalized triangle lemma to allow any appropriate "join" context to be passed. | 04 March 2021, 01:40:55 UTC |
| 03f0316 | Matthieu Sozeau | 03 March 2021, 19:06:54 UTC | Issue in confluence with the "fixed" contexts | 03 March 2021, 19:06:54 UTC |
| 8bf738c | Matthieu Sozeau | 02 March 2021, 16:51:07 UTC | Finished definition of rho and proof of invariance by renaming | 02 March 2021, 16:51:07 UTC |
| af01812 | Matthieu Sozeau | 02 March 2021, 10:58:06 UTC | Finished parallel reduction theory | 02 March 2021, 10:58:06 UTC |
| 8aba9a5 | Matthieu Sozeau | 26 February 2021, 11:56:37 UTC | Closer to correct statement for on_free_vars side-conditions in parallel reduction | 01 March 2021, 20:53:39 UTC |
| 66b39da | Matthieu Sozeau | 26 February 2021, 02:27:12 UTC | Proven substituion and strong substitution simultaneously | 26 February 2021, 02:27:12 UTC |
| 2d691fa | Matthieu Sozeau | 25 February 2021, 19:02:22 UTC | Try generalizing strong_substitutivity proof | 25 February 2021, 19:02:22 UTC |
| 31b7b9f | Matthieu Sozeau | 25 February 2021, 17:05:55 UTC | Proven weakening of pred1 | 25 February 2021, 17:05:55 UTC |
| ea79064 | Matthieu Sozeau | 21 February 2021, 17:13:25 UTC | Much simple statement for Parallel Reduction Weakening :) | 21 February 2021, 17:16:47 UTC |
| 35b0fed | Matthieu Sozeau | 21 February 2021, 16:53:02 UTC | Updating weakening for parallel reduction | 21 February 2021, 16:53:02 UTC |
| 845febd | Matthieu Sozeau | 21 February 2021, 03:34:39 UTC | It seems this will all work out in the end :) | 21 February 2021, 03:34:39 UTC |
| b7e0789 | Matthieu Sozeau | 21 February 2021, 02:54:54 UTC | We need induction on depths to support the "subst_context" happening in parallel reduction | 21 February 2021, 02:54:54 UTC |
| cdc4735 | Matthieu Sozeau | 20 February 2021, 21:41:20 UTC | Update wfuniverses, minor todos | 20 February 2021, 21:41:20 UTC |
| e50dbef | Matthieu Sozeau | 19 February 2021, 16:51:45 UTC | WIP updating substitution | 20 February 2021, 20:58:36 UTC |
| fe809a2 | Matthieu Sozeau | 19 February 2021, 13:34:40 UTC | Updated up to instantiation | 19 February 2021, 13:34:40 UTC |
| 9114cfa | Matthieu Sozeau | 18 February 2021, 04:39:36 UTC | Renaming updated | 18 February 2021, 04:39:36 UTC |
| 52b22a4 | Matthieu Sozeau | 18 February 2021, 02:37:45 UTC | Update Nameless | 18 February 2021, 02:37:45 UTC |
| bad37c4 | Matthieu Sozeau | 18 February 2021, 02:08:12 UTC | Update OnFreeVars | 18 February 2021, 02:08:12 UTC |
| ea2165d | Matthieu Sozeau | 17 February 2021, 17:57:30 UTC | Update equality to simpler notion for case contexts | 17 February 2021, 19:19:48 UTC |
| 77beb52 | Matthieu Sozeau | 17 February 2021, 17:18:39 UTC | WIP moving to simpler representation | 17 February 2021, 17:18:39 UTC |
| a717c03 | Matthieu Sozeau | 17 February 2021, 13:18:36 UTC | Move back to inert context for predicates/branches, simplifying everything | 17 February 2021, 13:18:36 UTC |
| f9b0aa5 | Matthieu Sozeau | 16 February 2021, 10:59:41 UTC | Refactor contexts-related lemmas for use in translation proofs | 16 February 2021, 11:36:18 UTC |
| f936a16 | Matthieu Sozeau | 16 February 2021, 04:20:05 UTC | Fix script | 16 February 2021, 04:34:53 UTC |
| 01dcee1 | Matthieu Sozeau | 16 February 2021, 04:11:35 UTC | Fix script in canonicity, len is more robust now | 16 February 2021, 04:11:35 UTC |
| 876c0aa | Matthieu Sozeau | 16 February 2021, 04:06:14 UTC | Cleanup PCUICElimination, removing old proofs | 16 February 2021, 04:06:14 UTC |
| 853b6c5 | Matthieu Sozeau | 16 February 2021, 03:45:49 UTC | No more todos in PCUIC except for the correctness proofs of translations | 16 February 2021, 04:03:36 UTC |
| 7547aac | Matthieu Sozeau | 16 February 2021, 00:17:11 UTC | Remove all TODOs in WfUniverse | 16 February 2021, 00:17:11 UTC |
| 9e4600e | Matthieu Sozeau | 15 February 2021, 23:26:47 UTC | Fill TODOs in CumulProp and Principality. | 15 February 2021, 23:26:47 UTC |
| 69f7030 | Matthieu Sozeau | 15 February 2021, 22:33:54 UTC | Minor refactorings | 15 February 2021, 22:33:54 UTC |
| 32b9b75 | Matthieu Sozeau | 14 February 2021, 21:28:11 UTC | More move of generic lemmas back in the prelude | 14 February 2021, 21:28:11 UTC |
| 5c3255f | Matthieu Sozeau | 14 February 2021, 18:29:03 UTC | Cleaned up notations in PCUICAlpha, move generic lemmas up | 14 February 2021, 18:29:03 UTC |
| aeab3a6 | Matthieu Sozeau | 14 February 2021, 17:58:48 UTC | Complete alpha-conversion proof | 14 February 2021, 17:58:48 UTC |
| c2167f0 | Matthieu Sozeau | 13 February 2021, 22:02:37 UTC | Refactor proofs so that alpha-conversion is not needed for PCUICInductiveInversion | 13 February 2021, 22:02:37 UTC |
| f748140 | Matthieu Sozeau | 13 February 2021, 15:33:47 UTC | Refactorings to finish PCUICAlpha | 13 February 2021, 15:33:47 UTC |
| 8b06578 | Matthieu Sozeau | 13 February 2021, 14:26:22 UTC | Admit free subject reduction proof | 13 February 2021, 14:26:22 UTC |
| 8d1c85d | Matthieu Sozeau | 12 February 2021, 23:25:03 UTC | Finished Subject Reduction for cases! | 12 February 2021, 23:39:46 UTC |
| fab0cae | Matthieu Sozeau | 12 February 2021, 21:51:41 UTC | Refactored wf_case_branches_types for reuse in SR proof | 12 February 2021, 21:51:41 UTC |
| 48e75f8 | Matthieu Sozeau | 12 February 2021, 04:53:21 UTC | Almost done in SR, only a refactoring is needed to avoid duplication, but all cases on case are done | 12 February 2021, 04:53:21 UTC |
| bb333db | Matthieu Sozeau | 11 February 2021, 11:05:02 UTC | Fix typing rule for SR (equivalent under context conversion) | 11 February 2021, 15:43:18 UTC |
| 75393b0 | Matthieu Sozeau | 11 February 2021, 03:06:11 UTC | Checked that congruence for params can be proved without changing the spec | 11 February 2021, 03:06:11 UTC |
| c3e2da3 | Matthieu Sozeau | 11 February 2021, 01:40:37 UTC | Finished and cleaned up iota reduction type preservation | 11 February 2021, 01:40:37 UTC |
| 31ca371 | Matthieu Sozeau | 10 February 2021, 20:08:44 UTC | Before trying subst_app_simpl instead | 10 February 2021, 20:08:50 UTC |
| 5daa2f6 | Matthieu Sozeau | 10 February 2021, 12:48:47 UTC | WIP in SR, much simpler now | 10 February 2021, 12:48:47 UTC |
