Definition of weak-head-reduction and proof of unicity of derivations

.gitignore

@@ -418,3 +418,6 @@ erasure/src/pCUICTypeChecker.ml
 erasure/src/pCUICTypeChecker.mli
 erasure/src/pCUICPrimitive.ml
 erasure/src/pCUICPrimitive.mli
+erasure/src/pCUICCases.ml
+erasure/src/pCUICCases.mli
+template-coq/gen-src/specFloat.ml.rej

.vscode/tasks.json

@@ -7,10 +7,20 @@
             "label": "make",
             "type": "shell",
             "command": "make",
+            "problemMatcher": []
+        },
+        {
+            "label": "makevos",
+            "type": "shell",
+            "options": {
+              "cwd" : "pcuic",
+            },
+            "command": "opam exec -- make -f Makefile.pcuic vos",
             "group": {
                 "kind": "build",
                 "isDefault": true
-            }
+            },
+            "problemMatcher": []
         }
     ]
 }

DOC.md

@@ -63,7 +63,17 @@ Quoting always produce fully qualified names. On the converse, unquoting allow t
 have only partially qualified names and rely on Coq to resolve them. The commands
 of the TemplateMonad also allow partially qualified names.
 
+## Hint databases
 
+The development uses three main hint databases:
+
+- The "len" databases which gathers all relevant length lemmas (mainly list length lemmas 
+  relevant to the operations). This database is large (> 100 lemmas) for a given theory
+  (PCUIC or Template-Coq) and it is advisable to not mix together both databases,
+  as autorewrite would become very slow.
+  BEWARE: If working in the PCUIC theory, do not require anything besides the BasicAst and utils modules from the Template-Coq module. 
+- The "pcuic" rewrite and auto database gathers lemmas helping solving side-conditions 
+  of typing judgements. 
 
 ## Options
 

TODO.md

@@ -38,9 +38,20 @@
 - 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?
+  Template -> PCUIC -> Template (in an environment extended with the identity functions)
+  becomes the identity, by translating back the cast function applications.
+  PCUIC -> Template -> PCUIC is also the identity, even by special casing on cast functions
+
 # Big projects
 
+- Cleaner version of the system for writing term manipulation and prooofs about them. 
+  - Develop a cleaned-up syntax profiting from Coq's type system, e.g.:
+    - HOAS representation of binding or first-order well-scoped binding representation (using `fin` for example)
+    - Well-bounded global references?
+    - Using vectors and fin for fixpoint bodies lists and index (no ill-formed
+    fixpoints by construction)
+  - Develop a proof mode for MetaCoq typing, à la Iris proof mode 
+
 - Refine the longest-simple-path algorithm on universes with the 
   Bender & al algorithm used in Coq, extended with edges of negative weight.
   Alternatively prove the spec for that algorithm. Refinement might be easier:
@@ -49,14 +60,13 @@
 
 - Verify parsing and printing of terms / votour
 
-- Primivite projections: we could be more relaxed on the elimination sort of the 
+- Primitive projections: we could be more relaxed on the elimination sort of the 
   inductive. If it is e.g. InProp, then all projections to types in Prop should
   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.
+  https://github.com/coq/coq/pull/13537 and try to use it to implement efficient explicit substitutions.
 
 ## Website
 

erasure/_PluginProject.in

@@ -2,8 +2,6 @@
 -Q src MetaCoq.Erasure
 -R theories MetaCoq.Erasure
 
-src/init.mli
-src/init.ml
 # src/classes0.mli
 # src/classes0.ml
 
@@ -17,8 +15,6 @@ src/orderedTypeAlt.ml
 
 src/ssrbool.ml
 src/ssrbool.mli
-src/monad_utils.ml
-src/monad_utils.mli
 src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml
@@ -35,20 +31,16 @@ src/pCUICPrimitive.mli
 src/pCUICPrimitive.ml
 src/pCUICAst.ml
 src/pCUICAst.mli
+src/pCUICCases.mli
+src/pCUICCases.ml
 src/pCUICAstUtils.ml
 src/pCUICAstUtils.mli
-src/pCUICLiftSubst.ml
-src/pCUICLiftSubst.mli
 # src/eqDecInstances.ml
 # src/eqDecInstances.mli
 src/pCUICReduction.ml
 src/pCUICReduction.mli
 src/pCUICTyping.ml
 src/pCUICTyping.mli
-src/pCUICUnivSubst.ml
-src/pCUICUnivSubst.mli
-# src/pCUICCumulativity.mli
-# src/pCUICCumulativity.ml
 src/pCUICPosition.mli
 src/pCUICPosition.ml
 src/pCUICNormal.mli

