Library MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd
(* Distributed under the terms of the MIT license. *)
From Stdlib Require Import Utf8 Program ssreflect ssrbool.
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config Kernames BasicAst EnvMap.
From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
Set Asymmetric Patterns.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
#[export]
Hint Constructors eval : core.
Definition atomic_term (t : term) :=
match t with
| tBox | tConst _ | tRel _ | tVar _ | tPrim _ ⇒ true
| _ ⇒ false
end.
Definition has_atom {etfl : ETermFlags} (t : term) :=
match t with
| tBox ⇒ has_tBox
| tConst _ ⇒ has_tConst
| tRel _ ⇒ has_tRel
| tVar _ ⇒ has_tVar
| _ ⇒ false
end.
Section OnSubterm.
Context {etfl : ETermFlags}.
Inductive on_subterms (Q : nat → term → Type) (n : nat) : term → Type :=
| on_atom t : has_atom t → atomic_term t → on_subterms Q n t
| on_evar k l : has_tEvar → All (Q n) l → on_subterms Q n (tEvar k l)
| on_lambda na t : has_tLambda → Q (S n) t → on_subterms Q n (tLambda na t)
| on_letin na t u : has_tLetIn → Q n t → Q (S n) u → on_subterms Q n (tLetIn na t u)
| on_app f u : has_tApp → Q n f → Q n u → on_subterms Q n (tApp f u)
| on_cstr i k args : has_tConstruct → All (Q n) args → on_subterms Q n (tConstruct i k args)
| on_case ci discr brs : has_tCase → Q n discr →
All (fun br ⇒ Q (#|br.1| + n) br.2) brs → on_subterms Q n (tCase ci discr brs)
| on_proj p c : has_tProj → Q n c → on_subterms Q n (tProj p c)
| on_fix mfix idx : has_tFix → All (fun d ⇒ Q (#|mfix| + n) d.(dbody)) mfix → on_subterms Q n (tFix mfix idx)
| on_cofix mfix idx : has_tCoFix → All (fun d ⇒ Q (#|mfix| + n) d.(dbody)) mfix → on_subterms Q n (tCoFix mfix idx)
| on_prim p : has_prim p → primProp (Q n) p → on_subterms Q n (tPrim p)
| on_lazy t : has_tLazy_Force → Q n t → on_subterms Q n (tLazy t)
| on_force t : has_tLazy_Force → Q n t → on_subterms Q n (tForce t).
Derive Signature for on_subterms.
End OnSubterm.
Class Qpres {etfl : ETermFlags} (Q : nat → term → Type) := qpres : ∀ n t, Q n t → on_subterms Q n t.
#[export] Hint Mode Qpres - ! : typeclass_instances.
Class Qapp {etfl : ETermFlags} (Q : nat → term → Type) := qapp : has_tApp → ∀ n f args, Q n (mkApps f args) <~> Q n f × All (Q n) args.
#[export] Hint Mode Qapp - ! : typeclass_instances.
Class Qcase {etfl : ETermFlags} (Q : nat → term → Type) := qcase : has_tCase →
∀ n ci discr brs, Q n (tCase ci discr brs) → ∀ discr', Q n discr' → Q n (tCase ci discr' brs).
#[export] Hint Mode Qcase - ! : typeclass_instances.
(* Class Qcstr {etfl : ETermFlags} (Q : nat -> term -> Type) := *)
(* qcstr : has_tConstruct -> forall i n args, Q n (tConstruct i n args) Q n discr × All (fun br => Q (|br.1| + n) br.2) brs. *)
(* [export] Hint Mode Qcase - ! : typeclass_instances. *)
Class Qproj {etfl : ETermFlags} (Q : nat → term → Type) := qproj : has_tProj → ∀ n p discr, Q n (tProj p discr) → ∀ discr', Q n discr' → Q n (tProj p discr').
#[export] Hint Mode Qproj - ! : typeclass_instances.
Class Qfix {etfl : ETermFlags} (Q : nat → term → Type) := qfix : has_tFix → ∀ n mfix idx, idx < #|mfix| → Q n (tFix mfix idx) → ∀ idx', idx' < #|mfix| → Q n (tFix mfix idx').
#[export] Hint Mode Qfix - ! : typeclass_instances.
Class Qcofix {etfl : ETermFlags} (Q : nat → term → Type) := qcofix : has_tCoFix → ∀ n mfix idx, idx < #|mfix| → Q n (tCoFix mfix idx) → ∀ idx', idx' < #|mfix| → Q n (tCoFix mfix idx').
#[export] Hint Mode Qcofix - ! : typeclass_instances.
Class Qsubst (Q : nat → term → Type) := qsubst : ∀ t l, Q (#|l|) t → All (Q 0) l → Q 0 (substl l t).
#[export] Hint Mode Qsubst ! : typeclass_instances.
Class Qfixs (Q : nat → term → Type) := qfixs : ∀ mfix idx, Q 0 (tFix mfix idx) →
∀ args fn, cunfold_fix mfix idx = Some (args, fn) →
Q 0 fn.
#[export] Hint Mode Qfixs ! : typeclass_instances.
Class Qcofixs (Q : nat → term → Type) := qcofixs : ∀ mfix idx, Q 0 (tCoFix mfix idx) →
∀ args fn, cunfold_cofix mfix idx = Some (args, fn) →
Q 0 fn.
#[export] Hint Mode Qcofixs ! : typeclass_instances.
Lemma Qfix_subst {etfl : ETermFlags} mfix Q : has_tFix → Qfix Q → Qpres Q → ∀ idx, idx < #|mfix| → Q 0 (tFix mfix idx) → All (Q 0) (fix_subst mfix).
Proof.
intros hasfix qfix qpre; unfold fix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
induction n. intros. constructor; auto.
intros. constructor. eapply qfix ⇒ //. 2:tea. tea.
eapply IHn. lia. 2:tea. assumption.
Qed.
Lemma Qcofix_subst {etfl : ETermFlags} mfix Q : has_tCoFix → Qcofix Q → Qpres Q → ∀ idx, idx < #|mfix| → Q 0 (tCoFix mfix idx) → All (Q 0) (cofix_subst mfix).
Proof.
intros hascofix qcofix qpre; unfold cofix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
induction n. intros. constructor; auto.
intros. constructor. eapply qcofix ⇒ //. 2:tea. tea.
eapply IHn. lia. 2:tea. assumption.
Qed.
#[export] Instance Qsubst_Qfixs {etfl : ETermFlags} Q : Qpres Q → Qfix Q → Qsubst Q → Qfixs Q.
Proof.
move⇒ qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tFix).
{ eapply qpres in hfix. now depelim hfix. }
rewrite /cunfold_fix.
destruct nth_error eqn:hnth ⇒ //.
pose proof (nth_error_Some_length hnth).
epose proof (Qfix_subst _ _ hasfix qfix qpres idx H hfix).
intros [= <-]. subst fn.
eapply Hs. rewrite fix_subst_length //.
eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a.
assumption.
Qed.
#[export] Instance Qsubst_Qcofixs {etfl : ETermFlags} Q : Qpres Q → Qcofix Q → Qsubst Q → Qcofixs Q.
Proof.
move⇒ qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tCoFix).
{ eapply qpres in hfix. now depelim hfix. }
rewrite /cunfold_cofix.
destruct nth_error eqn:hnth ⇒ //.
pose proof (nth_error_Some_length hnth).
epose proof (Qcofix_subst _ _ hasfix qfix qpres idx H hfix).
intros [= <-]. subst fn.
eapply Hs. rewrite cofix_subst_length //.
eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a.
assumption.
Qed.
Class Qconst Σ (Q : nat → term → Type) := qconst :
∀ kn decl, declared_constant Σ kn decl →
match cst_body decl with
| None ⇒ unit
| Some b ⇒ Q 0 b
end.
#[export] Hint Mode Qconst - ! : typeclass_instances.
Class Qpreserves {etfl : ETermFlags} (Q : nat → term → Type) Σ :=
{ qpres_qpres :: Qpres Q;
qpres_qcons :: Qconst Σ Q;
qpres_qapp :: Qapp Q;
qpres_qcase :: Qcase Q;
qpres_qproj :: Qproj Q;
qpres_qsubst :: Qsubst Q;
qpres_qfix :: Qfix Q;
qpres_qcofix :: Qcofix Q }.
Lemma eval_preserve_mkApps_ind :
∀ (wfl : WcbvFlags), with_constructor_as_block = true → ∀ {efl : EEnvFlags} (Σ : global_declarations)
(P' : term → term → Type)
(Q : nat → term → Type)
{Qpres : Qpreserves Q Σ}
(P := (fun x y ⇒ [× P' x y, Q 0 x & Q 0 y])%type)
(HPQ : ∀ t u, eval Σ t u → Q 0 t → P' t u → Q 0 u),
wf_glob Σ →
has_tApp →
(∀ (a t t' : term),
eval Σ a tBox →
P a tBox →
eval Σ t t' → P t t' → P' (tApp a t) tBox) →
(∀ (f0 : term) (na : name) (b a a' res : term),
eval Σ f0 (tLambda na b) →
P f0 (tLambda na b)
→ eval Σ a a'
→ P a a'
→ eval Σ (ECSubst.csubst a' 0 b) res
→ P (ECSubst.csubst a' 0 b) res → P' (tApp f0 a) res)
→ (∀ (na : name) (b0 b0' b1 res : term),
eval Σ b0 b0'
→ P b0 b0'
→ Q 1 b1
→ eval Σ (ECSubst.csubst b0' 0 b1) res
→ P (ECSubst.csubst b0' 0 b1) res →
P' (tLetIn na b0 b1) res)
→ (∀ (ind : inductive) (pars : nat) cdecl (discr : term)
(c : nat) (args : list term) (brs :
list
(list name × term))
(br : list name × term) (res : term),
eval Σ discr (tConstruct ind c args)
→ P discr (tConstruct ind c args)
→ constructor_isprop_pars_decl Σ ind c = Some (false, pars, cdecl)
→ nth_error brs c = Some br
→ #|args| = pars + cdecl.(cstr_nargs)
→ #|skipn pars args| = #|br.1|
→ Q #|br.1| br.2
→ eval Σ (iota_red pars args br) res
→ P (iota_red pars args br) res
→ P' (tCase (ind, pars) discr brs) res)
→ (∀ (ind : inductive) (pars : nat) (discr : term)
(brs : list (list name × term))
(n : list name) (f3 res : term),
with_prop_case
→ eval Σ discr tBox
→ P discr tBox
→ inductive_isprop_and_pars Σ ind = Some (true, pars)
→ brs = [(n, f3)]
→ Q #|n| f3
→ eval Σ (ECSubst.substl (repeat tBox #|n|) f3)
res
→ P (ECSubst.substl (repeat tBox #|n|) f3) res
→ P' (tCase (ind, pars) discr brs) res)
→ (∀ (f4 : term) (mfix : mfixpoint term)
(idx : nat) (argsv : list term)
(a av fn res : term),
with_guarded_fix →
eval Σ f4 (mkApps (tFix mfix idx) argsv)
→ P f4 (mkApps (tFix mfix idx) argsv)
→ eval Σ a av
→ P a av
→ cunfold_fix mfix idx = Some (#|argsv|, fn)
→ Q 0 fn
→ eval Σ (tApp (mkApps fn argsv) av) res
→ P (tApp (mkApps fn argsv) av) res
→ P' (tApp f4 a) res)
→ (∀ (f5 : term) (mfix : mfixpoint term)
(idx : nat) (argsv : list term)
(a av : term) (narg : nat) (fn : term),
with_guarded_fix →
eval Σ f5 (mkApps (tFix mfix idx) argsv)
→ P f5 (mkApps (tFix mfix idx) argsv)
→ eval Σ a av
→ P a av
→ cunfold_fix mfix idx = Some (narg, fn)
→ #|argsv| < narg
→ P' (tApp f5 a)
(tApp
(mkApps (tFix mfix idx) argsv) av))
→ (∀ (f5 : term) (mfix : mfixpoint term)
(idx : nat) (a av : term) (narg : nat) (fn : term) res,
with_guarded_fix = false →
eval Σ f5 (tFix mfix idx)
→ P f5 (tFix mfix idx)
→ cunfold_fix mfix idx = Some (narg, fn)
→ eval Σ a av → P a av
→ eval Σ (tApp fn av) res
→ P (tApp fn av) res
→ P' (tApp f5 a) res) →
(∀ (ip : inductive × nat) (mfix : mfixpoint term)
(idx : nat) (args : list term)
(narg : nat) discr (fn : term) (brs :
list
(list name × term))
(res : term),
cunfold_cofix mfix idx = Some (narg, fn)
→ eval Σ discr (mkApps (tCoFix mfix idx) args)
→ P discr (mkApps (tCoFix mfix idx) args)
→ eval Σ (tCase ip (mkApps fn args) brs) res
→ P (tCase ip (mkApps fn args) brs) res
→ P'
(tCase ip discr brs)
res)
→ (∀ (p : projection) (mfix : mfixpoint term)
(idx : nat) (args : list term)
(narg : nat) discr (fn res : term),
has_tProj →
cunfold_cofix mfix idx = Some (narg, fn)
→ eval Σ discr (mkApps (tCoFix mfix idx) args)
→ P discr (mkApps (tCoFix mfix idx) args)
→ eval Σ (tProj p (mkApps fn args)) res
→ P (tProj p (mkApps fn args)) res
→ P'
(tProj p discr) res)
→ (∀ (c : kername) (decl : constant_body)
(body : term),
declared_constant Σ c decl
→ ∀ res : term,
cst_body decl = Some body
→ eval Σ body res
→ P body res → P' (tConst c) res)
→ (∀ p cdecl (discr : term) (args : list term) a (res : term),
has_tProj →
eval Σ discr (tConstruct p.(proj_ind) 0 args)
→ P discr (tConstruct p.(proj_ind) 0 args)
→ constructor_isprop_pars_decl Σ p.(proj_ind) 0 = Some (false, p.(proj_npars), cdecl)
→ #|args| = p.(proj_npars) + cdecl.(cstr_nargs)
→ nth_error args (p.(proj_npars) + p.(proj_arg)) = Some a
→ eval Σ a res
→ P a res
→ P' (tProj p discr) res)
→ (∀ p (discr : term),
has_tProj →
with_prop_case
→ eval Σ discr tBox
→ P discr tBox
→ inductive_isprop_and_pars Σ p.(proj_ind) = Some (true, p.(proj_npars))
→ P' (tProj p discr) tBox) →
(∀ (f11 f' : term) a a',
∀ (ev : eval Σ f11 f'),
P f11 f' →
(∀ t u (ev' : eval Σ t u), eval_depth ev' ≤ eval_depth ev → Q 0 t → P t u) →
~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
|| isConstructApp f' || isPrimApp f' || isLazyApp f') →
eval Σ a a' → P a a' →
P' (tApp f11 a) (tApp f' a')) →
(∀ ind i mdecl idecl cdecl args args',
lookup_constructor Σ ind i = Some (mdecl, idecl, cdecl) →
#|args| = cstr_arity mdecl cdecl →
All2 (eval Σ) args args' →
All2 P args args' →
P' (tConstruct ind i args) (tConstruct ind i args')) →
(∀ p p' (ev : eval_primitive (eval Σ) p p'),
Q 0 (tPrim p) →
eval_primitive_ind _ (fun x y _ ⇒ P x y) _ _ ev →
P' (tPrim p) (tPrim p')) →
(∀ t t' v, eval Σ t (tLazy t') → eval Σ t' v →
P t (tLazy t') →
P t' v →
P' (tForce t) v) →
(∀ t : term, atom Σ t → Q 0 t → P' t t) →
∀ (t t0 : term), Q 0 t → eval Σ t t0 → P' t t0.
Proof.
intros wfl hcon. intros × Qpres P P'Q wfΣ hasapp.
assert (qfixs: Qfixs Q) by tc.
assert (qcofixs: Qcofixs Q) by tc.
intros.
pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
specialize (p (MR lt (fun x ⇒ eval_depth x.π2.π2.π2))).
set(foo := existT _ t (existT _ t0 (existT _ X17 H)) : { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
change t with (projT1 foo).
change t0 with (projT1 (projT2 foo)).
revert foo.
match goal with
|- let foo := _ in @?P foo ⇒ specialize (p (fun x ⇒ P x))
end.
forward p.
2:{ apply p. apply measure_wf, lt_wf. }
clear p.
rename X17 into qt. rename X13 into Xcappexp.
rename X14 into Qprim, X15 into Qforce, X16 into Qatom.
clear t t0 qt H.
intros (t & t0 & qt & ev).
intros IH.
set (IH' t t0 q H := IH (t; t0; q; H)). clearbody IH'; clear IH; rename IH' into IH.
cbn in IH. unfold MR in IH; cbn in IH. cbn.
Ltac ih :=
match goal with
[ IH : ∀ x y, ?Q 0 x → _ |- _ ] ⇒ unshelve eapply IH; tea; cbn; try lia
end.
Ltac hp' P'Q := intros ?; repeat split ⇒ //; try eapply P'Q; tea.
assert (and_assum : ∀ x y, P' x y →
((P' x y) → Q 0 x × Q 0 y) →
P x y).
{ intuition auto. red. intuition auto. }
Ltac ih' P'Q :=
match goal with
| [ H : _, IH : ∀ x y, ?Q 0 x → _ |- _ ] ⇒
eapply H; tea; (apply and_assum; [ih|hp' P'Q])
end.
Ltac myt hyp anda P'Q := eapply hyp; tea; (apply and_assum; [ih|hp' P'Q]).
destruct ev.
1-19:eapply qpres in qt as qt'; depelim qt' ⇒ //.
all:try congruence.
- eapply X; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (ql : Q 0 (tLambda na b)).
{ eapply P'Q; tea. ih. }
assert (qs: Q 0 (csubst a' 0 b)).
{ eapply qpres in ql. depelim ql ⇒ //.
eapply (qsubst b [a']) in q1. now cbn in q1.
repeat constructor.
eapply P'Q; tea; ih. }
eapply X0; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (qs : Q 0 (csubst b0' 0 b1)).
{ eapply (qsubst b1 [b0']) in q0. now cbn in q0.
repeat constructor.
eapply P'Q; tea; ih. }
eapply X1; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 (iota_red pars args br)).
{ unfold iota_red.
eapply nth_error_all in a; tea. cbn in a.
rewrite -e3 in a.
rewrite -(List.length_rev (skipn pars args)) in a.
rewrite Nat.add_0_r in a.
eapply (qsubst _ (List.rev (skipn pars args))) in a.
2:{ eapply All_rev, All_skipn.
assert (Q 0 (tConstruct ind c args)).
eapply P'Q; tea; ih. eapply qpres in X13.
depelim X13 ⇒ //. }
exact a. }
eapply nth_error_all in a; tea; cbn. rewrite Nat.add_0_r in a.
eapply X2; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 (substl (repeat tBox #|n|) f)).
{ subst brs. eapply All_tip in a. cbn in a.
rewrite -(repeat_length tBox #|n|) Nat.add_0_r in a.
eapply (qsubst _ (repeat tBox #|n|)) in a ⇒ //.
eapply All_repeat. eapply P'Q; tea; ih. }
eapply X3; tea. 1,3:(apply and_assum; [ih|hp' P'Q]).
subst brs. depelim a. now rewrite Nat.add_0_r in q0.
- pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //. 2:{ clear ev1'; ih. }
eapply qapp in ev1' as [hfix qargs] ⇒ //.
assert (hastfix : has_tFix).
{ eapply qpres in hfix. now depelim hfix. }
assert (qf : Q 0 fn).
{ eapply (qfixs mfix idx) in hfix; tea. }
assert (qa : Q 0 (tApp (mkApps fn argsv) av)).
{ rewrite -[tApp _ _](mkApps_app _ _ [av]).
unshelve eapply (qapp _ _ _ _).2; auto.
split ⇒ //.
eapply (qfixs mfix idx) in hfix; tea.
eapply All_app_inv ⇒ //. eapply All_tip.1.
eapply P'Q; tea; ih. }
eapply X4; tea. 1-3:(apply and_assum; [ih|hp' P'Q]).
- eapply X5; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (qav : Q 0 av).
{ eapply P'Q; tea; ih. }
assert (qa : Q 0 (tApp fn av)).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //. 2:clear ev1'; ih.
eapply qfixs in ev1'. cbn in IH. eapply ev1' in e.
unshelve eapply (qapp _ _ _ [av]); tea; split ⇒ //. now eapply All_tip.1. }
eapply X6; tea. 1-3:(apply and_assum; [ih|hp' P'Q]).
- assert (qa : Q 0 (tCase ip (mkApps fn args) brs)).
{ eapply qcase; tea ⇒ //.
pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qapp in ev1' as [hfix qargs] ⇒ //.
eapply qapp ⇒ //. split ⇒ //.
eapply (qcofixs mfix idx) in hfix; tea.
clear ev1'; ih. }
eapply X7; tea; (apply and_assum; [ih|hp' P'Q]).
- cbn in IH.
assert (qa : Q 0 (tProj p (mkApps fn args))).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qapp in ev1' as [hfix ?] ⇒ //.
eapply qproj; tea ⇒ //. eapply qapp ⇒ //. split ⇒ //.
eapply (qcofixs mfix idx) in hfix; tea.
clear ev1'; ih. }
eapply X8; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 body).
{ cbn in IH; eapply (qconst (Q:=Q)) in isdecl. now rewrite e in isdecl. }
eapply X9; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 a).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qpres in ev1'; depelim ev1' ⇒ //.
{ eapply nth_error_all in a0; tea. }
clear ev1'; ih. }
eapply X10; tea; (apply and_assum; [ih|hp' P'Q]).
- unshelve eapply X11; tea; try (intros; apply and_assum; [ih|hp' P'Q]).
- rename args into cargs.
eapply Xcappexp; tea. eauto.
cbn in IH.
clear -P'Q IH a a0 and_assum.
revert a0; induction a; constructor; auto. depelim a0.
apply and_assum; [ih|hp' P'Q].
eapply IHa. cbn. intros. eapply (IH _ _ q H). cbn. lia.
now depelim a0.
- eapply (X12 _ _ _ _ ev1); tea.
1,3:(apply and_assum; [ih|hp' P'Q]).
intros. apply and_assum; [ih|hp' P'Q].
- unshelve eapply Qprim; tea. depelim e.
× constructor.
× constructor.
× constructor.
× eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto.
+ apply All2_over_undep. cbn in IH.
depelim p0. destruct p.
clear -ev IH a0 P'Q and_assum. cbn in a0. subst a; cbn in ×.
induction ev; constructor; eauto.
** depelim a0.
eapply and_assum. unshelve eapply IH; tea. cbn. lia.
intros. split ⇒ //. eapply P'Q; tea.
** depelim a0. intuition eauto. eapply X; intros.
unshelve eapply IH; tea. cbn; lia.
+ depelim p0. destruct p.
eapply and_assum. unshelve eapply IH; tea. cbn; lia.
intros; split ⇒ //; eapply P'Q; tea.
- eapply qpres in qt; depelim qt ⇒ //.
assert (Q 0 (tLazy v)).
{ eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
eapply qpres in X13. depelim X13 ⇒ //.
eapply Qforce; tea.
+ eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
intros hp'. split ⇒ //. eapply P'Q; tea.
+ eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
intros hp'. split ⇒ //. eapply P'Q; tea.
- eapply Qatom; tea.
Qed.
Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ : wf_glob Σ → Qpreserves (fun n x ⇒ wellformed Σ n x) Σ.
Proof.
intros clΣ.
split.
- red. move⇒ n t.
destruct t; cbn -[lookup_constructor lookup_constructor_pars_args]; intuition auto; try solve [constructor; auto].
rtoProp; intuition auto.
constructor ⇒ //.
eapply on_evar; rtoProp; intuition auto. solve_all.
eapply on_lambda;rtoProp; intuition auto.
eapply on_letin; rtoProp; intuition auto.
eapply on_app; rtoProp; intuition auto.
constructor ⇒ //; rtoProp; intuition auto.
move/andP: H ⇒ [] /andP[] has isl hf ⇒ //.
eapply on_cstr ⇒ //. destruct cstr_as_blocks.
rtoProp; intuition auto. solve_all. destruct args ⇒ //.
eapply on_case; rtoProp; intuition auto. solve_all.
eapply on_proj; rtoProp; intuition auto.
rtoProp; intuition auto.
eapply on_fix ⇒ //. move/andP: H0 ⇒ [] _ ha. solve_all.
rtoProp; intuition auto.
eapply on_cofix ⇒ //. move/andP: H0 ⇒ [] _ ha. solve_all.
move/andP: H ⇒ [] hasp ht. eapply on_prim ⇒ //. solve_all.
eapply on_lazy; rtoProp; intuition auto.
eapply on_force; rtoProp; intuition auto.
- red. intros kn decl.
move/(lookup_env_wellformed clΣ).
unfold wf_global_decl. destruct cst_body ⇒ //.
- red. move⇒ hasapp n t args. rewrite wellformed_mkApps //.
split; intros; rtoProp; intuition auto; solve_all.
- red.
move⇒ hascase n ci discr brs. simpl.
rewrite /wf_brs.
destruct lookup_inductive eqn:hl ⇒ /= //.
intros; rtoProp; intuition auto; solve_all.
- red. simpl. move⇒ hasproj n p discr wf discr' wf'.
simpl. rtoProp; intuition auto.
- red. move⇒ t args clt cll.
eapply wellformed_substl. solve_all. now rewrite Nat.add_0_r.
- red. move⇒ n mfix idx. cbn. unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all. now apply Nat.ltb_lt.
- red. move⇒ n mfix idx. cbn. unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all. now apply Nat.ltb_lt.
Qed.
From Stdlib Require Import Utf8 Program ssreflect ssrbool.
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config Kernames BasicAst EnvMap.
From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
Set Asymmetric Patterns.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
#[export]
Hint Constructors eval : core.
Definition atomic_term (t : term) :=
match t with
| tBox | tConst _ | tRel _ | tVar _ | tPrim _ ⇒ true
| _ ⇒ false
end.
Definition has_atom {etfl : ETermFlags} (t : term) :=
match t with
| tBox ⇒ has_tBox
| tConst _ ⇒ has_tConst
| tRel _ ⇒ has_tRel
| tVar _ ⇒ has_tVar
| _ ⇒ false
end.
Section OnSubterm.
Context {etfl : ETermFlags}.
Inductive on_subterms (Q : nat → term → Type) (n : nat) : term → Type :=
| on_atom t : has_atom t → atomic_term t → on_subterms Q n t
| on_evar k l : has_tEvar → All (Q n) l → on_subterms Q n (tEvar k l)
| on_lambda na t : has_tLambda → Q (S n) t → on_subterms Q n (tLambda na t)
| on_letin na t u : has_tLetIn → Q n t → Q (S n) u → on_subterms Q n (tLetIn na t u)
| on_app f u : has_tApp → Q n f → Q n u → on_subterms Q n (tApp f u)
| on_cstr i k args : has_tConstruct → All (Q n) args → on_subterms Q n (tConstruct i k args)
| on_case ci discr brs : has_tCase → Q n discr →
All (fun br ⇒ Q (#|br.1| + n) br.2) brs → on_subterms Q n (tCase ci discr brs)
| on_proj p c : has_tProj → Q n c → on_subterms Q n (tProj p c)
| on_fix mfix idx : has_tFix → All (fun d ⇒ Q (#|mfix| + n) d.(dbody)) mfix → on_subterms Q n (tFix mfix idx)
| on_cofix mfix idx : has_tCoFix → All (fun d ⇒ Q (#|mfix| + n) d.(dbody)) mfix → on_subterms Q n (tCoFix mfix idx)
| on_prim p : has_prim p → primProp (Q n) p → on_subterms Q n (tPrim p)
| on_lazy t : has_tLazy_Force → Q n t → on_subterms Q n (tLazy t)
| on_force t : has_tLazy_Force → Q n t → on_subterms Q n (tForce t).
Derive Signature for on_subterms.
End OnSubterm.
Class Qpres {etfl : ETermFlags} (Q : nat → term → Type) := qpres : ∀ n t, Q n t → on_subterms Q n t.
#[export] Hint Mode Qpres - ! : typeclass_instances.
Class Qapp {etfl : ETermFlags} (Q : nat → term → Type) := qapp : has_tApp → ∀ n f args, Q n (mkApps f args) <~> Q n f × All (Q n) args.
#[export] Hint Mode Qapp - ! : typeclass_instances.
Class Qcase {etfl : ETermFlags} (Q : nat → term → Type) := qcase : has_tCase →
∀ n ci discr brs, Q n (tCase ci discr brs) → ∀ discr', Q n discr' → Q n (tCase ci discr' brs).
#[export] Hint Mode Qcase - ! : typeclass_instances.
(* Class Qcstr {etfl : ETermFlags} (Q : nat -> term -> Type) := *)
(* qcstr : has_tConstruct -> forall i n args, Q n (tConstruct i n args) Q n discr × All (fun br => Q (|br.1| + n) br.2) brs. *)
(* [export] Hint Mode Qcase - ! : typeclass_instances. *)
Class Qproj {etfl : ETermFlags} (Q : nat → term → Type) := qproj : has_tProj → ∀ n p discr, Q n (tProj p discr) → ∀ discr', Q n discr' → Q n (tProj p discr').
#[export] Hint Mode Qproj - ! : typeclass_instances.
Class Qfix {etfl : ETermFlags} (Q : nat → term → Type) := qfix : has_tFix → ∀ n mfix idx, idx < #|mfix| → Q n (tFix mfix idx) → ∀ idx', idx' < #|mfix| → Q n (tFix mfix idx').
#[export] Hint Mode Qfix - ! : typeclass_instances.
Class Qcofix {etfl : ETermFlags} (Q : nat → term → Type) := qcofix : has_tCoFix → ∀ n mfix idx, idx < #|mfix| → Q n (tCoFix mfix idx) → ∀ idx', idx' < #|mfix| → Q n (tCoFix mfix idx').
#[export] Hint Mode Qcofix - ! : typeclass_instances.
Class Qsubst (Q : nat → term → Type) := qsubst : ∀ t l, Q (#|l|) t → All (Q 0) l → Q 0 (substl l t).
#[export] Hint Mode Qsubst ! : typeclass_instances.
Class Qfixs (Q : nat → term → Type) := qfixs : ∀ mfix idx, Q 0 (tFix mfix idx) →
∀ args fn, cunfold_fix mfix idx = Some (args, fn) →
Q 0 fn.
#[export] Hint Mode Qfixs ! : typeclass_instances.
Class Qcofixs (Q : nat → term → Type) := qcofixs : ∀ mfix idx, Q 0 (tCoFix mfix idx) →
∀ args fn, cunfold_cofix mfix idx = Some (args, fn) →
Q 0 fn.
#[export] Hint Mode Qcofixs ! : typeclass_instances.
Lemma Qfix_subst {etfl : ETermFlags} mfix Q : has_tFix → Qfix Q → Qpres Q → ∀ idx, idx < #|mfix| → Q 0 (tFix mfix idx) → All (Q 0) (fix_subst mfix).
Proof.
intros hasfix qfix qpre; unfold fix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
induction n. intros. constructor; auto.
intros. constructor. eapply qfix ⇒ //. 2:tea. tea.
eapply IHn. lia. 2:tea. assumption.
Qed.
Lemma Qcofix_subst {etfl : ETermFlags} mfix Q : has_tCoFix → Qcofix Q → Qpres Q → ∀ idx, idx < #|mfix| → Q 0 (tCoFix mfix idx) → All (Q 0) (cofix_subst mfix).
Proof.
intros hascofix qcofix qpre; unfold cofix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
induction n. intros. constructor; auto.
intros. constructor. eapply qcofix ⇒ //. 2:tea. tea.
eapply IHn. lia. 2:tea. assumption.
Qed.
#[export] Instance Qsubst_Qfixs {etfl : ETermFlags} Q : Qpres Q → Qfix Q → Qsubst Q → Qfixs Q.
Proof.
move⇒ qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tFix).
{ eapply qpres in hfix. now depelim hfix. }
rewrite /cunfold_fix.
destruct nth_error eqn:hnth ⇒ //.
pose proof (nth_error_Some_length hnth).
epose proof (Qfix_subst _ _ hasfix qfix qpres idx H hfix).
intros [= <-]. subst fn.
eapply Hs. rewrite fix_subst_length //.
eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a.
assumption.
Qed.
#[export] Instance Qsubst_Qcofixs {etfl : ETermFlags} Q : Qpres Q → Qcofix Q → Qsubst Q → Qcofixs Q.
Proof.
move⇒ qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tCoFix).
{ eapply qpres in hfix. now depelim hfix. }
rewrite /cunfold_cofix.
destruct nth_error eqn:hnth ⇒ //.
pose proof (nth_error_Some_length hnth).
epose proof (Qcofix_subst _ _ hasfix qfix qpres idx H hfix).
intros [= <-]. subst fn.
eapply Hs. rewrite cofix_subst_length //.
eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a.
assumption.
Qed.
Class Qconst Σ (Q : nat → term → Type) := qconst :
∀ kn decl, declared_constant Σ kn decl →
match cst_body decl with
| None ⇒ unit
| Some b ⇒ Q 0 b
end.
#[export] Hint Mode Qconst - ! : typeclass_instances.
Class Qpreserves {etfl : ETermFlags} (Q : nat → term → Type) Σ :=
{ qpres_qpres :: Qpres Q;
qpres_qcons :: Qconst Σ Q;
qpres_qapp :: Qapp Q;
qpres_qcase :: Qcase Q;
qpres_qproj :: Qproj Q;
qpres_qsubst :: Qsubst Q;
qpres_qfix :: Qfix Q;
qpres_qcofix :: Qcofix Q }.
Lemma eval_preserve_mkApps_ind :
∀ (wfl : WcbvFlags), with_constructor_as_block = true → ∀ {efl : EEnvFlags} (Σ : global_declarations)
(P' : term → term → Type)
(Q : nat → term → Type)
{Qpres : Qpreserves Q Σ}
(P := (fun x y ⇒ [× P' x y, Q 0 x & Q 0 y])%type)
(HPQ : ∀ t u, eval Σ t u → Q 0 t → P' t u → Q 0 u),
wf_glob Σ →
has_tApp →
(∀ (a t t' : term),
eval Σ a tBox →
P a tBox →
eval Σ t t' → P t t' → P' (tApp a t) tBox) →
(∀ (f0 : term) (na : name) (b a a' res : term),
eval Σ f0 (tLambda na b) →
P f0 (tLambda na b)
→ eval Σ a a'
→ P a a'
→ eval Σ (ECSubst.csubst a' 0 b) res
→ P (ECSubst.csubst a' 0 b) res → P' (tApp f0 a) res)
→ (∀ (na : name) (b0 b0' b1 res : term),
eval Σ b0 b0'
→ P b0 b0'
→ Q 1 b1
→ eval Σ (ECSubst.csubst b0' 0 b1) res
→ P (ECSubst.csubst b0' 0 b1) res →
P' (tLetIn na b0 b1) res)
→ (∀ (ind : inductive) (pars : nat) cdecl (discr : term)
(c : nat) (args : list term) (brs :
list
(list name × term))
(br : list name × term) (res : term),
eval Σ discr (tConstruct ind c args)
→ P discr (tConstruct ind c args)
→ constructor_isprop_pars_decl Σ ind c = Some (false, pars, cdecl)
→ nth_error brs c = Some br
→ #|args| = pars + cdecl.(cstr_nargs)
→ #|skipn pars args| = #|br.1|
→ Q #|br.1| br.2
→ eval Σ (iota_red pars args br) res
→ P (iota_red pars args br) res
→ P' (tCase (ind, pars) discr brs) res)
→ (∀ (ind : inductive) (pars : nat) (discr : term)
(brs : list (list name × term))
(n : list name) (f3 res : term),
with_prop_case
→ eval Σ discr tBox
→ P discr tBox
→ inductive_isprop_and_pars Σ ind = Some (true, pars)
→ brs = [(n, f3)]
→ Q #|n| f3
→ eval Σ (ECSubst.substl (repeat tBox #|n|) f3)
res
→ P (ECSubst.substl (repeat tBox #|n|) f3) res
→ P' (tCase (ind, pars) discr brs) res)
→ (∀ (f4 : term) (mfix : mfixpoint term)
(idx : nat) (argsv : list term)
(a av fn res : term),
with_guarded_fix →
eval Σ f4 (mkApps (tFix mfix idx) argsv)
→ P f4 (mkApps (tFix mfix idx) argsv)
→ eval Σ a av
→ P a av
→ cunfold_fix mfix idx = Some (#|argsv|, fn)
→ Q 0 fn
→ eval Σ (tApp (mkApps fn argsv) av) res
→ P (tApp (mkApps fn argsv) av) res
→ P' (tApp f4 a) res)
→ (∀ (f5 : term) (mfix : mfixpoint term)
(idx : nat) (argsv : list term)
(a av : term) (narg : nat) (fn : term),
with_guarded_fix →
eval Σ f5 (mkApps (tFix mfix idx) argsv)
→ P f5 (mkApps (tFix mfix idx) argsv)
→ eval Σ a av
→ P a av
→ cunfold_fix mfix idx = Some (narg, fn)
→ #|argsv| < narg
→ P' (tApp f5 a)
(tApp
(mkApps (tFix mfix idx) argsv) av))
→ (∀ (f5 : term) (mfix : mfixpoint term)
(idx : nat) (a av : term) (narg : nat) (fn : term) res,
with_guarded_fix = false →
eval Σ f5 (tFix mfix idx)
→ P f5 (tFix mfix idx)
→ cunfold_fix mfix idx = Some (narg, fn)
→ eval Σ a av → P a av
→ eval Σ (tApp fn av) res
→ P (tApp fn av) res
→ P' (tApp f5 a) res) →
(∀ (ip : inductive × nat) (mfix : mfixpoint term)
(idx : nat) (args : list term)
(narg : nat) discr (fn : term) (brs :
list
(list name × term))
(res : term),
cunfold_cofix mfix idx = Some (narg, fn)
→ eval Σ discr (mkApps (tCoFix mfix idx) args)
→ P discr (mkApps (tCoFix mfix idx) args)
→ eval Σ (tCase ip (mkApps fn args) brs) res
→ P (tCase ip (mkApps fn args) brs) res
→ P'
(tCase ip discr brs)
res)
→ (∀ (p : projection) (mfix : mfixpoint term)
(idx : nat) (args : list term)
(narg : nat) discr (fn res : term),
has_tProj →
cunfold_cofix mfix idx = Some (narg, fn)
→ eval Σ discr (mkApps (tCoFix mfix idx) args)
→ P discr (mkApps (tCoFix mfix idx) args)
→ eval Σ (tProj p (mkApps fn args)) res
→ P (tProj p (mkApps fn args)) res
→ P'
(tProj p discr) res)
→ (∀ (c : kername) (decl : constant_body)
(body : term),
declared_constant Σ c decl
→ ∀ res : term,
cst_body decl = Some body
→ eval Σ body res
→ P body res → P' (tConst c) res)
→ (∀ p cdecl (discr : term) (args : list term) a (res : term),
has_tProj →
eval Σ discr (tConstruct p.(proj_ind) 0 args)
→ P discr (tConstruct p.(proj_ind) 0 args)
→ constructor_isprop_pars_decl Σ p.(proj_ind) 0 = Some (false, p.(proj_npars), cdecl)
→ #|args| = p.(proj_npars) + cdecl.(cstr_nargs)
→ nth_error args (p.(proj_npars) + p.(proj_arg)) = Some a
→ eval Σ a res
→ P a res
→ P' (tProj p discr) res)
→ (∀ p (discr : term),
has_tProj →
with_prop_case
→ eval Σ discr tBox
→ P discr tBox
→ inductive_isprop_and_pars Σ p.(proj_ind) = Some (true, p.(proj_npars))
→ P' (tProj p discr) tBox) →
(∀ (f11 f' : term) a a',
∀ (ev : eval Σ f11 f'),
P f11 f' →
(∀ t u (ev' : eval Σ t u), eval_depth ev' ≤ eval_depth ev → Q 0 t → P t u) →
~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
|| isConstructApp f' || isPrimApp f' || isLazyApp f') →
eval Σ a a' → P a a' →
P' (tApp f11 a) (tApp f' a')) →
(∀ ind i mdecl idecl cdecl args args',
lookup_constructor Σ ind i = Some (mdecl, idecl, cdecl) →
#|args| = cstr_arity mdecl cdecl →
All2 (eval Σ) args args' →
All2 P args args' →
P' (tConstruct ind i args) (tConstruct ind i args')) →
(∀ p p' (ev : eval_primitive (eval Σ) p p'),
Q 0 (tPrim p) →
eval_primitive_ind _ (fun x y _ ⇒ P x y) _ _ ev →
P' (tPrim p) (tPrim p')) →
(∀ t t' v, eval Σ t (tLazy t') → eval Σ t' v →
P t (tLazy t') →
P t' v →
P' (tForce t) v) →
(∀ t : term, atom Σ t → Q 0 t → P' t t) →
∀ (t t0 : term), Q 0 t → eval Σ t t0 → P' t t0.
Proof.
intros wfl hcon. intros × Qpres P P'Q wfΣ hasapp.
assert (qfixs: Qfixs Q) by tc.
assert (qcofixs: Qcofixs Q) by tc.
intros.
pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
specialize (p (MR lt (fun x ⇒ eval_depth x.π2.π2.π2))).
set(foo := existT _ t (existT _ t0 (existT _ X17 H)) : { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
change t with (projT1 foo).
change t0 with (projT1 (projT2 foo)).
revert foo.
match goal with
|- let foo := _ in @?P foo ⇒ specialize (p (fun x ⇒ P x))
end.
forward p.
2:{ apply p. apply measure_wf, lt_wf. }
clear p.
rename X17 into qt. rename X13 into Xcappexp.
rename X14 into Qprim, X15 into Qforce, X16 into Qatom.
clear t t0 qt H.
intros (t & t0 & qt & ev).
intros IH.
set (IH' t t0 q H := IH (t; t0; q; H)). clearbody IH'; clear IH; rename IH' into IH.
cbn in IH. unfold MR in IH; cbn in IH. cbn.
Ltac ih :=
match goal with
[ IH : ∀ x y, ?Q 0 x → _ |- _ ] ⇒ unshelve eapply IH; tea; cbn; try lia
end.
Ltac hp' P'Q := intros ?; repeat split ⇒ //; try eapply P'Q; tea.
assert (and_assum : ∀ x y, P' x y →
((P' x y) → Q 0 x × Q 0 y) →
P x y).
{ intuition auto. red. intuition auto. }
Ltac ih' P'Q :=
match goal with
| [ H : _, IH : ∀ x y, ?Q 0 x → _ |- _ ] ⇒
eapply H; tea; (apply and_assum; [ih|hp' P'Q])
end.
Ltac myt hyp anda P'Q := eapply hyp; tea; (apply and_assum; [ih|hp' P'Q]).
destruct ev.
1-19:eapply qpres in qt as qt'; depelim qt' ⇒ //.
all:try congruence.
- eapply X; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (ql : Q 0 (tLambda na b)).
{ eapply P'Q; tea. ih. }
assert (qs: Q 0 (csubst a' 0 b)).
{ eapply qpres in ql. depelim ql ⇒ //.
eapply (qsubst b [a']) in q1. now cbn in q1.
repeat constructor.
eapply P'Q; tea; ih. }
eapply X0; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (qs : Q 0 (csubst b0' 0 b1)).
{ eapply (qsubst b1 [b0']) in q0. now cbn in q0.
repeat constructor.
eapply P'Q; tea; ih. }
eapply X1; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 (iota_red pars args br)).
{ unfold iota_red.
eapply nth_error_all in a; tea. cbn in a.
rewrite -e3 in a.
rewrite -(List.length_rev (skipn pars args)) in a.
rewrite Nat.add_0_r in a.
eapply (qsubst _ (List.rev (skipn pars args))) in a.
2:{ eapply All_rev, All_skipn.
assert (Q 0 (tConstruct ind c args)).
eapply P'Q; tea; ih. eapply qpres in X13.
depelim X13 ⇒ //. }
exact a. }
eapply nth_error_all in a; tea; cbn. rewrite Nat.add_0_r in a.
eapply X2; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 (substl (repeat tBox #|n|) f)).
{ subst brs. eapply All_tip in a. cbn in a.
rewrite -(repeat_length tBox #|n|) Nat.add_0_r in a.
eapply (qsubst _ (repeat tBox #|n|)) in a ⇒ //.
eapply All_repeat. eapply P'Q; tea; ih. }
eapply X3; tea. 1,3:(apply and_assum; [ih|hp' P'Q]).
subst brs. depelim a. now rewrite Nat.add_0_r in q0.
- pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //. 2:{ clear ev1'; ih. }
eapply qapp in ev1' as [hfix qargs] ⇒ //.
assert (hastfix : has_tFix).
{ eapply qpres in hfix. now depelim hfix. }
assert (qf : Q 0 fn).
{ eapply (qfixs mfix idx) in hfix; tea. }
assert (qa : Q 0 (tApp (mkApps fn argsv) av)).
{ rewrite -[tApp _ _](mkApps_app _ _ [av]).
unshelve eapply (qapp _ _ _ _).2; auto.
split ⇒ //.
eapply (qfixs mfix idx) in hfix; tea.
eapply All_app_inv ⇒ //. eapply All_tip.1.
eapply P'Q; tea; ih. }
eapply X4; tea. 1-3:(apply and_assum; [ih|hp' P'Q]).
- eapply X5; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (qav : Q 0 av).
{ eapply P'Q; tea; ih. }
assert (qa : Q 0 (tApp fn av)).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //. 2:clear ev1'; ih.
eapply qfixs in ev1'. cbn in IH. eapply ev1' in e.
unshelve eapply (qapp _ _ _ [av]); tea; split ⇒ //. now eapply All_tip.1. }
eapply X6; tea. 1-3:(apply and_assum; [ih|hp' P'Q]).
- assert (qa : Q 0 (tCase ip (mkApps fn args) brs)).
{ eapply qcase; tea ⇒ //.
pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qapp in ev1' as [hfix qargs] ⇒ //.
eapply qapp ⇒ //. split ⇒ //.
eapply (qcofixs mfix idx) in hfix; tea.
clear ev1'; ih. }
eapply X7; tea; (apply and_assum; [ih|hp' P'Q]).
- cbn in IH.
assert (qa : Q 0 (tProj p (mkApps fn args))).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qapp in ev1' as [hfix ?] ⇒ //.
eapply qproj; tea ⇒ //. eapply qapp ⇒ //. split ⇒ //.
eapply (qcofixs mfix idx) in hfix; tea.
clear ev1'; ih. }
eapply X8; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 body).
{ cbn in IH; eapply (qconst (Q:=Q)) in isdecl. now rewrite e in isdecl. }
eapply X9; tea; (apply and_assum; [ih|hp' P'Q]).
- assert (Q 0 a).
{ pose proof (ev1' := ev1). eapply P'Q in ev1' ⇒ //.
eapply qpres in ev1'; depelim ev1' ⇒ //.
{ eapply nth_error_all in a0; tea. }
clear ev1'; ih. }
eapply X10; tea; (apply and_assum; [ih|hp' P'Q]).
- unshelve eapply X11; tea; try (intros; apply and_assum; [ih|hp' P'Q]).
- rename args into cargs.
eapply Xcappexp; tea. eauto.
cbn in IH.
clear -P'Q IH a a0 and_assum.
revert a0; induction a; constructor; auto. depelim a0.
apply and_assum; [ih|hp' P'Q].
eapply IHa. cbn. intros. eapply (IH _ _ q H). cbn. lia.
now depelim a0.
- eapply (X12 _ _ _ _ ev1); tea.
1,3:(apply and_assum; [ih|hp' P'Q]).
intros. apply and_assum; [ih|hp' P'Q].
- unshelve eapply Qprim; tea. depelim e.
× constructor.
× constructor.
× constructor.
× eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto.
+ apply All2_over_undep. cbn in IH.
depelim p0. destruct p.
clear -ev IH a0 P'Q and_assum. cbn in a0. subst a; cbn in ×.
induction ev; constructor; eauto.
** depelim a0.
eapply and_assum. unshelve eapply IH; tea. cbn. lia.
intros. split ⇒ //. eapply P'Q; tea.
** depelim a0. intuition eauto. eapply X; intros.
unshelve eapply IH; tea. cbn; lia.
+ depelim p0. destruct p.
eapply and_assum. unshelve eapply IH; tea. cbn; lia.
intros; split ⇒ //; eapply P'Q; tea.
- eapply qpres in qt; depelim qt ⇒ //.
assert (Q 0 (tLazy v)).
{ eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
eapply qpres in X13. depelim X13 ⇒ //.
eapply Qforce; tea.
+ eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
intros hp'. split ⇒ //. eapply P'Q; tea.
+ eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
intros hp'. split ⇒ //. eapply P'Q; tea.
- eapply Qatom; tea.
Qed.
Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ : wf_glob Σ → Qpreserves (fun n x ⇒ wellformed Σ n x) Σ.
Proof.
intros clΣ.
split.
- red. move⇒ n t.
destruct t; cbn -[lookup_constructor lookup_constructor_pars_args]; intuition auto; try solve [constructor; auto].
rtoProp; intuition auto.
constructor ⇒ //.
eapply on_evar; rtoProp; intuition auto. solve_all.
eapply on_lambda;rtoProp; intuition auto.
eapply on_letin; rtoProp; intuition auto.
eapply on_app; rtoProp; intuition auto.
constructor ⇒ //; rtoProp; intuition auto.
move/andP: H ⇒ [] /andP[] has isl hf ⇒ //.
eapply on_cstr ⇒ //. destruct cstr_as_blocks.
rtoProp; intuition auto. solve_all. destruct args ⇒ //.
eapply on_case; rtoProp; intuition auto. solve_all.
eapply on_proj; rtoProp; intuition auto.
rtoProp; intuition auto.
eapply on_fix ⇒ //. move/andP: H0 ⇒ [] _ ha. solve_all.
rtoProp; intuition auto.
eapply on_cofix ⇒ //. move/andP: H0 ⇒ [] _ ha. solve_all.
move/andP: H ⇒ [] hasp ht. eapply on_prim ⇒ //. solve_all.
eapply on_lazy; rtoProp; intuition auto.
eapply on_force; rtoProp; intuition auto.
- red. intros kn decl.
move/(lookup_env_wellformed clΣ).
unfold wf_global_decl. destruct cst_body ⇒ //.
- red. move⇒ hasapp n t args. rewrite wellformed_mkApps //.
split; intros; rtoProp; intuition auto; solve_all.
- red.
move⇒ hascase n ci discr brs. simpl.
rewrite /wf_brs.
destruct lookup_inductive eqn:hl ⇒ /= //.
intros; rtoProp; intuition auto; solve_all.
- red. simpl. move⇒ hasproj n p discr wf discr' wf'.
simpl. rtoProp; intuition auto.
- red. move⇒ t args clt cll.
eapply wellformed_substl. solve_all. now rewrite Nat.add_0_r.
- red. move⇒ n mfix idx. cbn. unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all. now apply Nat.ltb_lt.
- red. move⇒ n mfix idx. cbn. unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all. now apply Nat.ltb_lt.
Qed.