Base MLTT 1.0

This release contains the basic MLTT with natural numbers as the base type, Pi types, and a cumulative universe hierarchy with covariant universe subtyping. The release contains a normalizer, a subtyping decision procedure, a type checking procedure, and a front-end.

---

What's Changed

• Extract parser to Coq by @jinh0 in #11
• Reorganize Coq modules + AST definition by @jinh0 in #13
• Fix parser by @jinh0 in #21
• [WIP] Well-Scopedness Lemma by @IanGrenville in #12
• Merge fork into typing-rules branch by @jinh0 in #22
• Add typing rules by @jinh0 in #26
• Jason's proof for the well-scopedness lemma by @HuStmpHrrr in #24
• Add lemmas for context conversion proof by @IanGrenville in #28
• Context conversion Lemmas by @IanGrenville in #29
• Proof of syntactic validity(Presup) Lemmas by @IanGrenville in #30
• Update CI build by @IanGrenville in #37
• Update README.md by @HuStmpHrrr in #38
• Update notations by @Ailrun in #39
• Update project structure by @Ailrun in #40
• Update makefile to make extraction cleaner by @Ailrun in #41
• Update Makefile by @Ailrun in #42
• Add natural number recursor by @Ailrun in #43
• Refactor syntatic code style by @Ailrun in #45
• Add domain and related props by @Ailrun in #46
• Fix errors in Semantics by @Ailrun in #48
• Add PER definition by @Ailrun in #47
• Add helper tactic for functional relations by @Ailrun in #50
• Finish PER transitivity by @Ailrun in #49
• fix scripts by @HuStmpHrrr in #53
• attempt to remove unnecessary axioms by @HuStmpHrrr in #52
• Streamline some proofs by @Ailrun in #54
• Streamline some syntactic proofs by @Ailrun in #55
• Rearrange PER parts a bit by @Ailrun in #56
• Finish all PERs by @Ailrun in #57
• Fix per_univ_elem by @Ailrun in #58
• Remove some complexity for PER by @Ailrun in #59
• Finish Realizability for PER by @Ailrun in #60
• Some refactoring by @Ailrun in #62
• Refactor the module structure by @Ailrun in #66
• Prove cumulativity by @Ailrun in #67
• Prove PER for per_ctx_env by @Ailrun in #68
• Refactoring structure by @Ailrun in #69
• Improve proof quality by @Ailrun in #70
• Start to write the base of completeness proof by @Ailrun in #72
• Prove some cases of completeness by @Ailrun in #74
• Update some proofs by @Ailrun in #77
• define type class instances for PERs by @HuStmpHrrr in #79
• Change isomorphism between per_elem by @Ailrun in #81
• Extraction of NbE by @HuStmpHrrr in #80
• make CI parallel by @HuStmpHrrr in #83
• More completeness cases by @Ailrun in #84
• Remove depedence on axioms for PER lemmas by @Ailrun in #89
• More cases for completeness by @Ailrun in #88
• working on the logrel for soundness proof by @HuStmpHrrr in #86
• Finish completeness by @Ailrun in #90
• Add some templates by @Ailrun in #91
• add lemmas for weakenings by @HuStmpHrrr in #92
• improve presup performance by @HuStmpHrrr in #94
• Add build time check to CI by @Ailrun in #96
• Feature/logrel lemmas by @HuStmpHrrr in #93
• Refactoring and optimizing proofs by @Ailrun in #98
• Update ci_build.yml by @Ailrun in #103
• Optimize completeness proofs by @Ailrun in #102
• need a few lemmas to push through this proof by @HuStmpHrrr in #99
• (Probably) Last completeness optimization by @Ailrun in #104
• True last one by @Ailrun in #105
• Try container-based CI by @Ailrun in #106
• Add syntactic judgements for type subsumption by @Ailrun in #101
• Add helper lemmas by @Ailrun in #107
• Add inversion theorems by @Ailrun in #112
• Update inversion theorems by @Ailrun in #114
• Prove some additional lemmas by @Ailrun in #115
• Fix inversion lemmas by @Ailrun in #117
• Prove more lemmas by @Ailrun in #119
• Working on subtyping by @HuStmpHrrr in #122
• remove unnecessary hints by @HuStmpHrrr in #123
• fix tactics by @HuStmpHrrr in #126
• remove contra-variant subtyping by @HuStmpHrrr in #127
• subtyping in the PER model by @HuStmpHrrr in #128
• working on algorithmic subtyping by @HuStmpHrrr in #124
• working on completeness rules for subtyping by @HuStmpHrrr in #130
• finish completeness proof by @HuStmpHrrr in #133
• Some updates on soundness by @Ailrun in #132
• Refactor gen rewritings by @Ailrun in #137
• Prove admitted lemmas by @Ailrun in #138
• Update ci_build.yaml by @HuStmpHrrr in #139
• Provide more soundness lemmas by @Ailrun in #141
• working on realizability by @HuStmpHrrr in #140
• implement monotonicity by @HuStmpHrrr in #149
• add more morphisms by @HuStmpHrrr in #148
• Gluing Cumulativity by @Ailrun in #150
• Prove per escape lemma along gluing by @Ailrun in #151
• Prove subtyping case for soundness by @Ailrun in #153
• Rearrange soundness proofs by @Ailrun in #155
• Provide placeholders for cases by @Ailrun in #156
• Change system rules by @Ailrun in #157
• Prove all easy soundness cases by @Ailrun in #158
• working on subtyping impl by @HuStmpHrrr in #152
• Finish function cases by @Ailrun in #159
• Finish nat cases by @Ailrun in #160
• Add Algorithmic Typing Rules by @Ailrun in #163
• Implement type checker by @Ailrun in #164
• Optimize soundness a bit by @Ailrun in #165
• Reorganize code by @Ailrun in #168
• Use consistent naming by @Ailrun in #169
• Update Coq by @Ailrun in #171
• Add a more "proper" entrypoint with fuller parser by @Ailrun in #170
• update main file by @HuStmpHrrr in #178
• update build process by @HuStmpHrrr in #179
• implement a homepage by @HuStmpHrrr in #183
• Bump actions/checkout from 3 to 4 by @dependabot in #185
• Bump docker/build-push-action from 5 to 6 by @dependabot in #184
• working on homepage by @HuStmpHrrr in #186
• use string test instead by @HuStmpHrrr in #187
• Update ci_build.yaml by @HuStmpHrrr in #188
• Update ci_build.yaml by @HuStmpHrrr in #190
• Remove warnings in extraction impls by @Ailrun in #192
• recover timed CI by @HuStmpHrrr in #193
• Update header.html by @HuStmpHrrr in #194
• Update some executable related things by @Ailrun in #195
• Update OCamlFormat by @Ailrun in #196
• Update opam informations by @Ailrun in #197
• Create LICENSE by @HuStmpHrrr in #198
• Update Dockerfile by @Ailrun in #199
• Add some tests by @Ailrun in #200
• Optimizing proofs by @Ailrun in #201
• Update README.md by @HuStmpHrrr in #203
• Update ci_build.yaml by @HuStmpHrrr in #204
• exit properly by @HuStmpHrrr in #209
• Working on ocaml doc by @HuStmpHrrr in #191
• Replace special exit codes with non-reserved ones by @Ailrun in #210
• Update Mcltt.ml by @HuStmpHrrr in #211
• Use Löf consistently by @Ailrun in #212
• Update doc comments by @Ailrun in #213
• Fix weird TOC by @Ailrun in #215
• Update docker.yaml to have cache by @Ailrun in #217
• Update docker.yaml to work with cache by @Ailrun in #218
• Update ci_build.yaml by @Ailrun in #219
• Fix grammar so that sub notation is printed by @Ailrun in #220
• Generate dep svg by @Ailrun in #225
• Add graphviz to Docker image by @Ailrun in #226
• Update dockerfile by @Ailrun in #227
• Bump JamesIves/github-pages-deploy-action from 4.6.4 to 4.6.8 by @dependabot in #228
• Update presup a bit by @Ailrun in #230
• Fix graph color by @Ailrun in #232
• Prove more consequences by @Ailrun in #236
• Update escape notation by @Ailrun in #239
• Update ci_build.yaml by @HuStmpHrrr in #242
• Simplify installation steps by @HuStmpHrrr in #243
• Update semantic consequences a bit by @Ailrun in #247
• Clean up some modules by @Ailrun in #248
• Update README.md by @Ailrun in #250
• Simple let-bindings by @Antoine-something in #234
• remove redundant check by @HuStmpHrrr in #253

Full Changelog: https://github.com/Beluga-lang/McLTT/commits/base-mltt-v1.0