erasure/src/metacoq_erasure_plugin.mlpack

@@ -1,4 +1,3 @@
-Monad_utils
 MSetWeakList
 EqdepFacts
 Ssrbool
@@ -9,16 +8,14 @@ UGraph0
 OrderedTypeAlt
 Kernames
 
-Init
 Classes0
 Logic1
 Relation
 Relation_Properties
 PCUICPrimitive
 PCUICAst
+PCUICCases
 PCUICAstUtils
-PCUICUnivSubst
-PCUICLiftSubst
 EqDecInstances
 PCUICEquality
 PCUICTyping

erasure/theories/EArities.v

@@ -40,7 +40,7 @@ Qed.
 
 Lemma isArity_ind_type (Σ : global_env_ext) mind ind idecl :
   wf Σ ->
-  declared_inductive (fst Σ) mind ind idecl ->
+  declared_inductive (fst Σ) ind mind idecl ->
   isArity (ind_type idecl).
 Proof.
   intros. 
@@ -92,21 +92,21 @@ Proof.
 Qed.
 
 Lemma typing_spine_red :
-  forall (Σ : PCUICAst.global_env_ext) Γ (args args' : list PCUICAst.term) (X : All2 (red Σ Γ) args args') (bla : wf Σ)
+  forall (Σ : global_env_ext) Γ (args args' : list PCUICAst.term) (X : All2 (red Σ Γ) args args') (bla : wf Σ)
     (T x x0 : PCUICAst.term) (t0 : typing_spine Σ Γ x args x0) (c : Σ;;; Γ |- x0 <= T) (x1 : PCUICAst.term)
     (c0 : Σ;;; Γ |- x1 <= x), isType Σ Γ T -> typing_spine Σ Γ x1 args' T.
 Proof.
   intros Σ Γ args args' X wf T x x0 t0 c x1 c0 ?. revert args' X.
   dependent induction t0; intros.
-  - inv X. econstructor. eauto. eapply PCUICConversion.cumul_trans. assumption.
-    eauto. eapply PCUICConversion.cumul_trans. assumption. eauto. eauto.
+  - inv X. econstructor. eauto. eapply cumul_trans. assumption.
+    eauto. eapply cumul_trans. assumption. eauto. eauto.
   - inv X. econstructor.
     + eauto.
-    + eapply PCUICConversion.cumul_trans ; eauto.
+    + eapply cumul_trans ; eauto.
     + eapply subject_reduction; eauto.
     + eapply IHt0; eauto.
       eapply PCUICCumulativity.red_cumul_inv.
-      unfold PCUICLiftSubst.subst1.
+      unfold subst1.
       eapply (red_red Σ Γ [_] [] [_] [_]).
       eauto. econstructor. eauto. econstructor. econstructor. econstructor.
       Grab Existential Variables. all: repeat econstructor.
@@ -199,9 +199,8 @@ Proof.
     revert c0 t0 i. generalize x at 1 3.
     intros x2 c0 t0 i.
     assert (HWF : isType Σ Γ x2).
