Compile pipeline app

erasure/theories/EArities.v

@@ -1031,23 +1031,23 @@ Proof.
   exists Tty. split => //. eapply subject_reduction; tea.
 Qed.
 
-Lemma not_isErasable Σ Γ f A u : 
+Lemma not_isErasable Σ Γ f A u :
   wf_ext Σ -> wf_local Σ Γ ->
   ∥Σ;;; Γ |- f : A∥ ->
   (forall B, ∥Σ;;; Γ ⊢ A ⇝ B∥ -> A = B) ->
   (forall B, ∥Σ ;;; Γ |- f : B∥ -> ∥Σ ;;; Γ ⊢ A ≤ B∥) ->
   ~ ∥ isArity A ∥ ->
-  ∥ Σ;;; Γ |- A : tSort u ∥ -> 
+  ∥ Σ;;; Γ |- A : tSort u ∥ ->
   ~ is_propositional u ->
   ~ ∥ Extract.isErasable Σ Γ f ∥.
 Proof.
   intros wfΣ Hlocal Hf Hnf Hprinc Harity Hfu Hu  [[T [HT []]]]; sq.
-  - eapply Harity; sq. 
+  - eapply Harity; sq.
     eapply EArities.arity_type_inv in i as [T' [? ?]]; eauto.
     eapply Hnf in H. subst; eauto.
-  - destruct s as [s [? ?]]. eapply Hu. 
+  - destruct s as [s [? ?]]. eapply Hu.
     specialize (Hprinc _ (sq HT)).
-    pose proof (Hs := i). sq.  
+    pose proof (Hs := i). sq.
     eapply PCUICElimination.unique_sorting_equality_propositional in Hprinc; eauto.
-    rewrite Hprinc; eauto.   
-Qed. 
+    rewrite Hprinc; eauto.
+Qed.

erasure/theories/EAstUtils.v

@@ -18,6 +18,12 @@ Definition decompose_app f := decompose_app_rec f [].
 Definition head t := fst (decompose_app t).
 Definition spine t := snd (decompose_app t).
 
+Lemma decompose_app_head_spine t : decompose_app t = (head t, spine t).
+Proof.
+  unfold head, spine.
+  destruct decompose_app => //.
+Qed.
+
 Lemma decompose_app_rec_mkApps f l l' :
   decompose_app_rec (mkApps f l) l' = decompose_app_rec f (l ++ l').
 Proof.
@@ -31,7 +37,6 @@ Proof.
   destruct f; simpl in *; (discriminate || reflexivity).
 Qed.
 
-
 Lemma mkApps_app t l l' : mkApps t (l ++ l') = mkApps (mkApps t l) l'.
 Proof.
   induction l in t, l' |- *; simpl; auto.
@@ -156,6 +161,12 @@ Proof.
   intros napp. destruct t => //.
 Qed.
 
+Lemma head_mkApps_nApp f a : ~~ EAst.isApp f -> head (EAst.mkApps f a) = f.
+Proof.
+  rewrite head_mkApps /head => appf.
+  rewrite (decompose_app_mkApps f []) //.
+Qed.
+
 Lemma mkApps_eq_inj {t t' l l'} :
   mkApps t l = mkApps t' l' ->
   ~~ isApp t -> ~~ isApp t' -> t = t' /\ l = l'.

erasure/theories/EEnvMap.v

@@ -1,4 +1,4 @@
-From Coq Require Import ssreflect ssrbool Morphisms Setoid.
+From Coq Require Import ssreflect ssrbool Morphisms Setoid ProofIrrelevance.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Kernames EnvMap BasicAst.
@@ -173,6 +173,12 @@ Module GlobalContextMap.
     {| global_decls := g;
        map := EnvMap.of_global_env g |}.
 
+  Lemma make_irrel Σ fr fr' : EEnvMap.GlobalContextMap.make Σ fr = EEnvMap.GlobalContextMap.make Σ fr'.
+  Proof.
+    unfold make. f_equal.
+    apply proof_irrelevance.
+  Qed.
+
 End GlobalContextMap.
 
 Coercion GlobalContextMap.global_decls : GlobalContextMap.t >-> global_declarations.

erasure/theories/EEtaExpanded.v

