Library MetaCoq.Erasure.EGenericMapEnv
From Coq Require Import Utf8 Program.
From MetaCoq.Template Require Import config utils Kernames BasicAst EnvMap.
From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd 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.
Section sec.
Variable gen_transform : global_context → term → term.
Definition gen_transform_constant_decl Σ cb :=
{| cst_body := option_map (gen_transform Σ) cb.(cst_body) |}.
Definition gen_transform_decl Σ d :=
match d with
| ConstantDecl cb ⇒ ConstantDecl (gen_transform_constant_decl Σ cb)
| InductiveDecl idecl ⇒ d
end.
Definition gen_transform_env Σ :=
map (on_snd (gen_transform_decl Σ)) Σ.
Program Fixpoint gen_transform_env' Σ : global_context :=
match Σ with
| [] ⇒ []
| hd :: tl ⇒ on_snd (gen_transform_decl tl) hd :: gen_transform_env' tl
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 -[lookup_projection].
unfold lookup_projection.
destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl ⇒ //.
simpl.
rewrite (extends_lookup_constructor wf ext _ _ _ hl) //.
Qed.
Variable efl' : EEnvFlags.
Variable efl : EEnvFlags.
Hypothesis wellformed_gen_transform_extends : ∀ {Σ : global_context} t,
∀ n, EWellformed.wellformed Σ n t →
∀ {Σ' : global_context}, extends Σ Σ' → wf_glob Σ' →
gen_transform Σ t = gen_transform Σ' t.
Lemma wellformed_gen_transform_decl_extends {Σ : global_context} t :
wf_global_decl Σ t →
∀ {Σ' : global_context}, extends Σ Σ' → wf_glob Σ' →
gen_transform_decl Σ t = gen_transform_decl Σ' t.
Proof.
destruct t ⇒ /= //.
intros wf Σ' ext wf'. f_equal. unfold gen_transform_constant_decl. f_equal.
destruct (cst_body c) ⇒ /= //. f_equal.
now eapply wellformed_gen_transform_extends.
Qed.
Lemma lookup_env_gen_transform_env_Some {Σ : global_context} kn d :
wf_glob Σ →
lookup_env Σ kn = Some d →
∑ Σ' : global_context,
[× extends Σ' Σ, wf_global_decl Σ' d &
lookup_env (gen_transform_env Σ) kn = Some (gen_transform_decl Σ' d)].
Proof.
induction Σ in |- *; simpl; auto ⇒ //.
intros wfg.
case: eqb_specT ⇒ //.
- intros →. cbn. intros [= <-]. ∃ Σ. split.
now eexists [_].
cbn. now depelim wfg.
f_equal. symmetry. eapply wellformed_gen_transform_decl_extends. cbn. now depelim wfg.
cbn. now ∃ [a]. now cbn.
- intros _.
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 wellformed_gen_transform_extends.
eapply map_ext_in ⇒ kn hin. unfold on_snd. f_equal.
symmetry. eapply wellformed_gen_transform_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_gen_transform_env_None {Σ : global_context} kn :
lookup_env Σ kn = None →
lookup_env (gen_transform_env Σ) kn = None.
Proof.
cbn. intros hl. rewrite lookup_env_map_snd hl //.
Qed.
Lemma lookup_env_gen_transform {Σ : global_context} kn :
wf_glob Σ →
lookup_env (gen_transform_env Σ) kn = option_map (gen_transform_decl Σ) (lookup_env Σ kn).
Proof.
intros wf.
destruct (lookup_env Σ kn) eqn:hl.
- eapply lookup_env_gen_transform_env_Some in hl as [Σ' [ext wf' hl']] ⇒ /=.
rewrite hl'. f_equal.
eapply wellformed_gen_transform_decl_extends; eauto. auto.
- cbn. now eapply lookup_env_gen_transform_env_None in hl.
Qed.
Lemma is_propositional_gen_transform {Σ : global_context} ind :
wf_glob Σ →
inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (gen_transform_env Σ) ind.
Proof.
rewrite /inductive_isprop_and_pars ⇒ wf.
rewrite /lookup_inductive /lookup_minductive.
rewrite (lookup_env_gen_transform (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_gen_transform {Σ : global_context} ind c :
wf_glob Σ →
constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (gen_transform_env Σ) ind c.
Proof.
rewrite /constructor_isprop_pars_decl ⇒ wf.
rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite (lookup_env_gen_transform (inductive_mind ind) wf).
rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
/GlobalContextMap.lookup_minductive.
destruct lookup_env as [[decl|]|] ⇒ //.
Qed.
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_gen_transform {Σ : global_context} {ind c} :
wf_glob Σ →
lookup_constructor Σ ind c = lookup_constructor (gen_transform_env Σ) ind c.
Proof.
intros wfΣ. rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite lookup_env_gen_transform // /=. destruct lookup_env ⇒ // /=.
destruct g ⇒ //.
Qed.
Lemma lookup_projection_gen_transform {Σ : global_context} {p} :
wf_glob Σ →
lookup_projection Σ p = lookup_projection (gen_transform_env Σ) p.
Proof.
intros wfΣ. rewrite /lookup_projection.
rewrite -lookup_constructor_gen_transform //.
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 (ha : has_tApp) Σ k f args : reflect (wellformed Σ k f ∧ forallb (wellformed Σ k) args) (wellformed Σ k (mkApps f args)).
Proof.
rewrite wellformed_mkApps //. eapply andP.
Qed.
Lemma gen_transform_env_extends' {Σ Σ' : global_context} :
extends Σ Σ' →
wf_glob Σ' →
List.map (on_snd (gen_transform_decl Σ)) Σ =
List.map (on_snd (gen_transform_decl Σ')) Σ.
Proof.
intros ext.
move⇒ wfΣ.
assert (Hext : extends Σ Σ); auto. now ∃ [].
assert (Hwfg : wf_glob Σ).
{ eapply extends_wf_glob. exact ext. tea. }
revert Hext Hwfg.
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_gen_transform_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 gen_transform_env_eq (Σ : global_context) : wf_glob Σ → gen_transform_env Σ = gen_transform_env' Σ.
Proof.
intros wf.
unfold gen_transform_env.
induction Σ ⇒ //.
cbn. f_equal.
destruct a as [kn d]; unfold on_snd; cbn. f_equal. symmetry.
eapply wellformed_gen_transform_decl_extends ⇒ //. cbn. now depelim wf. cbn. now ∃ [(kn, d)]. cbn.
erewrite <- IHΣ.
2:now depelim wf.
symmetry. eapply gen_transform_env_extends'; eauto.
cbn. now ∃ [a].
Qed.
Variable Pre : global_context → term → Prop.
Hypothesis gen_transform_wellformed : ∀ {Σ : global_context} n t,
has_tBox → has_tRel → Pre Σ t →
@wf_glob efl Σ → @EWellformed.wellformed efl Σ n t →
EWellformed.wellformed (efl := efl') Σ n (gen_transform Σ t).
Import EWellformed.
Lemma gen_transform_wellformed_irrel {Σ : global_context} t :
wf_glob Σ →
∀ n, wellformed (efl := efl') Σ n t →
wellformed (efl := efl') (gen_transform_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_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //. destruct (cst_body c); cbn; eauto.
- rewrite lookup_env_gen_transform //.
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_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //. subst g.
destruct nth_error ⇒ /= //.
intros; rtoProp; intuition auto; solve_all.
- rewrite lookup_env_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=; intros; rtoProp; repeat split; eauto.
destruct g eqn:hg ⇒ /= //.
Qed.
Lemma gen_transform_wellformed_decl_irrel {Σ : global_context} d :
wf_glob Σ →
wf_global_decl (efl:= efl') Σ d →
wf_global_decl (efl := efl') (gen_transform_env Σ) d.
Proof.
intros wf; destruct d ⇒ /= //.
destruct (cst_body c) ⇒ /= //.
now eapply gen_transform_wellformed_irrel.
Qed.
Hypothesis axioms_efl : ∀ _ : is_true (@has_axioms efl), is_true (@has_axioms efl').
Hypothesis cstrs_efl : ∀ _ : is_true (@has_cstr_params efl), is_true (@has_cstr_params efl').
Definition Pre_decl Σ d := match d with ConstantDecl cb ⇒ match cb.(cst_body) with Some b ⇒ Pre Σ b | _ ⇒ True end | _ ⇒ True end.
Lemma gen_transform_decl_wf {Σ : global_context} :
has_tBox → has_tRel → wf_glob Σ →
∀ d, wf_global_decl Σ d → Pre_decl Σ d →
wf_global_decl (efl := efl') (gen_transform_env Σ) (gen_transform_decl Σ d).
Proof.
intros hasb hasr wf d.
intros hd. intros pre.
eapply gen_transform_wellformed_decl_irrel; tea; eauto.
move: hd.
destruct d ⇒ /= //. cbn in pre.
destruct (cst_body c) ⇒ /= //.
intros hwf. eapply gen_transform_wellformed ⇒ //. auto.
destruct efl ⇒ //; eauto. destruct m ⇒ //. cbn. unfold wf_minductive.
cbn. move/andP ⇒ [] hp //. rtoProp. solve_all.
eapply orb_true_iff. eapply orb_true_iff in hp as []; eauto.
left. eapply cstrs_efl. now rewrite H.
Qed.
Lemma fresh_global_gen_transform_env {Σ : global_context} kn :
fresh_global kn Σ →
fresh_global kn (gen_transform_env Σ).
Proof.
induction 1; cbn; constructor; auto.
now eapply Forall_map; cbn.
Qed.
Fixpoint Pre_glob Σ :=
match Σ with
| nil ⇒ True
| (kn, d) :: Σ ⇒ Pre_decl Σ d ∧ Pre_glob Σ
end.
Lemma gen_transform_env_wf {Σ : global_context} :
has_tBox → has_tRel → Pre_glob Σ →
wf_glob Σ → wf_glob (efl := efl') (gen_transform_env Σ).
Proof.
intros hasb hasrel pre.
intros wfg. rewrite gen_transform_env_eq //.
induction wfg; cbn; constructor; invs pre; auto.
- rewrite /= -(gen_transform_env_eq Σ) ⇒ //. eauto.
eapply gen_transform_decl_wf ⇒ //.
- rewrite /= -(gen_transform_env_eq Σ) //.
now eapply fresh_global_gen_transform_env.
Qed.
End sec.
From MetaCoq.Template Require Import config utils Kernames BasicAst EnvMap.
From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd 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.
Section sec.
Variable gen_transform : global_context → term → term.
Definition gen_transform_constant_decl Σ cb :=
{| cst_body := option_map (gen_transform Σ) cb.(cst_body) |}.
Definition gen_transform_decl Σ d :=
match d with
| ConstantDecl cb ⇒ ConstantDecl (gen_transform_constant_decl Σ cb)
| InductiveDecl idecl ⇒ d
end.
Definition gen_transform_env Σ :=
map (on_snd (gen_transform_decl Σ)) Σ.
Program Fixpoint gen_transform_env' Σ : global_context :=
match Σ with
| [] ⇒ []
| hd :: tl ⇒ on_snd (gen_transform_decl tl) hd :: gen_transform_env' tl
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 -[lookup_projection].
unfold lookup_projection.
destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl ⇒ //.
simpl.
rewrite (extends_lookup_constructor wf ext _ _ _ hl) //.
Qed.
Variable efl' : EEnvFlags.
Variable efl : EEnvFlags.
Hypothesis wellformed_gen_transform_extends : ∀ {Σ : global_context} t,
∀ n, EWellformed.wellformed Σ n t →
∀ {Σ' : global_context}, extends Σ Σ' → wf_glob Σ' →
gen_transform Σ t = gen_transform Σ' t.
Lemma wellformed_gen_transform_decl_extends {Σ : global_context} t :
wf_global_decl Σ t →
∀ {Σ' : global_context}, extends Σ Σ' → wf_glob Σ' →
gen_transform_decl Σ t = gen_transform_decl Σ' t.
Proof.
destruct t ⇒ /= //.
intros wf Σ' ext wf'. f_equal. unfold gen_transform_constant_decl. f_equal.
destruct (cst_body c) ⇒ /= //. f_equal.
now eapply wellformed_gen_transform_extends.
Qed.
Lemma lookup_env_gen_transform_env_Some {Σ : global_context} kn d :
wf_glob Σ →
lookup_env Σ kn = Some d →
∑ Σ' : global_context,
[× extends Σ' Σ, wf_global_decl Σ' d &
lookup_env (gen_transform_env Σ) kn = Some (gen_transform_decl Σ' d)].
Proof.
induction Σ in |- *; simpl; auto ⇒ //.
intros wfg.
case: eqb_specT ⇒ //.
- intros →. cbn. intros [= <-]. ∃ Σ. split.
now eexists [_].
cbn. now depelim wfg.
f_equal. symmetry. eapply wellformed_gen_transform_decl_extends. cbn. now depelim wfg.
cbn. now ∃ [a]. now cbn.
- intros _.
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 wellformed_gen_transform_extends.
eapply map_ext_in ⇒ kn hin. unfold on_snd. f_equal.
symmetry. eapply wellformed_gen_transform_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_gen_transform_env_None {Σ : global_context} kn :
lookup_env Σ kn = None →
lookup_env (gen_transform_env Σ) kn = None.
Proof.
cbn. intros hl. rewrite lookup_env_map_snd hl //.
Qed.
Lemma lookup_env_gen_transform {Σ : global_context} kn :
wf_glob Σ →
lookup_env (gen_transform_env Σ) kn = option_map (gen_transform_decl Σ) (lookup_env Σ kn).
Proof.
intros wf.
destruct (lookup_env Σ kn) eqn:hl.
- eapply lookup_env_gen_transform_env_Some in hl as [Σ' [ext wf' hl']] ⇒ /=.
rewrite hl'. f_equal.
eapply wellformed_gen_transform_decl_extends; eauto. auto.
- cbn. now eapply lookup_env_gen_transform_env_None in hl.
Qed.
Lemma is_propositional_gen_transform {Σ : global_context} ind :
wf_glob Σ →
inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (gen_transform_env Σ) ind.
Proof.
rewrite /inductive_isprop_and_pars ⇒ wf.
rewrite /lookup_inductive /lookup_minductive.
rewrite (lookup_env_gen_transform (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_gen_transform {Σ : global_context} ind c :
wf_glob Σ →
constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (gen_transform_env Σ) ind c.
Proof.
rewrite /constructor_isprop_pars_decl ⇒ wf.
rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite (lookup_env_gen_transform (inductive_mind ind) wf).
rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
/GlobalContextMap.lookup_minductive.
destruct lookup_env as [[decl|]|] ⇒ //.
Qed.
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_gen_transform {Σ : global_context} {ind c} :
wf_glob Σ →
lookup_constructor Σ ind c = lookup_constructor (gen_transform_env Σ) ind c.
Proof.
intros wfΣ. rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
rewrite lookup_env_gen_transform // /=. destruct lookup_env ⇒ // /=.
destruct g ⇒ //.
Qed.
Lemma lookup_projection_gen_transform {Σ : global_context} {p} :
wf_glob Σ →
lookup_projection Σ p = lookup_projection (gen_transform_env Σ) p.
Proof.
intros wfΣ. rewrite /lookup_projection.
rewrite -lookup_constructor_gen_transform //.
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 (ha : has_tApp) Σ k f args : reflect (wellformed Σ k f ∧ forallb (wellformed Σ k) args) (wellformed Σ k (mkApps f args)).
Proof.
rewrite wellformed_mkApps //. eapply andP.
Qed.
Lemma gen_transform_env_extends' {Σ Σ' : global_context} :
extends Σ Σ' →
wf_glob Σ' →
List.map (on_snd (gen_transform_decl Σ)) Σ =
List.map (on_snd (gen_transform_decl Σ')) Σ.
Proof.
intros ext.
move⇒ wfΣ.
assert (Hext : extends Σ Σ); auto. now ∃ [].
assert (Hwfg : wf_glob Σ).
{ eapply extends_wf_glob. exact ext. tea. }
revert Hext Hwfg.
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_gen_transform_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 gen_transform_env_eq (Σ : global_context) : wf_glob Σ → gen_transform_env Σ = gen_transform_env' Σ.
Proof.
intros wf.
unfold gen_transform_env.
induction Σ ⇒ //.
cbn. f_equal.
destruct a as [kn d]; unfold on_snd; cbn. f_equal. symmetry.
eapply wellformed_gen_transform_decl_extends ⇒ //. cbn. now depelim wf. cbn. now ∃ [(kn, d)]. cbn.
erewrite <- IHΣ.
2:now depelim wf.
symmetry. eapply gen_transform_env_extends'; eauto.
cbn. now ∃ [a].
Qed.
Variable Pre : global_context → term → Prop.
Hypothesis gen_transform_wellformed : ∀ {Σ : global_context} n t,
has_tBox → has_tRel → Pre Σ t →
@wf_glob efl Σ → @EWellformed.wellformed efl Σ n t →
EWellformed.wellformed (efl := efl') Σ n (gen_transform Σ t).
Import EWellformed.
Lemma gen_transform_wellformed_irrel {Σ : global_context} t :
wf_glob Σ →
∀ n, wellformed (efl := efl') Σ n t →
wellformed (efl := efl') (gen_transform_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_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //. destruct (cst_body c); cbn; eauto.
- rewrite lookup_env_gen_transform //.
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_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=.
destruct g eqn:hg ⇒ /= //. subst g.
destruct nth_error ⇒ /= //.
intros; rtoProp; intuition auto; solve_all.
- rewrite lookup_env_gen_transform //.
destruct lookup_env eqn:hl ⇒ // /=; intros; rtoProp; repeat split; eauto.
destruct g eqn:hg ⇒ /= //.
Qed.
Lemma gen_transform_wellformed_decl_irrel {Σ : global_context} d :
wf_glob Σ →
wf_global_decl (efl:= efl') Σ d →
wf_global_decl (efl := efl') (gen_transform_env Σ) d.
Proof.
intros wf; destruct d ⇒ /= //.
destruct (cst_body c) ⇒ /= //.
now eapply gen_transform_wellformed_irrel.
Qed.
Hypothesis axioms_efl : ∀ _ : is_true (@has_axioms efl), is_true (@has_axioms efl').
Hypothesis cstrs_efl : ∀ _ : is_true (@has_cstr_params efl), is_true (@has_cstr_params efl').
Definition Pre_decl Σ d := match d with ConstantDecl cb ⇒ match cb.(cst_body) with Some b ⇒ Pre Σ b | _ ⇒ True end | _ ⇒ True end.
Lemma gen_transform_decl_wf {Σ : global_context} :
has_tBox → has_tRel → wf_glob Σ →
∀ d, wf_global_decl Σ d → Pre_decl Σ d →
wf_global_decl (efl := efl') (gen_transform_env Σ) (gen_transform_decl Σ d).
Proof.
intros hasb hasr wf d.
intros hd. intros pre.
eapply gen_transform_wellformed_decl_irrel; tea; eauto.
move: hd.
destruct d ⇒ /= //. cbn in pre.
destruct (cst_body c) ⇒ /= //.
intros hwf. eapply gen_transform_wellformed ⇒ //. auto.
destruct efl ⇒ //; eauto. destruct m ⇒ //. cbn. unfold wf_minductive.
cbn. move/andP ⇒ [] hp //. rtoProp. solve_all.
eapply orb_true_iff. eapply orb_true_iff in hp as []; eauto.
left. eapply cstrs_efl. now rewrite H.
Qed.
Lemma fresh_global_gen_transform_env {Σ : global_context} kn :
fresh_global kn Σ →
fresh_global kn (gen_transform_env Σ).
Proof.
induction 1; cbn; constructor; auto.
now eapply Forall_map; cbn.
Qed.
Fixpoint Pre_glob Σ :=
match Σ with
| nil ⇒ True
| (kn, d) :: Σ ⇒ Pre_decl Σ d ∧ Pre_glob Σ
end.
Lemma gen_transform_env_wf {Σ : global_context} :
has_tBox → has_tRel → Pre_glob Σ →
wf_glob Σ → wf_glob (efl := efl') (gen_transform_env Σ).
Proof.
intros hasb hasrel pre.
intros wfg. rewrite gen_transform_env_eq //.
induction wfg; cbn; constructor; invs pre; auto.
- rewrite /= -(gen_transform_env_eq Σ) ⇒ //. eauto.
eapply gen_transform_decl_wf ⇒ //.
- rewrite /= -(gen_transform_env_eq Σ) //.
now eapply fresh_global_gen_transform_env.
Qed.
End sec.