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
• wo...