Library MetaCoq.Erasure.EInlineProjections
From Coq Require Import Utf8 Program.
From MetaCoq.Template Require Import config utils Kernames BasicAst.
From MetaCoq.Erasure Require Import EAst EAstUtils EExtends
ELiftSubst ECSubst EGlobalEnv EWellformed EWcbvEval Extract
EEnvMap EArities EProgram.
Local Open Scope string_scope.
Set Asymmetric Patterns.
Import MCMonadNotation.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Require Import ssreflect ssrbool.
From MetaCoq.Template Require Import config utils Kernames BasicAst.
From MetaCoq.Erasure Require Import EAst EAstUtils EExtends
ELiftSubst ECSubst EGlobalEnv EWellformed EWcbvEval Extract
EEnvMap EArities EProgram.
Local Open Scope string_scope.
Set Asymmetric Patterns.
Import MCMonadNotation.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Require Import ssreflect ssrbool.
We assumes Prop </= Type and universes are checked correctly in the following.
Local Existing Instance extraction_checker_flags.
Ltac introdep := let H := fresh in intros H; depelim H.
#[global]
Hint Constructors eval : core.
Ltac introdep := let H := fresh in intros H; depelim H.
#[global]
Hint Constructors eval : core.
Allow everything in terms
Definition switch_no_params (efl : EEnvFlags) :=
{| has_axioms := has_axioms;
has_cstr_params := false;
term_switches := term_switches ;
cstr_as_blocks := false
|}.
Definition flags_after_projs := (switch_no_params all_env_flags).
Local Existing Instance flags_after_projs.
Arguments lookup_projection : simpl never.
Arguments GlobalContextMap.lookup_projection : simpl never.
Lemma lookup_inductive_wellformed {efl : EEnvFlags} Σ (kn : kername)
(decl : mutual_inductive_body) :
wf_glob Σ → lookup_minductive Σ kn = Some decl → wf_minductive decl.
Proof.
intros wfΣ.
rewrite /lookup_minductive.
destruct lookup_env as [[]|] eqn:hl ⇒ //=.
intros [= <-]. now eapply lookup_env_wellformed in hl.
Qed.
Lemma wellformed_projection_args {efl : EEnvFlags} {Σ p mdecl idecl cdecl pdecl} :
wf_glob Σ →
lookup_projection Σ p = Some (mdecl, idecl, cdecl, pdecl) →
p.(proj_arg) < cdecl.(cstr_nargs).
Proof.
intros wfΣ.
rewrite /lookup_projection /lookup_constructor /lookup_inductive.
destruct lookup_minductive eqn:hl ⇒ //=.
eapply lookup_inductive_wellformed in hl; eauto.
move: hl. unfold wf_minductive.
destruct nth_error eqn:hnth ⇒ //.
destruct ind_ctors as [|? []] eqn:hnth' ⇒ //.
destruct (nth_error (ind_projs _) _) eqn:hnth'' ⇒ //.
intros wf [= <- <- <- <-].
move: wf ⇒ /andP[] _.
move/(nth_error_forallb hnth). rewrite /wf_inductive /wf_projections.
destruct ind_projs ⇒ //. now rewrite nth_error_nil in hnth''.
rewrite hnth'. cbn. move/(@eqb_eq nat). intros <-.
eapply nth_error_Some_length in hnth''. now cbn in hnth''.
destruct (nth_error (ind_projs _) _) eqn:hnth'' ⇒ //.
move⇒ /andP[] _.
move/(nth_error_forallb hnth). rewrite /wf_inductive /wf_projections.
destruct ind_projs ⇒ //. now rewrite nth_error_nil in hnth''.
rewrite hnth' //.
Qed.
Section optimize.
Context (Σ : GlobalContextMap.t).
Fixpoint optimize (t : term) : term :=
match t with
| tRel i ⇒ tRel i
| tEvar ev args ⇒ tEvar ev (List.map optimize args)
| tLambda na M ⇒ tLambda na (optimize M)
| tApp u v ⇒ tApp (optimize u) (optimize v)
| tLetIn na b b' ⇒ tLetIn na (optimize b) (optimize b')
| tCase ind c brs ⇒ tCase ind (optimize c) (map (on_snd optimize) brs)
| tProj p c ⇒
match GlobalContextMap.lookup_projection Σ p with
| Some (mdecl, idecl, cdecl, pdecl) ⇒
tCase (p.(proj_ind), p.(proj_npars)) (optimize c) [(unfold cdecl.(cstr_nargs) (fun n ⇒ nAnon), tRel (cdecl.(cstr_nargs) - S p.(proj_arg)))]
| _ ⇒ tProj p (optimize c)
end
| tFix mfix idx ⇒
let mfix' := List.map (map_def optimize) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def optimize) mfix in
tCoFix mfix' idx
| tBox ⇒ t
| tVar _ ⇒ t
| tConst _ ⇒ t
| tConstruct ind n args ⇒ tConstruct ind n (map optimize args)
end.
Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l).
Proof using Type.
induction l using rev_ind; simpl; auto.
now rewrite mkApps_app /= IHl map_app /= mkApps_app /=.
Qed.
Lemma map_optimize_repeat_box n : map optimize (repeat tBox n) = repeat tBox n.
Proof using Type. by rewrite map_repeat. Qed.
Lemma wf_optimize t k :
wf_glob Σ →
wellformed Σ k t → wellformed Σ k (optimize t).
Proof using Type.
intros wfΣ.
induction t in k |- × using EInduction.term_forall_list_ind; simpl; auto;
intros; try easy;
rewrite → ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
unfold wf_fix_gen, test_def in *;
simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
- rtoProp. split; eauto. destruct args; eauto.
- move/andP: H ⇒ [] /andP[] → clt cll /=.
rewrite IHt //=. solve_all.
- rewrite GlobalContextMap.lookup_projection_spec.
destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl; auto ⇒ //.
simpl.
have arglen := wellformed_projection_args wfΣ hl.
apply lookup_projection_lookup_constructor, lookup_constructor_lookup_inductive in hl.
rewrite hl /= andb_true_r.
rewrite IHt //=; len. apply Nat.ltb_lt.
lia.
- len. rtoProp; solve_all. rewrite forallb_map; solve_all.
- len. rtoProp; solve_all. rewrite forallb_map; solve_all.
Qed.
Lemma optimize_csubst {a k b} n :
wf_glob Σ →
wellformed Σ (k + n) b →
optimize (ECSubst.csubst a k b) = ECSubst.csubst (optimize a) k (optimize b).
Proof using Type.
intros wfΣ.
induction b in k |- × using EInduction.term_forall_list_ind; simpl; auto;
intros wft; try easy;
rewrite → ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
unfold wf_fix, test_def in *;
simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
- destruct (k ?= n0)%nat; auto.
- f_equal. rtoProp. now destruct args; inv H0.
- move/andP: wft ⇒ [] /andP[] hi hb hl. rewrite IHb. f_equal. unfold on_snd; solve_all.
repeat toAll. f_equal. solve_all. unfold on_snd; cbn. f_equal.
rewrite a0 //. now rewrite -Nat.add_assoc.
- move/andP: wft ⇒ [] hp hb.
rewrite GlobalContextMap.lookup_projection_spec.
destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl ⇒ /= //.
f_equal; eauto. f_equal. len. f_equal.
have arglen := wellformed_projection_args wfΣ hl.
case: Nat.compare_spec. lia. lia.
auto.
- f_equal. move/andP: wft ⇒ [hidx hb].
solve_all. unfold map_def. f_equal.
eapply a0. now rewrite -Nat.add_assoc.
- f_equal. move/andP: wft ⇒ [hidx hb].
solve_all. unfold map_def. f_equal.
eapply a0. now rewrite -Nat.add_assoc.
Qed.
Lemma optimize_substl s t :
wf_glob Σ →
forallb (wellformed Σ 0) s →
wellformed Σ #|s| t →
optimize (substl s t) = substl (map optimize s) (optimize t).
Proof using Type.
intros wfΣ. induction s in t |- *; simpl; auto.
move/andP ⇒ [] cla cls wft.
rewrite IHs //. eapply wellformed_csubst ⇒ //.
f_equal. rewrite (optimize_csubst (S #|s|)) //.
Qed.
Lemma optimize_iota_red pars args br :
wf_glob Σ →
forallb (wellformed Σ 0) args →
wellformed Σ #|skipn pars args| br.2 →
optimize (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map optimize args) (on_snd optimize br).
Proof using Type.
intros wfΣ wfa wfbr.
unfold EGlobalEnv.iota_red.
rewrite optimize_substl //.
rewrite forallb_rev forallb_skipn //.
now rewrite List.rev_length.
now rewrite map_rev map_skipn.
Qed.
Lemma optimize_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.fix_subst mfix).
Proof using Type.
unfold EGlobalEnv.fix_subst.
rewrite map_length.
generalize #|mfix|.
induction n; simpl; auto.
f_equal; auto.
Qed.
Lemma optimize_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.cofix_subst mfix).
Proof using Type.
unfold EGlobalEnv.cofix_subst.
rewrite map_length.
generalize #|mfix|.
induction n; simpl; auto.
f_equal; auto.
Qed.
Lemma optimize_cunfold_fix mfix idx n f :
wf_glob Σ →
wellformed Σ 0 (tFix mfix idx) →
cunfold_fix mfix idx = Some (n, f) →
cunfold_fix (map (map_def optimize) mfix) idx = Some (n, optimize f).
Proof using Type.
intros wfΣ hfix.
unfold cunfold_fix.
rewrite nth_error_map.
cbn in hfix. move/andP: hfix ⇒ [] hidx hfix.
destruct nth_error eqn:hnth ⇒ //.
intros [= <- <-] ⇒ /=. f_equal.
rewrite optimize_substl //. eapply wellformed_fix_subst ⇒ //.
rewrite fix_subst_length.
eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix.
now rewrite optimize_fix_subst.
Qed.
Lemma optimize_cunfold_cofix mfix idx n f :
wf_glob Σ →
wellformed Σ 0 (tCoFix mfix idx) →
cunfold_cofix mfix idx = Some (n, f) →
cunfold_cofix (map (map_def optimize) mfix) idx = Some (n, optimize f).
Proof using Type.
intros wfΣ hfix.
unfold cunfold_cofix.
rewrite nth_error_map.
cbn in hfix. move/andP: hfix ⇒ [] hidx hfix.
destruct nth_error eqn:hnth ⇒ //.
intros [= <- <-] ⇒ /=. f_equal.
rewrite optimize_substl //. eapply wellformed_cofix_subst ⇒ //.
rewrite cofix_subst_length.
eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix.
now rewrite optimize_cofix_subst.
Qed.
End optimize.
Definition optimize_constant_decl Σ cb :=
{| cst_body := option_map (optimize Σ) cb.(cst_body) |}.
Definition optimize_decl Σ d :=
match d with
| ConstantDecl cb ⇒ ConstantDecl (optimize_constant_decl Σ cb)
| InductiveDecl idecl ⇒ d
end.
Definition optimize_env Σ :=
map (on_snd (optimize_decl Σ)) Σ.(GlobalContextMap.global_decls).
Import EnvMap.
Program Fixpoint optimize_env' Σ : EnvMap.fresh_globals Σ → global_context :=
match Σ with
| [] ⇒ fun _ ⇒ []
| hd :: tl ⇒ fun HΣ ⇒
let Σg := GlobalContextMap.make tl (fresh_globals_cons_inv HΣ) in
on_snd (optimize_decl Σg) hd :: optimize_env' tl (fresh_globals_cons_inv HΣ)
end.
Import EGlobalEnv EExtends.
Lemma extends_lookup_projection {efl : EEnvFlags} {Σ Σ' p} : extends Σ Σ' → wf_glob Σ' →
isSome (lookup_projection Σ p) →
lookup_projection Σ p = lookup_projection Σ' p.
Proof.
intros ext wf; cbn.
unfold lookup_projection.
destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl ⇒ //.
simpl.
rewrite (extends_lookup_constructor wf ext _ _ _ hl) //.
Qed.
Lemma wellformed_optimize_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
∀ n, EWellformed.wellformed Σ n t →
∀ {Σ' : GlobalContextMap.t}, extends Σ Σ' → wf_glob Σ' →
optimize Σ t = optimize Σ' t.
Proof.
induction t using EInduction.term_forall_list_ind; cbn -[lookup_constant lookup_inductive
GlobalContextMap.lookup_projection]; intros ⇒ //.
all:unfold wf_fix_gen in *; rtoProp; intuition auto.
5:{ destruct cstr_as_blocks; rtoProp. f_equal; eauto; solve_all. destruct args; cbn in *; eauto. }
all:f_equal; eauto; solve_all.
- rewrite !GlobalContextMap.lookup_projection_spec.
rewrite -(extends_lookup_projection H0 H1 H3).
destruct lookup_projection as [[[[]]]|]. f_equal; eauto.
now cbn in H3.
Qed.
Lemma wellformed_optimize_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
wf_global_decl Σ t →
∀ {Σ' : GlobalContextMap.t}, extends Σ Σ' → wf_glob Σ' →
optimize_decl Σ t = optimize_decl Σ' t.
Proof.
destruct t ⇒ /= //.
intros wf Σ' ext wf'. f_equal. unfold optimize_constant_decl. f_equal.
destruct (cst_body c) ⇒ /= //. f_equal.
now eapply wellformed_optimize_extends.
Qed.
Lemma lookup_env_optimize_env_Some {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn d :
wf_glob Σ →
GlobalContextMap.lookup_env Σ kn = Some d →
∑ Σ' : GlobalContextMap.t,
[× extends Σ' Σ, wf_global_decl Σ' d &
lookup_env (optimize_env Σ) kn = Some (optimize_decl Σ' d)].
Proof.
rewrite GlobalContextMap.lookup_env_spec.
destruct Σ as [Σ map repr wf].
induction Σ in map, repr, wf |- *; simpl; auto ⇒ //.
intros wfg.
case: eqb_specT ⇒ //.
- intros →. cbn. intros [= <-].
∃ (GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). split.
now eexists [_].
cbn. now depelim wfg.
f_equal. symmetry. eapply wellformed_optimize_decl_extends. cbn. now depelim wfg.
cbn. now ∃ [a]. now cbn.
- intros _.
set (Σ' := GlobalContextMap.make Σ (fresh_globals_cons_inv wf)).
specialize (IHΣ (GlobalContextMap.map Σ') (GlobalContextMap.repr Σ') (GlobalContextMap.wf Σ')).
cbn in IHΣ. forward IHΣ. now depelim wfg.
intros hl. specialize (IHΣ hl) as [Σ'' [ext wfgd hl']].
∃ Σ''. split ⇒ //.
× destruct ext as [? ->].
now ∃ (a :: x).
× rewrite -hl'. f_equal.
clear -wfg.
eapply map_ext_in ⇒ kn hin. unfold on_snd. f_equal.
symmetry. eapply wellformed_optimize_decl_extends ⇒ //. cbn.
eapply lookup_env_In in hin. 2:now depelim wfg.
depelim wfg. eapply lookup_env_wellformed; tea.
cbn. now ∃ [a].
Qed.
Lemma lookup_env_map_snd Σ f kn : lookup_env (List.map (on_snd f) Σ) kn = option_map f (lookup_env Σ kn).
Proof.
induction Σ; cbn; auto.
case: eqb_spec ⇒ //.
Qed.
Lemma lookup_env_optimize_env_None {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
GlobalContextMap.lookup_env Σ kn = None →
lookup_env (optimize_env Σ) kn = None.
Proof.
rewrite GlobalContextMap.lookup_env_spec.
destruct Σ as [Σ map repr wf].
cbn. intros hl. rewrite lookup_env_map_snd hl //.
Qed.
Lemma lookup_env_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
wf_glob Σ →
lookup_env (optimize_env Σ) kn = option_map (optimize_decl Σ) (lookup_env Σ kn).
Proof.
intros wf.
rewrite -GlobalContextMap.lookup_env_spec.
destruct (GlobalContextMap.lookup_env Σ kn) eqn:hl.
- eapply lookup_env_optimize_env_Some in hl as [Σ' [ext wf' hl']] ⇒ /=.
rewrite hl'. f_equal.
eapply wellformed_optimize_decl_extends; eauto. auto.
- cbn. now eapply lookup_env_optimize_env_None in hl.
Qed.
Lemma is_propositional_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind :
wf_glob Σ →
inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (optimize_env Σ) ind.
Proof.
rewrite /inductive_isprop_and_pars ⇒ wf.
rewrite /lookup_inductive /lookup_minductive.
rewrite (lookup_env_optimize (inductive_mind ind) wf).
rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
/GlobalContextMap.lookup_minductive.
destruct lookup_env as [[decl|]|] ⇒ //.
Qed.
Lemma is_propositional_cstr_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind c :
wf_glob Σ →
constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (optimize_env Σ) ind c.
Proof.
rewrite /constructor_isprop_pars_decl ⇒ wf.
rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite (lookup_env_optimize (inductive_mind ind) wf).
rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
/GlobalContextMap.lookup_minductive.
destruct lookup_env as [[decl|]|] ⇒ //.
Qed.
Lemma closed_iota_red pars c args brs br :
forallb (closedn 0) args →
nth_error brs c = Some br →
#|skipn pars args| = #|br.1| →
closedn #|br.1| br.2 →
closed (iota_red pars args br).
Proof.
intros clargs hnth hskip clbr.
rewrite /iota_red.
eapply ECSubst.closed_substl ⇒ //.
now rewrite forallb_rev forallb_skipn.
now rewrite List.rev_length hskip Nat.add_0_r.
Qed.
Definition disable_prop_cases fl := {| with_prop_case := false; with_guarded_fix := fl.(@with_guarded_fix) ; with_constructor_as_block := false |}.
Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] ⇒ true | _ ⇒ false end.
Proof.
induction l using rev_ind; cbn.
- now rewrite andb_true_r.
- rewrite mkApps_app /=. now destruct l ⇒ /= //; rewrite andb_false_r.
Qed.
Lemma lookup_constructor_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} {ind c} :
wf_glob Σ →
lookup_constructor Σ ind c = lookup_constructor (optimize_env Σ) ind c.
Proof.
intros wfΣ. rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite lookup_env_optimize // /=. destruct lookup_env ⇒ // /=.
destruct g ⇒ //.
Qed.
Lemma lookup_projection_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} {p} :
wf_glob Σ →
lookup_projection Σ p = lookup_projection (optimize_env Σ) p.
Proof.
intros wfΣ. rewrite /lookup_projection.
rewrite -lookup_constructor_optimize //.
Qed.
Lemma constructor_isprop_pars_decl_inductive {Σ ind c} {prop pars cdecl} :
constructor_isprop_pars_decl Σ ind c = Some (prop, pars, cdecl) →
inductive_isprop_and_pars Σ ind = Some (prop, pars).
Proof.
rewrite /constructor_isprop_pars_decl /inductive_isprop_and_pars /lookup_constructor.
destruct lookup_inductive as [[mdecl idecl]|]=> /= //.
destruct nth_error ⇒ //. congruence.
Qed.
Lemma constructor_isprop_pars_decl_constructor {Σ ind c} {mdecl idecl cdecl} :
lookup_constructor Σ ind c = Some (mdecl, idecl, cdecl) →
constructor_isprop_pars_decl Σ ind c = Some (ind_propositional idecl, ind_npars mdecl, cdecl).
Proof.
rewrite /constructor_isprop_pars_decl. intros → ⇒ /= //.
Qed.
Lemma wf_mkApps Σ k f args : reflect (wellformed Σ k f ∧ forallb (wellformed Σ k) args) (wellformed Σ k (mkApps f args)).
Proof.
rewrite wellformed_mkApps //. eapply andP.
Qed.
Lemma substl_closed s t : closed t → substl s t = t.
Proof.
induction s in t |- *; cbn ⇒ //.
intros clt. rewrite csubst_closed //. now apply IHs.
Qed.
Lemma substl_rel s k a :
closed a →
nth_error s k = Some a →
substl s (tRel k) = a.
Proof.
intros cla.
induction s in k |- ×.
- rewrite nth_error_nil //.
- destruct k ⇒ //=.
× intros [= ->]. rewrite substl_closed //.
× intros hnth. now apply IHs.
Qed.
Lemma optimize_correct {fl} {wcon : with_constructor_as_block = false} { Σ : GlobalContextMap.t} t v :
wf_glob Σ →
@eval fl Σ t v →
wellformed Σ 0 t →
@eval fl (optimize_env Σ) (optimize Σ t) (optimize Σ v).
Proof.
intros wfΣ ev.
induction ev; simpl in ×.
- move/andP ⇒ [] cla clt. econstructor; eauto.
- move/andP ⇒ [] clf cla.
eapply eval_wellformed in ev2; tea ⇒ //.
eapply eval_wellformed in ev1; tea ⇒ //.
econstructor; eauto.
rewrite -(optimize_csubst _ 1) //.
apply IHev3. eapply wellformed_csubst ⇒ //.
- move/andP ⇒ [] clb0 clb1.
intuition auto.
eapply eval_wellformed in ev1; tea ⇒ //.
forward IHev2 by eapply wellformed_csubst ⇒ //.
econstructor; eauto. rewrite -(optimize_csubst _ 1) //.
- move/andP ⇒ [] /andP[] hl wfd wfbrs. rewrite optimize_mkApps in IHev1.
eapply eval_wellformed in ev1 ⇒ //.
move/wf_mkApps: ev1 ⇒ [] wfc' wfargs.
eapply nth_error_forallb in wfbrs; tea.
rewrite Nat.add_0_r in wfbrs.
forward IHev2. eapply wellformed_iota_red; tea ⇒ //.
rewrite optimize_iota_red in IHev2 ⇒ //. now rewrite e3.
econstructor; eauto.
rewrite -is_propositional_cstr_optimize //. tea.
rewrite nth_error_map e1 //. len. len.
- congruence.
- move/andP ⇒ [] /andP[] hl wfd wfbrs.
forward IHev2. eapply wellformed_substl; tea ⇒ //.
rewrite forallb_repeat //. len.
rewrite e0 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
rewrite optimize_substl in IHev2 ⇒ //.
rewrite forallb_repeat //. len.
rewrite e0 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
eapply eval_iota_sing ⇒ //; eauto.
rewrite -is_propositional_optimize //.
rewrite e0 //. simpl.
rewrite map_repeat in IHev2 ⇒ //.
- move/andP ⇒ [] clf cla. rewrite optimize_mkApps in IHev1.
simpl in ×.
eapply eval_wellformed in ev1 ⇒ //.
move/wf_mkApps: ev1 ⇒ [] wff wfargs.
eapply eval_fix; eauto.
rewrite map_length.
eapply optimize_cunfold_fix; tea.
rewrite optimize_mkApps in IHev3. apply IHev3.
rewrite wellformed_mkApps // wfargs.
eapply eval_wellformed in ev2; tas ⇒ //. rewrite ev2 /= !andb_true_r.
eapply wellformed_cunfold_fix; tea.
- move/andP ⇒ [] clf cla.
eapply eval_wellformed in ev1 ⇒ //.
move/wf_mkApps: ev1 ⇒ [] clfix clargs.
eapply eval_wellformed in ev2; tas ⇒ //.
rewrite optimize_mkApps in IHev1 |- ×.
simpl in ×. eapply eval_fix_value. auto. auto. auto.
eapply optimize_cunfold_fix; eauto.
now rewrite map_length.
- move/andP ⇒ [] clf cla.
eapply eval_wellformed in ev1 ⇒ //.
eapply eval_wellformed in ev2; tas ⇒ //.
simpl in ×. eapply eval_fix'. auto. auto.
eapply optimize_cunfold_fix; eauto.
eapply IHev2; tea. eapply IHev3.
apply/andP; split ⇒ //.
eapply wellformed_cunfold_fix; tea. now cbn.
- move/andP ⇒ [] /andP[] hl cd clbrs. specialize (IHev1 cd).
eapply eval_wellformed in ev1; tea ⇒ //.
move/wf_mkApps: ev1 ⇒ [] wfcof wfargs.
forward IHev2.
rewrite hl wellformed_mkApps // /= wfargs clbrs !andb_true_r.
eapply wellformed_cunfold_cofix; tea ⇒ //.
rewrite !optimize_mkApps /= in IHev1, IHev2.
eapply eval_cofix_case. tea.
eapply optimize_cunfold_cofix; tea.
exact IHev2.
- move/andP ⇒ [] hl hd.
rewrite GlobalContextMap.lookup_projection_spec in IHev2 |- ×.
destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl' ⇒ //.
eapply eval_wellformed in ev1 ⇒ //.
move/wf_mkApps: ev1 ⇒ [] wfcof wfargs.
forward IHev2.
{ rewrite /= wellformed_mkApps // wfargs andb_true_r.
eapply wellformed_cunfold_cofix; tea. }
rewrite optimize_mkApps /= in IHev1.
eapply eval_cofix_case. eauto.
eapply optimize_cunfold_cofix; tea.
rewrite optimize_mkApps in IHev2 ⇒ //.
- rewrite /declared_constant in isdecl.
move: (lookup_env_optimize c wfΣ).
rewrite isdecl /= //.
intros hl.
econstructor; tea. cbn. rewrite e //.
apply IHev.
eapply lookup_env_wellformed in wfΣ; tea.
move: wfΣ. rewrite /wf_global_decl /= e //.
- move⇒ /andP[] iss cld.
rewrite GlobalContextMap.lookup_projection_spec.
eapply eval_wellformed in ev1; tea ⇒ //.
move/wf_mkApps: ev1 ⇒ [] wfc wfargs.
destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' ⇒ //.
pose proof (lookup_projection_lookup_constructor hl').
rewrite (constructor_isprop_pars_decl_constructor H) in e0. noconf e0.
forward IHev1 by auto.
forward IHev2. eapply nth_error_forallb in wfargs; tea.
rewrite optimize_mkApps /= in IHev1.
eapply eval_iota; tea.
rewrite /constructor_isprop_pars_decl -lookup_constructor_optimize // H //= //.
rewrite H0 H1; reflexivity. cbn. reflexivity. len. len.
rewrite skipn_length. lia.
unfold iota_red. cbn.
rewrite (substl_rel _ _ (optimize Σ a)) ⇒ //.
{ eapply nth_error_forallb in wfargs; tea.
eapply wf_optimize in wfargs ⇒ //.
now eapply wellformed_closed in wfargs. }
pose proof (wellformed_projection_args wfΣ hl'). cbn in H1.
rewrite nth_error_rev. len. rewrite skipn_length. lia.
rewrite List.rev_involutive. len. rewrite skipn_length.
rewrite nth_error_skipn nth_error_map.
rewrite e1 -H1.
assert((ind_npars mdecl + cstr_nargs cdecl - ind_npars mdecl) = cstr_nargs cdecl) by lia.
rewrite H3.
eapply (f_equal (option_map (optimize Σ))) in e2.
cbn in e2. rewrite -e2. f_equal. f_equal. lia.
- congruence.
- move⇒ /andP[] iss cld.
rewrite GlobalContextMap.lookup_projection_spec.
destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' ⇒ //.
pose proof (lookup_projection_lookup_constructor hl').
simpl in H.
move: e. rewrite /inductive_isprop_and_pars.
rewrite (lookup_constructor_lookup_inductive H) /=.
intros [= eq <-].
eapply eval_iota_sing ⇒ //; eauto.
rewrite -is_propositional_optimize // /inductive_isprop_and_pars
(lookup_constructor_lookup_inductive H) //=. congruence.
have lenarg := wellformed_projection_args wfΣ hl'.
rewrite (substl_rel _ _ tBox) ⇒ //.
{ rewrite nth_error_repeat //. len. }
now constructor.
- move/andP⇒ [] clf cla.
rewrite optimize_mkApps.
eapply eval_construct; tea.
rewrite -lookup_constructor_optimize //. exact e0.
rewrite optimize_mkApps in IHev1. now eapply IHev1.
now len.
now eapply IHev2.
- congruence.
- move/andP ⇒ [] clf cla.
specialize (IHev1 clf). specialize (IHev2 cla).
eapply eval_app_cong; eauto.
eapply eval_to_value in ev1.
destruct ev1; simpl in *; eauto.
× destruct t ⇒ //; rewrite optimize_mkApps /=.
× destruct with_guarded_fix.
+ move: i.
rewrite !negb_or.
rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps.
destruct args using rev_case ⇒ // /=. rewrite map_app !mkApps_app /= //.
rewrite !andb_true_r.
rtoProp; intuition auto.
destruct v ⇒ /= //.
destruct v ⇒ /= //.
+ move: i.
rewrite !negb_or.
rewrite optimize_mkApps !isConstructApp_mkApps.
destruct args using rev_case ⇒ // /=. rewrite map_app !mkApps_app /= //.
destruct v ⇒ /= //.
- destruct t ⇒ //.
all:constructor; eauto.
cbn [atom optimize] in i |- ×.
rewrite -lookup_constructor_optimize //.
destruct l; cbn in *; eauto.
Qed.
From MetaCoq.Erasure Require Import EEtaExpanded.
Lemma isLambda_optimize Σ t : isLambda t → isLambda (optimize Σ t).
Proof. destruct t ⇒ //. Qed.
Lemma isBox_optimize Σ t : isBox t → isBox (optimize Σ t).
Proof. destruct t ⇒ //. Qed.
Lemma optimize_expanded {Σ : GlobalContextMap.t} t : expanded Σ t → expanded Σ (optimize Σ t).
Proof.
induction 1 using expanded_ind.
all:try solve[constructor; eauto; solve_all].
all:rewrite ?optimize_mkApps.
- eapply expanded_mkApps_expanded ⇒ //. solve_all.
- cbn -[GlobalContextMap.inductive_isprop_and_pars].
rewrite GlobalContextMap.lookup_projection_spec.
destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] ⇒ /= //.
2:constructor; eauto; solve_all.
destruct proj as [[ind npars] arg].
econstructor; eauto. repeat constructor.
- cbn. eapply expanded_tFix. solve_all.
rewrite isLambda_optimize //.
- eapply expanded_tConstruct_app; tea.
now len. solve_all.
Qed.
Lemma optimize_expanded_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ → expanded Σ t → expanded (optimize_env Σ) t.
Proof.
intros wf; induction 1 using expanded_ind.
all:try solve[constructor; eauto; solve_all].
eapply expanded_tConstruct_app.
destruct H as [[H ?] ?].
split ⇒ //. split ⇒ //. red.
red in H. rewrite lookup_env_optimize // /= H //. 1-2:eauto. auto. solve_all.
Qed.
Lemma optimize_expanded_decl {Σ : GlobalContextMap.t} t : expanded_decl Σ t → expanded_decl Σ (optimize_decl Σ t).
Proof.
destruct t as [[[]]|] ⇒ /= //.
unfold expanded_constant_decl ⇒ /=.
apply optimize_expanded.
Qed.
Lemma optimize_expanded_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ → expanded_decl Σ t → expanded_decl (optimize_env Σ) t.
Proof.
destruct t as [[[]]|] ⇒ /= //.
unfold expanded_constant_decl ⇒ /=.
apply optimize_expanded_irrel.
Qed.
Lemma optimize_env_extends' {efl : EEnvFlags} {Σ Σ' : GlobalContextMap.t} :
extends Σ Σ' →
wf_glob Σ' →
List.map (on_snd (optimize_decl Σ)) Σ.(GlobalContextMap.global_decls) =
List.map (on_snd (optimize_decl Σ')) Σ.(GlobalContextMap.global_decls).
Proof.
intros ext.
destruct Σ as [Σ map repr wf]; cbn in ×.
move⇒ wfΣ.
assert (extends Σ Σ); auto. now ∃ [].
assert (wf_glob Σ).
{ eapply extends_wf_glob. exact ext. tea. }
revert H H0.
generalize Σ at 1 3 5 6. intros Σ''.
induction Σ'' ⇒ //. cbn.
intros hin wfg. depelim wfg.
f_equal.
2:{ eapply IHΣ'' ⇒ //. destruct hin. ∃ (x ++ [(kn, d)]). rewrite -app_assoc /= //. }
unfold on_snd. cbn. f_equal.
eapply wellformed_optimize_decl_extends ⇒ //. cbn.
eapply extends_wf_global_decl. 3:tea.
eapply extends_wf_glob; tea.
destruct hin. ∃ (x ++ [(kn, d)]). rewrite -app_assoc /= //.
Qed.
Lemma optimize_env_eq {efl : EEnvFlags} (Σ : GlobalContextMap.t) : wf_glob Σ → optimize_env Σ = optimize_env' Σ.(GlobalContextMap.global_decls) Σ.(GlobalContextMap.wf).
Proof.
intros wf.
unfold optimize_env.
destruct Σ; cbn. cbn in wf.
induction global_decls in map, repr, wf0, wf |- × ⇒ //.
cbn. f_equal.
destruct a as [kn d]; unfold on_snd; cbn. f_equal. symmetry.
eapply wellformed_optimize_decl_extends ⇒ //. cbn. now depelim wf. cbn. now ∃ [(kn, d)]. cbn.
set (Σg' := GlobalContextMap.make global_decls (fresh_globals_cons_inv wf0)).
erewrite <- (IHglobal_decls (GlobalContextMap.map Σg') (GlobalContextMap.repr Σg')).
2:now depelim wf.
set (Σg := {| GlobalContextMap.global_decls := _ :: _ |}).
symmetry. eapply (optimize_env_extends' (Σ := Σg') (Σ' := Σg)) ⇒ //.
cbn. now ∃ [a].
Qed.
Lemma optimize_env_expanded {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
wf_glob Σ → expanded_global_env Σ → expanded_global_env (optimize_env Σ).
Proof.
unfold expanded_global_env; move⇒ wfg.
rewrite optimize_env_eq //.
destruct Σ as [Σ map repr wf]. cbn in ×.
clear map repr.
induction 1; cbn; constructor; auto.
cbn in IHexpanded_global_declarations.
unshelve eapply IHexpanded_global_declarations. now depelim wfg. cbn.
set (Σ' := GlobalContextMap.make _ _).
rewrite -(optimize_env_eq Σ'). cbn. now depelim wfg.
eapply (optimize_expanded_decl_irrel (Σ := Σ')). now depelim wfg.
now unshelve eapply (optimize_expanded_decl (Σ:=Σ')).
Qed.
Definition disable_projections_term_flags (et : ETermFlags) :=
{| has_tBox := has_tBox
; has_tRel := has_tRel
; has_tVar := has_tVar
; has_tEvar := has_tEvar
; has_tLambda := has_tLambda
; has_tLetIn := has_tLetIn
; has_tApp := has_tApp
; has_tConst := has_tConst
; has_tConstruct := has_tConstruct
; has_tCase := true
; has_tProj := false
; has_tFix := has_tFix
; has_tCoFix := has_tCoFix
|}.
Definition disable_projections_env_flag (efl : EEnvFlags) :=
{| has_axioms := true;
term_switches := disable_projections_term_flags term_switches;
has_cstr_params := true ;
cstr_as_blocks := efl.(cstr_as_blocks) |}.
Lemma optimize_wellformed {efl : EEnvFlags} {Σ : GlobalContextMap.t} n t :
has_tBox → has_tRel →
wf_glob Σ → EWellformed.wellformed Σ n t →
EWellformed.wellformed (efl := disable_projections_env_flag efl) Σ n (optimize Σ t).
Proof.
intros hbox hrel wfΣ.
induction t in n |- × using EInduction.term_forall_list_ind ⇒ //.
all:try solve [cbn; rtoProp; intuition auto; solve_all].
- simpl. destruct lookup_constant ⇒ //.
move/andP ⇒ [] hasc _ ⇒ //. now rewrite hasc.
- cbn -[lookup_constructor_pars_args]. intros. rtoProp. repeat split; eauto.
destruct cstr_as_blocks; rtoProp; eauto.
destruct lookup_constructor_pars_args as [ [] | ]; eauto. split; len. solve_all. split; eauto.
solve_all. now destruct args; invs H0.
- cbn. move/andP ⇒ [] /andP[] hast hl wft.
rewrite GlobalContextMap.lookup_projection_spec.
destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl'; auto ⇒ //.
simpl.
rewrite (lookup_constructor_lookup_inductive (lookup_projection_lookup_constructor hl')) /=.
rewrite hrel IHt //= andb_true_r.
have hargs' := wellformed_projection_args wfΣ hl'.
apply Nat.ltb_lt. len.
- cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len.
unfold test_def in ×. len. eauto.
- cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len.
unfold test_def in ×. len. eauto.
Qed.
Import EWellformed.
Lemma optimize_wellformed_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
wf_glob Σ →
∀ n, wellformed (efl := disable_projections_env_flag efl) Σ n t →
wellformed (efl := disable_projections_env_flag efl) (optimize_env Σ) n t.
Proof.
intros wfΣ. induction t using EInduction.term_forall_list_ind; cbn ⇒ //.
all:try solve [intros; unfold wf_fix_gen in *; rtoProp; intuition eauto; solve_all].
- rewrite lookup_env_optimize //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //.
- rewrite lookup_env_optimize //.
destruct lookup_env eqn:hl ⇒ // /=; intros; rtoProp; eauto.
destruct g eqn:hg ⇒ /= //; intros; rtoProp; eauto.
repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all.
- rewrite lookup_env_optimize //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //. subst g.
destruct nth_error ⇒ /= //.
intros; rtoProp; intuition auto; solve_all.
Qed.
Lemma optimize_wellformed_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} d :
wf_glob Σ →
wf_global_decl (efl:= disable_projections_env_flag efl) Σ d →
wf_global_decl (efl := disable_projections_env_flag efl) (optimize_env Σ) d.
Proof.
intros wf; destruct d ⇒ /= //.
destruct (cst_body c) ⇒ /= //.
now eapply optimize_wellformed_irrel.
Qed.
Lemma optimize_decl_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
has_tBox → has_tRel → wf_glob Σ →
∀ d, wf_global_decl Σ d →
wf_global_decl (efl := disable_projections_env_flag efl) (optimize_env Σ) (optimize_decl Σ d).
Proof.
intros hasb hasr wf d.
intros hd.
eapply optimize_wellformed_decl_irrel; tea; eauto.
move: hd.
destruct d ⇒ /= //.
destruct (cst_body c) ⇒ /= //.
intros hwf. eapply optimize_wellformed ⇒ //. auto.
destruct efl ⇒ //. destruct m ⇒ //. cbn. unfold wf_minductive.
cbn. move/andP ⇒ [] hp //.
Qed.
Lemma fresh_global_optimize_env {Σ : GlobalContextMap.t} kn :
fresh_global kn Σ →
fresh_global kn (optimize_env Σ).
Proof.
destruct Σ as [Σ map repr wf]; cbn in ×.
induction 1; cbn; constructor; auto.
now eapply Forall_map; cbn.
Qed.
Lemma optimize_env_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
has_tBox → has_tRel →
wf_glob Σ → wf_glob (efl := disable_projections_env_flag efl) (optimize_env Σ).
Proof.
intros hasb hasrel.
intros wfg. rewrite optimize_env_eq //.
destruct Σ as [Σ map repr wf]; cbn in ×.
clear map repr.
induction wfg; cbn; constructor; auto.
- rewrite /= -(optimize_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
eapply optimize_decl_wf ⇒ //.
- rewrite /= -(optimize_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
now eapply fresh_global_optimize_env.
Qed.
Definition optimize_program (p : eprogram_env) :=
(optimize_env p.1, optimize p.1 p.2).
Definition optimize_program_wf {efl : EEnvFlags} (p : eprogram_env) {hastbox : has_tBox} {hastrel : has_tRel} :
wf_eprogram_env efl p → wf_eprogram (disable_projections_env_flag efl) (optimize_program p).
Proof.
intros []; split.
now eapply optimize_env_wf.
cbn. eapply optimize_wellformed_irrel ⇒ //. now eapply optimize_wellformed.
Qed.
Definition optimize_program_expanded {efl} (p : eprogram_env) :
wf_eprogram_env efl p →
expanded_eprogram_env_cstrs p → expanded_eprogram_cstrs (optimize_program p).
Proof.
unfold expanded_eprogram_env_cstrs.
move⇒ [wfe wft] /andP[] etae etat.
apply/andP; split.
cbn. eapply expanded_global_env_isEtaExp_env, optimize_env_expanded ⇒ //.
now eapply isEtaExp_env_expanded_global_env.
eapply expanded_isEtaExp.
eapply optimize_expanded_irrel ⇒ //.
now apply optimize_expanded, isEtaExp_expanded.
Qed.