Assumptions file

Makefile

@@ -11,9 +11,12 @@ autosubst:
 	cd theories/autosubst ; \
 	$(MAKE) -f Makefile
 
+clean-assumptions: all
+	rm theories/Assumptions.vo
+
 force _CoqProject Makefile: ;
 
 %: Makefile.coq force
 	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean autosubst
+.PHONY: all clean clean-assumptions autosubst

README.md

@@ -66,8 +66,11 @@ The only part of the development which may use those axioms is the admissible
 rules and the GRTT to GTT translation which uses those rules. We also conjecture
 it could be done without, albeit with longer proofs.
 
-The suspicious reader may use `Print Assumptions` on our main theorems to verify
-that we do not require any hidden axioms.
+We provide a file `Assumptions.v` with reference to all lemmas of the
+submissions. It uses `Print Assumptions` on all of them which has the effect
+of printing the list of axioms used for each one.
+You may run `make clean-assumptions` and then `make` again if you wish to only
+check assumptions (after the project has been fully built).
 
 
 

_CoqProject

@@ -40,3 +40,5 @@ theories/ElimReflection.v
 
 theories/TransNat.v
 theories/TransVec.v
+
+theories/Assumptions.v

theories/Assumptions.v

@@ -0,0 +1,95 @@
+(** This file checks assumptions of all the lemmas of the submission **)
+
+From Coq Require Import Utf8 List Bool Lia.
+From Equations Require Import Equations.
+From GhostTT.autosubst Require Import CCAST GAST core unscoped.
+From GhostTT Require Import Util BasicAST SubstNotations ContextDecl
+  Scoping TermMode CastRemoval Typing BasicMetaTheory Admissible RTyping
+  Potential Model FreeTheorem ElimReflection.
+
+(* Lemma 2.1 *)
+Print Assumptions BasicMetaTheory.scoping_subst.
+
+(* Lemma 2.2 *)
+Print Assumptions BasicMetaTheory.scoping_castrm.
+
+(* Lemma 2.3 *)
+Print Assumptions BasicMetaTheory.castrm_subst.
+
+(* Lemma 2.4 *)
+Print Assumptions BasicMetaTheory.conv_md.
+
+(* Lemma 2.5 *)
+Print Assumptions BasicMetaTheory.typing_subst.
+
+(* Lemma 2.6 *)
+Print Assumptions BasicMetaTheory.validity.
+
+(* Lemma 3.1 *)
+Print Assumptions Erasure.erase_subst.
+
+(* Lemma 3.2 *)
+Print Assumptions Erasure.erase_castrm.
+
+(* Lemma 3.3 *)
+Print Assumptions Erasure.erase_typing.
+Print Assumptions Erasure.erase_conv.
+Print Assumptions Erasure.erase_context.
+
+(* Lemma 3.4 *)
+Print Assumptions Revival.type_to_rev.
+
+(* Lemma 3.5 *)
+Print Assumptions Revival.revive_subst.
+
+(* Lemma 3.6 *)
+Print Assumptions Revival.revive_castrm.
+
+(* Lemma 3.7 *)
+Print Assumptions Revival.revive_typing.
+Print Assumptions Revival.revive_conv.
+Print Assumptions Revival.revive_context.
+
+(* Lemma 3.8 *)
+Print Assumptions Param.typing_rev_sub_param.
+Print Assumptions Param.typing_er_sub_param.
+
+(* Lemma 3.9 *)
+Print Assumptions Param.param_subst.
+
+(* Lemma 3.10 *)
+Print Assumptions Param.param_scoping.
+
+(* Lemma 3.11 *)
+Print Assumptions Param.param_castrm.
+
+(* Lemma 3.12 *)
+Print Assumptions Param.param_typing.
+Print Assumptions Param.param_conv.
+Print Assumptions Param.param_context.
+
+(* Theorem 4.1 *)
+Print Assumptions Model.relative_consistency.
+
+(* Lemma 4.4 *)
+Print Assumptions Model.mode_coherence.
+
+(* Free theorem *)
+Print Assumptions FreeTheorem.constant_free_theorem.
+
+(* Lemma 6.1 *)
+Print Assumptions Potential.tr_choice.
+
+(* Lemma 6.2 *)
+Print Assumptions Potential.tr_sort_eq.
+Print Assumptions Potential.tr_bot_eq.
+
+(* Theorem 6.3 *)
+Print Assumptions ElimReflection.elim_reflection.
+Print Assumptions ElimReflection.elim_ctx.
+
+(* Theorem 6.4 *)
+Print Assumptions ElimReflection.conservativity.
+
+(* Theorem 6.5 *)
+Print Assumptions ElimReflection.consistency.