Cleanup ErasureCorrectness

Author: mattam82

erasure-plugin/theories/ErasureCorrectness.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

@@ -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

@@ -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/Extract.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).

erasure/theories/Typed/OptimizeCorrectness.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.