Merge pull request #533 from MetaCoq/template-pcuic-proofs

Template <-> PCUIC proofs

Author: mattam82

INSTALL.md

@@ -25,7 +25,6 @@ MetaCoq is split into multiple packages that get all installed using the
 `coq-metacoq` meta-package:
 
  - `coq-metacoq-template` for the Template Monad and quoting plugin
- - `coq-metacoq-checker` for the UNverified checker of template-coq terms
  - `coq-metacoq-pcuic` for the PCUIC development and proof of the
    Template-Coq -> PCUIC translation
  - `coq-metacoq-safechecker` for the verified checker on PCUIC terms
@@ -103,7 +102,7 @@ the sources directory.
 
 Then use:
 
-- `make` to compile the `template-coq` plugin, the `checker`, the `pcuic`
+- `make` to compile the `template-coq` plugin, the `pcuic`
   development and the `safechecker` and `erasure` plugins.
   You can also selectively build each target.
 

Makefile

@@ -1,20 +1,18 @@
 TIMED ?=
 
-all: template-coq checker pcuic safechecker erasure examples
+all: template-coq pcuic safechecker erasure examples
 
-.PHONY: all template-coq checker pcuic erasure install html clean mrproper .merlin test-suite translations
+.PHONY: all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
 
 install: all
 	$(MAKE) -C template-coq install
-	$(MAKE) -C checker install
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
 	$(MAKE) -C erasure install
 	$(MAKE) -C translations install
 
 uninstall: all
 	$(MAKE) -C template-coq uninstall
-	$(MAKE) -C checker uninstall
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
 	$(MAKE) -C erasure uninstall
@@ -23,7 +21,6 @@ uninstall: all
 html: all
 	"coqdoc" -toc -utf8 -interpolate -l -html \
 		-R template-coq/theories MetaCoq.Template \
-		-R checker/theories MetaCoq.Checker \
 		-R pcuic/theories MetaCoq.PCUIC \
 		-R safechecker/theories MetaCoq.SafeChecker \
 		-R erasure/theories MetaCoq.Erasure \
@@ -32,7 +29,6 @@ html: all
 
 clean:
 	$(MAKE) -C template-coq clean
-	$(MAKE) -C checker clean
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C erasure clean
@@ -45,7 +41,6 @@ mrproper:
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C erasure mrproper
-	$(MAKE) -C checker mrproper
 	$(MAKE) -C examples mrproper
 	$(MAKE) -C test-suite mrproper
 	$(MAKE) -C translations mrproper
@@ -55,7 +50,6 @@ mrproper:
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C erasure .merlin
-	$(MAKE) -C checker .merlin
 
 template-coq:
 	$(MAKE) -C template-coq
@@ -69,22 +63,17 @@ safechecker: template-coq pcuic
 erasure: template-coq safechecker pcuic
 	$(MAKE) -C erasure
 
-checker: template-coq
-	$(MAKE) -C checker
-
 examples: checker safechecker erasure
 	$(MAKE) -C examples
 
-test-suite: template-coq checker safechecker erasure
+test-suite: template-coq safechecker erasure
 	$(MAKE) -C test-suite
 
-translations: template-coq checker
+translations: template-coq
 	$(MAKE) -C translations
 
 cleanplugins:
 	$(MAKE) -C template-coq cleanplugin
-	$(MAKE) -C pcuic cleanplugin
-	$(MAKE) -C checker cleanplugin
 	$(MAKE) -C safechecker cleanplugin
 	$(MAKE) -C erasure cleanplugin
 

README.md

@@ -69,21 +69,13 @@ In addition to this representation of terms, Template Coq includes:
   checker, and inserting them in the global environment, in
   the style of MTac.
 
-
-### [Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.11/checker)
-
-A partial type-checker for the Calculus of Inductive Constructions,
-whose extraction to ML is runnable as a plugin (using command `MetaCoq
-Check foo`). This checker uses _fuel_, so it must be passed a number
-of maximal reduction steps to perform when calling conversion, and is
-NOT verified.
-
+- A formalisation of the expected typing rules reflecting the ones of Coq
 
 ### [PCUIC](https://github.com/MetaCoq/metacoq/tree/coq-8.11/pcuic)
 
 PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is
 a cleaned up version of the term language of Coq and its associated
-type system, equivalent to the one of Coq. This version of the
+type system, shown equivalent to the one of Coq. This version of the
 calculus has proofs of standard metatheoretical results:
 
 - Weakening for global declarations, weakening and substitution for

TODO.md

@@ -33,6 +33,12 @@
 
 - Finish the PCUICSigmaCalculus proofs.
 
+# Medium Projects
+
+- Change Template-PCUIC translations to translate casts to applications of 
+  identity functions (vm_cast, default_cast etc) to make the back and forth
+  the identity and derive weakening/substitution/etc.. from the PCUIC theorems.
+  Is that really better than identity functions?
 # Big projects
 
 - Refine the longest-simple-path algorithm on universes with the 
@@ -48,6 +54,9 @@
   be definable. Probably not very useful though because if the elimination is 
   restricted then it means some Type is in the constructor and won't be projectable.
 
+- Verify the substitution calculus of P.M Pédrot using skewed lists at
+  https://github.com/coq/coq/pull/13537 and try to use it to implement efficient explicit 
+  substitutions.
 
 ## Website