@@ -670,6 +670,18 @@ Proof.
     eapply expanded_mkApps => //. now rewrite eqc. solve_all.
 Qed.
 
+Lemma isEtaExp_tApp_arg Σ t u : isEtaExp Σ (tApp t u) -> isEtaExp Σ u.
+Proof.
+  move/isEtaExp_tApp. destruct decompose_app eqn:da.
+  eapply decompose_app_inv in da. destruct l using rev_case.
+  - cbn in da. subst t0. cbn. now move/and3P => [].
+  - rewrite mkApps_app in da. noconf da.
+    destruct construct_viewc.
+    * intros [_ [_ [_ H]]]. move/andP: H => [] /andP[] _. rewrite forallb_app.
+      move=> /andP[] //=. now rewrite andb_true_r.
+    * now move/and4P => [].
+Qed.
+
 From MetaCoq.Erasure Require Import EEtaExpandedFix.
 
 Local Ltac simp_eta ::= simp isEtaExp; rewrite -?isEtaExp_equation_1 -?EEtaExpanded.isEtaExp_equation_1.

erasure/theories/EEtaExpandedFix.v

@@ -533,7 +533,7 @@ Section isEtaExp.
     funelim (isEtaExp Γ_ b); try simp_eta; eauto; try fold csubst;
       try toAll; try solve_all; subst.
     - intros. simp isEtaExp ; cbn. destruct (Nat.compare_spec #|Γ0| i) => //; simp_eta.
-      + rewrite nth_error_app2 in H0; try lia; cbn in H0; try easy. subst. rewrite minus_diag in H0. cbn in H0. easy.
+      + rewrite nth_error_app2 in H0; try lia; cbn in H0; try easy. subst. rewrite Nat.sub_diag in H0. cbn in H0. easy.
       + rewrite !nth_error_app2 in H0 |- *; cbn; try lia.
         erewrite option_default_ext; eauto. f_equal.
         destruct i; cbn; lia.
@@ -587,7 +587,7 @@ Section isEtaExp.
         rtoProp. repeat split; eauto.
         * unfold isEtaExp_fixapp. rewrite Hnth. len.
           subst. rewrite nth_error_app2 in H1; try lia.
-          rewrite minus_diag in H1. cbn in H1. eapply Nat.ltb_lt.
+          rewrite Nat.sub_diag in H1. cbn in H1. eapply Nat.ltb_lt.
           eapply Nat.leb_le in H1. lia.
         * cbn in Hcl. solve_all. rtoProp; intuition auto.
           now eapply expanded_weakening.
@@ -1942,3 +1942,19 @@ Proof.
   destruct (cst_body c); cbn in * => //.
   now eapply expanded_isEtaExp.
 Qed.
+
+Lemma isEtaExpFix_tApp_arg Σ Γ t u : isEtaExp Σ Γ (tApp t u) -> isEtaExp Σ Γ u.
+Proof.
+  move/isEtaExp_tApp'. destruct decompose_app eqn:da.
+  eapply decompose_app_inv in da. destruct l using rev_case.
+  - cbn in da. subst t0. cbn. now move/and3P => [].
+  - rewrite mkApps_app in da. noconf da.
+    destruct expanded_head_viewc.
+    * intros [_ [_ [_ H]]]. move/andP: H => [] /andP[] _. rewrite forallb_app.
+      move=> /andP[] //=. now rewrite andb_true_r.
+    * intros [_ [_ [_ H]]]. move/andP: H => [] /andP[] _ _. rewrite forallb_app.
+      move=> /andP[] //=. now rewrite andb_true_r.
+    * intros [_ [_ [_ H]]]. move/andP: H => [] _. rewrite forallb_app.
+      move=> /andP[] //=. now rewrite andb_true_r.
+    * now move/and4P => [].
+Qed.

erasure/theories/ERemoveParams.v

@@ -402,6 +402,14 @@ Proof.
   do 2 destruct nth_error => //.
 Qed.
 
+Lemma lookup_constructor_pars_args_strip (Σ : GlobalContextMap.t) i n npars nargs :
+  EGlobalEnv.lookup_constructor_pars_args Σ i n = Some (npars, nargs) ->
+  EGlobalEnv.lookup_constructor_pars_args (strip_env Σ) i n = Some (0, nargs).
+Proof.
+  rewrite /EGlobalEnv.lookup_constructor_pars_args. rewrite lookup_constructor_strip //=.
+  destruct EGlobalEnv.lookup_constructor => //. destruct p as [[] ?] => //=. now intros [= <- <-].
+Qed.
+
 Lemma is_propositional_strip (Σ : GlobalContextMap.t) ind :
   match inductive_isprop_and_pars Σ.(GlobalContextMap.global_decls) ind with
   | Some (prop, npars) =>

erasure/theories/EWcbvEval.v

@@ -1290,6 +1290,13 @@ Section Wcbv.
     now noconf H.
   Qed.
 
+  Lemma eval_value v v' :
+    value v -> eval v v' -> v = v'.
+  Proof.
+    intros isv ev.
+    now pose proof (eval_deterministic ev (value_final _ isv)).
+  Qed.
+
   Lemma eval_deterministic_all {t v v'} :
     All2 eval t v ->
     All2 eval t v' ->

erasure/theories/EWcbvEvalNamed.v

@@ -1,10 +1,14 @@
 (* Distributed under the terms of the MIT license. *)
 From Coq Require Import Utf8 Program.
-From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config BasicAst.
+From MetaCoq.Utils Require Import utils.
 From MetaCoq.PCUIC Require PCUICWcbvEval.
 From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst EReflect EGlobalEnv
   EWellformed EWcbvEval.
+From MetaCoq.Utils Require Import bytestring MCString.
+From MetaCoq.Erasure Require Import EWcbvEvalCstrsAsBlocksFixLambdaInd.
+From Coq Require Import BinaryString.
+Import String.
 
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -672,10 +676,6 @@ Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
 Local Hint Constructors represents : core.
 Local Hint Constructors represents_value : core.
 
-From MetaCoq.Utils Require Import bytestring MCString.
-Require Import BinaryString.
-Import String.
-
 Fixpoint gen_fresh_aux (na : ident) (Γ : list string) i :=
   match i with
   | 0 => na
@@ -1560,8 +1560,6 @@ Proof.
     + eapply All2_All2_Set, All2_app. eapply H1; eauto. econstructor; eauto.
 Qed.
 
-From MetaCoq Require Import EWcbvEvalCstrsAsBlocksFixLambdaInd.
-
 Lemma lookup_in_env Σ Σ' ind i :
   All2 (fun d d' => d.1 = d'.1 × match d.2 with ConstantDecl (Build_constant_body (Some body)) =>
     ∑ body', d'.2 = ConstantDecl (Build_constant_body (Some body')) × [] ;;; [] ⊩ body' ~ body

erasure/theories/ErasureFunctionProperties.v

@@ -8,7 +8,8 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive
   PCUICReduction PCUICReflect PCUICWeakeningEnv PCUICWeakeningEnvTyp PCUICCasesContexts
   PCUICWeakeningConv PCUICWeakeningTyp PCUICContextConversionTyp PCUICTyping PCUICGlobalEnv PCUICInversion PCUICGeneration
   PCUICConfluence PCUICConversion PCUICUnivSubstitutionTyp PCUICCumulativity PCUICSR PCUICSafeLemmata PCUICNormalization
-  PCUICValidity PCUICPrincipality PCUICElimination PCUICOnFreeVars PCUICWellScopedCumulativity PCUICSN PCUICEtaExpand.
+  PCUICValidity PCUICPrincipality PCUICElimination PCUICOnFreeVars PCUICWellScopedCumulativity PCUICSN PCUICEtaExpand
+  PCUICFirstorder.
 
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICSafeReduce PCUICSafeRetyping PCUICRetypingEnvIrrelevance.
 From MetaCoq.Erasure Require Import EAstUtils EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness ErasureFunction.
@@ -1984,9 +1985,10 @@ Proof.
     intros. sq. now rewrite (abstract_env_ext_irr _ H H2).
 Qed.
 
-From MetaCoq.PCUIC Require Import PCUICFirstorder.
+(*Inductive is_abstraction : EAst.term -> Prop :=
+  | is_lam na b : is_abstraction (EAst.tLambda na b)
+  | is_fix mfix idx : is_abstraction (EAst.tFix mfix idx). *)
 
-From Equations Require Import Equations.
 
 Inductive firstorder_evalue Σ : EAst.term -> Prop :=
   | is_fo i n args npars nargs :

erasure/theories/Extract.v

@@ -3,15 +3,59 @@ From Coq Require Import Program ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Primitive.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive PCUICTyping
-     PCUICElimination PCUICWcbvEval PCUICFirstorder.
+     PCUICElimination PCUICWcbvEval PCUICFirstorder
+     PCUICWellScopedCumulativity PCUICFirstorder PCUICNormalization PCUICReduction
+     PCUICConversion PCUICPrincipality PCUICNormal.
+
 From MetaCoq.Erasure Require EAst EGlobalEnv.
 
 Module E := EAst.
 
 Local Existing Instance extraction_checker_flags.
 
-Definition isErasable Σ Γ t := ∑ T, Σ ;;; Γ |- t : T × (isArity T + (∑ u, (Σ ;;; Γ |- T : tSort u) *
-  is_propositional u))%type.
+(* A term is erasable if it has _a_ type which either:
+  - is a syntactic arity
+  - is of propositional type *)
+Definition isErasable Σ Γ t :=
+  ∑ T, Σ ;;; Γ |- t : T ×
+  (isArity T + (∑ u, (Σ ;;; Γ |- T : tSort u) * is_propositional u))%type.
+
+(* A more positive notion of relevant terms.
+  Showing that a term is not erasable requires quantification over all its possible typings.
+  We give a more positive characterization of relevant terms. A term is not erasable if
+  it has _a_ type in normal form which is not an arity and whose sort is not propositional.
+*)
+Definition nisErasable Σ Γ t :=
+  ∑ T u,
+    [× Σ;;; Γ |- t : T,
+      nf Σ Γ T,
+    ~ isArity T,
+    Σ;;; Γ |- T : tSort u &
+    ~ is_propositional u].
+
+Lemma nisErasable_spec Σ Γ t :
+  wf_ext Σ -> wf_local Σ Γ ->
+  nisErasable Σ Γ t -> ~ ∥ isErasable Σ Γ t ∥.
+Proof.
+  intros wf wf' [T [u []]].
+  intros []. destruct X as [T' []].
+  destruct s.
+  * destruct (common_typing _ _ t0 t2) as (? & e & ? & ?).
+    eapply PCUICClassification.invert_cumul_arity_l_gen in e. destruct e as [s [[hr] ha]].
+    eapply (proj2 (nf_red _ _ _ _)) in n. 2:eapply hr. subst. contradiction.
+    eapply PCUICClassification.invert_cumul_arity_r_gen. 2:exact w.
+    exists T'. split; auto. sq.
+    eapply PCUICValidity.validity in t2 as [s Hs].
+    eapply PCUICClassification.wt_closed_red_refl; eauto.
+  * destruct (principal_type _ _ t0) as [princ hprinc].
+    destruct s as [u' [hs isp]].
+    pose proof (hprinc _ t2) as [].
+    destruct (PCUICValidity.validity t3).
+    eapply PCUICElimination.unique_sorting_equality_propositional in hs; tea; eauto.
+    pose proof (hprinc _ t0) as [].
+    eapply PCUICElimination.unique_sorting_equality_propositional in t1; tea; eauto.
+    congruence.
+Qed.
 
 Fixpoint mkAppBox c n :=
   match n with

erasure/theories/Typed/OptimizeCorrectness.v

@@ -24,6 +24,9 @@ Import ExAst.
 Import Kernames.
 Import ListNotations.
 
+Local Set Firstorder Solver auto.
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Lemma lookup_env_trans_env Σ kn :
   EGlobalEnv.lookup_env (trans_env Σ) kn =
   option_map trans_global_decl (lookup_env Σ kn).

pcuic/theories/PCUICEtaExpand.v

@@ -1368,3 +1368,9 @@ Proof.
   eapply IHX0_2. now eapply IHX0_1.
 Qed.
 
+Lemma expanded_tApp_arg Σ Γ t u : expanded Σ Γ (tApp t u) -> expanded Σ Γ u.
+Proof.
+  move/expanded_mkApps_inv' => [expa _].
+  move: expa; rewrite (arguments_mkApps t [u]).
+  move/Forall_app => [] _ hu; now depelim hu.
+Qed.