Timings for EWcbvEvalCstrsAsBlocksInd.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-metacoq-erasure.dev//./erasure/theories/EWcbvEvalCstrsAsBlocksInd.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-metacoq-erasure.dev//./erasure/theories/EWcbvEvalCstrsAsBlocksInd.v.timing
(* Distributed under the terms of the MIT license. *)
From Coq Require Import Utf8 Program ssreflect ssrbool.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
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.
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).
Derive Signature for on_subterms.
Class Qpres {etfl : ETermFlags} (Q : nat -> term -> Type) := qpres : forall 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 -> forall 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 ->
forall n ci discr brs, Q n (tCase ci discr brs) -> forall 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 -> forall n p discr, Q n (tProj p discr) -> forall 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 -> forall n mfix idx, idx < #|mfix| -> Q n (tFix mfix idx) -> forall 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 -> forall n mfix idx, idx < #|mfix| -> Q n (tCoFix mfix idx) -> forall idx', idx' < #|mfix| -> Q n (tCoFix mfix idx').
#[export] Hint Mode Qcofix - ! : typeclass_instances.
Class Qsubst (Q : nat -> term -> Type) := qsubst : forall 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 : forall mfix idx, Q 0 (tFix mfix idx) ->
forall 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 : forall mfix idx, Q 0 (tCoFix mfix idx) ->
forall 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 -> forall idx, idx < #|mfix| -> Q 0 (tFix mfix idx) -> All (Q 0) (fix_subst mfix).
intros hasfix qfix qpre; unfold fix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
Lemma Qcofix_subst {etfl : ETermFlags} mfix Q : has_tCoFix -> Qcofix Q -> Qpres Q -> forall idx, idx < #|mfix| -> Q 0 (tCoFix mfix idx) -> All (Q 0) (cofix_subst mfix).
intros hascofix qcofix qpre; unfold cofix_subst.
generalize (Nat.le_refl #|mfix|).
generalize #|mfix| at 1 4.
#[export] Instance Qsubst_Qfixs {etfl : ETermFlags} Q : Qpres Q -> Qfix Q -> Qsubst Q -> Qfixs Q.
move=> qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tFix).
destruct nth_error eqn:hnth => //.
pose proof (nth_error_Some_length hnth).
epose proof (Qfix_subst _ _ hasfix qfix qpres idx H hfix).
rewrite fix_subst_length //.
eapply nth_error_all in a; tea.
now rewrite Nat.add_0_r in a.
#[export] Instance Qsubst_Qcofixs {etfl : ETermFlags} Q : Qpres Q -> Qcofix Q -> Qsubst Q -> Qcofixs Q.
move=> qpres qfix; rewrite /Qsubst /Qfixs.
intros Hs mfix idx hfix args fn.
assert (hasfix : has_tCoFix).
destruct nth_error eqn:hnth => //.
pose proof (nth_error_Some_length hnth).
epose proof (Qcofix_subst _ _ hasfix qfix qpres idx H hfix).
rewrite cofix_subst_length //.
eapply nth_error_all in a; tea.
now rewrite Nat.add_0_r in a.
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.
Set Warnings "-future-coercion-class-field".
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 }.
Set Warnings "+future-coercion-class-field".
Lemma eval_preserve_mkApps_ind :
∀ (wfl : WcbvFlags), with_constructor_as_block = true -> forall {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',
forall (ev : eval Σ f11 f'),
P f11 f' ->
(forall 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') →
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')) →
(forall 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 : term, atom Σ t → Q 0 t -> P' t t) ->
∀ (t t0 : term), Q 0 t -> eval Σ t t0 → P' t t0.
intros * Qpres P P'Q wfΣ hasapp.
assert (qfixs: Qfixs Q) by tc.
assert (qcofixs: Qcofixs Q) by tc.
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 _ X16 H)) : { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
change t with (projT1 foo).
change t0 with (projT1 (projT2 foo)).
match goal with
|- let foo := _ in @?P foo => specialize (p (fun x => P x))
end.
rename X13 into Xcappexp.
rename X14 into Qprim, X15 into Qatom.
intros (t & t0 & qt & ev).
set (IH' t t0 q H := IH (t; t0; q; H)).
clearbody IH'; clear IH; rename IH' into IH.
unfold MR in IH; cbn in IH.
Ltac ih :=
match goal with
[ IH : forall 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 : forall x y, P' x y ->
((P' x y) -> Q 0 x × Q 0 y) ->
P x y).
Ltac ih' P'Q :=
match goal with
| [ H : _, IH : forall 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]).
1-18:eapply qpres in qt as qt'; depelim qt' => //.
eapply X; tea; (apply and_assum; [ih|hp' P'Q]).
assert (ql : Q 0 (tLambda na b)).
assert (qs: Q 0 (csubst a' 0 b)).
eapply (qsubst b [a']) in q1.
eapply X0; tea; (apply and_assum; [ih|hp' P'Q]).
assert (qs : Q 0 (csubst b0' 0 b1)).
eapply (qsubst b1 [b0']) in q0.
eapply X1; tea; (apply and_assum; [ih|hp' P'Q]).
assert (Q 0 (iota_red pars args br)).
eapply nth_error_all in a; tea.
rewrite -(List.rev_length (skipn pars args)) in a.
rewrite Nat.add_0_r in a.
eapply (qsubst _ (List.rev (skipn pars args))) in a.
eapply All_rev, All_skipn.
assert (Q 0 (tConstruct ind c args)).
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)).
rewrite -(repeat_length tBox #|n|) Nat.add_0_r in a.
eapply (qsubst _ (repeat tBox #|n|)) in a => //.
1,3:(apply and_assum; [ih|hp' P'Q]).
now rewrite Nat.add_0_r in q0.
pose proof (ev1' := ev1).
eapply P'Q in ev1' => //.
eapply qapp in ev1' as [hfix qargs] => //.
assert (hastfix : has_tFix).
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.
eapply (qfixs mfix idx) in hfix; tea.
eapply All_app_inv => //.
1-3:(apply and_assum; [ih|hp' P'Q]).
eapply X5; tea; (apply and_assum; [ih|hp' P'Q]).
assert (qa : Q 0 (tApp fn av)).
pose proof (ev1' := ev1).
eapply P'Q in ev1' => //.
unshelve eapply (qapp _ _ _ [av]); tea; split => //.
1-3:(apply and_assum; [ih|hp' P'Q]).
assert (qa : Q 0 (tCase ip (mkApps fn args) brs)).
pose proof (ev1' := ev1).
eapply P'Q in ev1' => //.
eapply qapp in ev1' as [hfix qargs] => //.
eapply (qcofixs mfix idx) in hfix; tea.
eapply X7; tea; (apply and_assum; [ih|hp' P'Q]).
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 (qcofixs mfix idx) in hfix; tea.
eapply X8; tea; (apply and_assum; [ih|hp' P'Q]).
cbn in IH; eapply (qconst (Q:=Q)) in isdecl.
eapply X9; tea; (apply and_assum; [ih|hp' P'Q]).
pose proof (ev1' := ev1).
eapply P'Q in ev1' => //.
eapply qpres in ev1'; depelim ev1' => //.
eapply nth_error_all in a0; tea.
eapply X10; tea; (apply and_assum; [ih|hp' P'Q]).
unshelve eapply X11; tea; try (intros; apply and_assum; [ih|hp' P'Q]).
clear -P'Q IH a a0 and_assum.
revert a0; induction a; constructor; auto.
apply and_assum; [ih|hp' P'Q].
eapply (X12 _ _ _ _ ev1); tea.
1,3:(apply and_assum; [ih|hp' P'Q]).
apply and_assum; [ih|hp' P'Q].
unshelve eapply Qprim; tea.
clear -ev IH a0 P'Q and_assum.
induction ev; constructor; eauto.
intros; split => //; eapply P'Q; tea.
Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ : wf_glob Σ -> Qpreserves (fun n x => wellformed Σ n x) Σ.
destruct t; cbn -[lookup_constructor lookup_constructor_pars_args]; intuition auto; try solve [constructor; auto].
eapply on_evar; rtoProp; intuition auto.
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_case; rtoProp; intuition auto.
eapply on_proj; rtoProp; intuition auto.
move/andP: H0 => [] _ ha.
move/andP: H0 => [] _ ha.
move/andP: H => [] hasp ht.
move/(lookup_env_wellformed clΣ).
rewrite wellformed_mkApps //.
split; intros; rtoProp; intuition auto; solve_all.
move=> hascase n ci discr brs.
destruct lookup_inductive eqn:hl => /= //.
intros; rtoProp; intuition auto; solve_all.
move=> hasproj n p discr wf discr' wf'.
eapply wellformed_substl.
unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all.
unfold EWellformed.wf_fix.
intros; rtoProp; intuition auto; solve_all.