Merge pull request #1013 from MetaCoq/compile-pipeline-app

Compile pipeline app: applications of eta-expanded terms are preserved by the erasure pipeline.
This introduces a judgment for normal forms (and neutrals), and a proof that the PCUICExpandLets transformation preserves normal forms. Also introduces a more positive `nisErasable` notion that characterizes non-erasable/relevant terms.

Author: mattam82

erasure-plugin/theories/ErasureCorrectness.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/EArities.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/EAstUtils.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/EEnvMap.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/EEtaExpanded.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/EEtaExpandedFix.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/ERemoveParams.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/EWcbvEval.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/EWcbvEvalNamed.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 :