-    { eapply PCUICValidity.validity.
-      - eauto.
-      - eapply type_mkApps. 2:eauto. eauto.
+    { eapply PCUICValidity.validity; tea.
+      eapply type_mkApps. 2:eauto. eauto.
     }
     eapply inversion_Construct in t as (? & ? & ? & ? & ? & ? & ?) ; auto. (* destruct x5. destruct p. cbn in *. *)
     assert (HL : #|ind_bodies x3| > 0).
@@ -212,24 +211,24 @@ Proof.
     (* eapply isArity_typing_spine_inv in t0; eauto. *)
     (* destruct t0 as (? & [] & ?). *)
     (* eapply PCUICCumulativity.red_cumul in X. *)
-    destruct (PCUICWeakeningEnv.on_declared_constructor _ d) as [XX [s [XX1 Ht]]].
-    destruct x5 as [[? ?] ?]; cbn in *; subst.
-    destruct Ht. unfold cdecl_type in cstr_eq. simpl in cstr_eq. subst.
+    destruct (PCUICWeakeningEnv.on_declared_constructor d) as [XX [s [XX1 Ht]]].
+    destruct x5 as []; cbn in *; subst.
+    destruct Ht; cbn in *. subst.
     change PCUICEnvironment.it_mkProd_or_LetIn with it_mkProd_or_LetIn in c2.
     change PCUICEnvironment.ind_params with ind_params in *.
     change PCUICEnvironment.to_extended_list_k with to_extended_list_k in *.
     rewrite <- it_mkProd_or_LetIn_app in c2.
-    rewrite PCUICUnivSubst.subst_instance_constr_it_mkProd_or_LetIn in c2.
-    rewrite PCUICUnivSubst.subst_instance_constr_mkApps in c2.
-    rewrite PCUICSubstitution.subst_it_mkProd_or_LetIn in c2.
+    rewrite PCUICUnivSubst.subst_instance_it_mkProd_or_LetIn in c2.
+    rewrite PCUICUnivSubst.subst_instance_mkApps in c2.
+    rewrite subst_it_mkProd_or_LetIn in c2.
     rewrite subst_mkApps in c2.
     cbn in c2.
-    rewrite PCUICUnivSubst.subst_instance_context_length in c2.
+    rewrite subst_instance_length in c2.
     rewrite app_length in c2.
-    destruct (Nat.leb_spec (#|cshape_args s| + #|ind_params x3| + 0) (#|ind_bodies x3| - S (inductive_ind ind) + #|ind_params x3| + #|cshape_args s|)). 2:lia.
+    destruct (Nat.leb_spec (#|cstr_args0| + #|ind_params x3| + 0) (#|ind_bodies x3| - S (inductive_ind ind) + #|ind_params x3| + #|cstr_args0|)). 2:lia.
     clear H.
     assert ((#|ind_bodies x3| - S (inductive_ind ind) + #|ind_params x3| +
-                                                                         #|cshape_args s| - (#|cshape_args s| + #|ind_params x3| + 0)) < #|inds (inductive_mind ind) u (ind_bodies x3)|).
+    #|cstr_args0| - (#|cstr_args0| + #|ind_params x3| + 0)) < #|inds (inductive_mind ind) u (ind_bodies x3)|).
     { rewrite inds_length. lia. }
     eapply nth_error_Some in H.
     destruct (nth_error (inds _ _ _) _) eqn:Heq; try congruence.
@@ -291,8 +290,7 @@ Proof.
     intros x2 c0 t0 i.
     assert (HWF : isType Σ Γ x2).
     { eapply PCUICValidity.validity.
-      - eauto.
-      - eapply type_mkApps. 2:eauto. eauto.
+      eapply type_mkApps. 2:eauto. eauto.
     }
     eapply inversion_CoFix in t as (? & ? & ? & ? & ? & ? & ?) ; auto.
     eapply invert_cumul_arity_r in c0; eauto.
@@ -304,10 +302,10 @@ Proof.
     eapply invert_cumul_arity_r_gen in c0; eauto.
     destruct c0. destruct H as [[r] isA].
     move: r; rewrite subst_it_mkProd_or_LetIn eqT; autorewrite with len.
-    rewrite expand_lets_mkApps subst_mkApps /=.
+    rewrite PCUICSigmaCalculus.expand_lets_mkApps subst_mkApps /=.
     move/red_it_mkProd_or_LetIn_mkApps_Ind => [ctx' [args' eq]].
     subst x4. now eapply it_mkProd_arity, isArity_mkApps in isA.
-    move: cum => [] Hx1; rewrite eqT expand_lets_mkApps subst_mkApps /= => cum.
+    move: cum => [] Hx1; rewrite eqT PCUICSigmaCalculus.expand_lets_mkApps subst_mkApps /= => cum.
     eapply invert_cumul_arity_r_gen in c0; eauto.
     destruct c0 as [? [[r] isA]].
     eapply red_mkApps_tInd in r as [args' [eq _]]; auto.
@@ -445,7 +443,7 @@ Proof.
     eapply PCUICCumulativity.red_cumul_inv in X.
 
     eapply invert_cumul_arity_l in H0 as (? & ? & ?).
-    2: eapply PCUICConversion.cumul_trans; eauto.
+    2: eapply cumul_trans; eauto.
     destruct H.
     eapply typing_spine_red in t1. 2:{ eapply All_All2_refl.
                                                   clear. induction L; eauto. }
@@ -592,7 +590,7 @@ Lemma nIs_conv_to_Arity_isWfArity_elim {Σ : global_env_ext} {Γ x} :
 Proof.
   intros nis [isTy [ctx [s da]]]. apply nis.
   red. exists (it_mkProd_or_LetIn ctx (tSort s)).
-  split. sq. apply PCUICArities.destArity_spec_Some in da.
+  split. sq. apply destArity_spec_Some in da.
   simpl in da. subst x.
   reflexivity.
   now eapply it_mkProd_isArity.