Timings for PCUICSafeReduce.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-metacoq-safechecker.dev/./safechecker/theories/PCUICSafeReduce.v.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-metacoq-safechecker.dev/./safechecker/theories/PCUICSafeReduce.v.timing
(* Distributed under the terms of the MIT license. *)
From Coq Require Import RelationClasses.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
PCUICGeneration PCUICLiftSubst
PCUICUnivSubst PCUICTyping PCUICPosition PCUICNormal
PCUICInversion PCUICSR PCUICSN
PCUICUtils PCUICReduction PCUICValidity PCUICSafeLemmata
PCUICConfluence PCUICConversion
PCUICOnFreeVars PCUICWellScopedCumulativity
PCUICClassification.
From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfReduction PCUICWfEnv.
Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.
Set Equations Transparent.
(** * Reduction machine for PCUIC without fuel
We implement the reduction machine of Coq without relying on fuel.
Instead we assume strong normalization of the system (for well-typed terms)
and proceed by well-founded induction.
Once extracted, this should roughly correspond to the OCaml implementation.
*)
(* From Program *)
Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : metacoq_scope.
Set Default Goal Selector "!".
Local Set Keyed Unification.
Implicit Types (cf : checker_flags) (Σ : global_env_ext).
Lemma welltyped_is_closed_context {cf Σ} {wfΣ : wf Σ} {Γ t} :
welltyped Σ Γ t -> is_closed_context Γ.
now eapply typing_wf_local in X; fvs.
#[global] Hint Resolve welltyped_is_closed_context : fvs.
Lemma welltyped_is_open_term {cf Σ} {wfΣ : wf Σ} {Γ t} :
welltyped Σ Γ t -> is_open_term Γ t.
#[global] Hint Resolve welltyped_is_open_term : fvs.
(* We assume normalization of the reduction.
We state is as well-foundedness of the reduction.
*)
Context {cf : checker_flags} {no : normalizing_flags}.
Context (flags : RedFlags.t).
Context (Σ : global_env_ext).
Definition R_aux Γ :=
dlexprod (cored Σ Γ) (@posR).
Definition R Γ u v :=
R_aux Γ (zip u ; stack_pos (fst u) (snd u))
(zip v ; stack_pos (fst v) (snd v)).
Lemma cored_welltyped :
forall {Γ u v},
wf Σ -> welltyped Σ Γ u ->
cored Σ Γ v u ->
welltyped Σ Γ v.
eapply subject_reduction1 ; eassumption.
specialize IHr with (1 := ltac:(eassumption)).
eapply subject_reduction1 ; eassumption.
Lemma red_welltyped :
forall {Γ u v},
wf Σ -> welltyped Σ Γ u ->
red (fst Σ) Γ u v ->
welltyped Σ Γ v.
apply red_cored_or_eq in r.
destruct r as [r|[]]; [|assumption].
eapply cored_welltyped ; eauto.
Derive Signature for Acc.
Lemma R_positionR :
forall Γ t1 t2 (p1 : pos t1) (p2 : pos t2),
t1 = t2 ->
positionR (` p1) (` p2) ->
R_aux Γ (t1 ; p1) (t2 ; p2).
intros Γ t1 t2 p1 p2 e h.
Definition Req Γ t t' :=
t = t' \/ R Γ t t'.
Lemma Rtrans :
forall Γ u v w,
R Γ u v ->
R Γ v w ->
R Γ u w.
eapply cored_trans' ; eassumption.
Lemma Req_trans :
forall {Γ}, Transitive (Req Γ).
eapply Rtrans ; eassumption.
Lemma R_to_Req :
forall {Γ u v},
R Γ u v ->
Req Γ u v.
Instance Req_refl : forall Γ, Reflexive (Req Γ).
Lemma R_Req_R :
forall {Γ u v w},
R Γ u v ->
Req Γ v w ->
R Γ u w.
eapply Rtrans ; eassumption.
(* Added by Julien Forest on 13/11/20 in Coq stdlib, adapted to subset case by M. Sozeau *)
Section Acc_sidecond_generator.
Context {A : Type} {R : A -> A -> Prop} {P : A -> Prop}.
Variable Pimpl : forall x y, P x -> R y x -> P y.
(* *Lazily* add 2^n - 1 Acc_intro on top of wf.
Needed for fast reductions using Function and Program Fixpoint
and probably using Fix and Fix_F_2
*)
Fixpoint Acc_intro_generator n (acc : forall t, P t -> Acc R t) : forall t, P t -> Acc R t :=
match n with
| O => acc
| S n => fun x Px =>
Acc_intro x (fun y Hy => Acc_intro_generator n (Acc_intro_generator n acc) y (Pimpl _ _ Px Hy))
end.
End Acc_sidecond_generator.
(** We leave it opaque for now, as some simplification tactics
might otherwise unfold the large Acc proof. Don't forget to make it transparent
when computing. *)
Opaque Acc_intro_generator.
Context {cf : checker_flags} {no : normalizing_flags}.
Context (flags : RedFlags.t).
Context (X_type : abstract_env_impl).
Context (X : X_type.π2.π1).
Context {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ}.
(* Local Definition gΣ := abstract_env_ext_rel Σ. *)
Local Definition heΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf_ext Σ ∥ := abstract_env_ext_wf _ wfΣ.
Local Definition hΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf Σ ∥ := abstract_env_ext_sq_wf _ _ _ wfΣ.
Existing Instance Req_refl.
Lemma acc_dlexprod_gen P Q A B (leA : P -> A -> A -> Prop)
(HQ : ∥ ∑ p , Q p ∥)
(HP : forall p p' x x', Q p -> Q p' -> leA p x x' -> leA p' x x')
(leB : forall x : A, B x -> B x -> Prop) :
(forall x, well_founded (leB x)) ->
forall x,
Acc (fun t t' => forall (p:P), Q p -> leA p t t') x ->
forall y,
Acc (leB x) y ->
Acc (fun t t' => forall (p:P), Q p -> @dlexprod A B (leA p) leB t t') (x;y).
induction 1 as [x hx ih1].
induction 1 as [y hy ih2].
now eapply (HP _ _ _ _ q).
pose proof (projT2_eq H1) as p2.
set (projT1_eq H1) as p1 in *; cbn in p1.
destruct p1; cbn in p2; destruct p2.
Lemma dlexprod_Acc_gen P Q A B (leA : P -> A -> A -> Prop)
(HQ : ∥ ∑ p , Q p ∥)
(HP : forall p p' x x', Q p -> Q p' -> leA p x x' -> leA p' x x')
(leB : forall x : A, B x -> B x -> Prop) :
(forall x, well_founded (leB x)) ->
forall x y,
Acc (fun t t' => forall (p:P), Q p -> leA p t t') x ->
Acc (fun t t' => forall (p:P), Q p -> @dlexprod A B (leA p) leB t t') (x;y).
eapply acc_dlexprod_gen ; try assumption.
Definition R_singleton Abs A
(R : Abs -> A -> A -> Prop) (Q : Abs -> Prop) x (q : Q x)
(HQ : forall x x' , Q x -> Q x' -> x = x') (a a' : A) :
R x a a' <-> (forall x, Q x -> R x a a').
specialize (HQ x x' q q').
Fixpoint Acc_equiv A (R R' : A -> A -> Prop)
(Heq : forall a a', R a a' <-> R' a a') a
(HAcc : Acc R a) : Acc R' a.
Corollary R_Acc_aux :
forall Γ t p,
(forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t) ->
(Acc (fun t t' => forall Σ (wfΣ : abstract_env_ext_rel X Σ), R_aux Σ Γ t t') (t ; p)).
Proof using normalization_in.
apply abstract_env_ext_exists.
eapply abstract_env_cored; try apply H1; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
destruct (heΣ _ wfΣ).
eapply Acc_equiv; try
eapply normalization_in; eauto.
eapply R_singleton with (Q := abstract_env_ext_rel X)
(R := fun Σ a a' => cored Σ Γ a a'); eauto.
intros; eapply abstract_env_ext_irr; eauto.
Corollary R_Acc :
forall Γ t,
(forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zip t)) ->
Acc (fun t t' => forall Σ (wfΣ : abstract_env_ext_rel X Σ), R Σ Γ t t') t.
Proof using normalization_in.
pose proof (R_Acc_aux _ _ (stack_pos (fst t) (snd t)) h) as h'.
Definition inspect {A} (x : A) : { y : A | y = x } := exist x eq_refl.
Definition Pr (t' : term * stack) π :=
snd (decompose_stack π) = snd (decompose_stack (snd t')).
Notation givePr := (_) (only parsing).
Definition Pr' (t' : term * stack) :=
isApp (fst t') = false /\
(RedFlags.beta flags -> isLambda (fst t') -> isStackApp (snd t') = false).
Notation givePr' := (conj _ (fun β hl => _)) (only parsing).
Notation rec reduce t π :=
(let smaller := _ in
let '(exist res prf_Σ) := reduce t π smaller in
exist res (fun Σ wfΣ => let '((conj prf (conj h (conj h1 h2)))) := prf_Σ Σ wfΣ in conj (Req_trans _ _ _ _ _ (R_to_Req _ (smaller Σ wfΣ))) (conj givePr givePr'))
) (only parsing).
Notation give t π :=
(exist (t,π) (fun Σ wfΣ => conj _ (conj givePr givePr'))) (only parsing).
Tactic Notation "zip" "fold" "in" hyp(h) :=
lazymatch type of h with
| context C[ zipc ?t ?π ] =>
let C' := context C[ zip (t,π) ] in
change C' in h
end.
Tactic Notation "zip" "fold" :=
lazymatch goal with
| |- context C[ zipc ?t ?π ] =>
let C' := context C[ zip (t,π) ] in
change C'
end.
Lemma Req_red Σ :
forall Γ x y,
Req Σ Γ y x ->
∥ red Σ Γ (zip x) (zip y) ∥.
intros Γ [t π] [t' π'] h; simpl.
(* Show Obligation Tactic. *)
Ltac obTac :=
(* program_simpl ; *)
Program.Tactics.program_simplify ;
Equations.CoreTactics.equations_simpl ;
try Program.Tactics.program_solve_wf ;
try reflexivity.
Obligation Tactic := obTac.
Equations discr_construct (t : term) : Prop :=
discr_construct (tConstruct ind n ui) := False ;
discr_construct _ := True.
Inductive construct_view : term -> Type :=
| view_construct : forall ind n ui, construct_view (tConstruct ind n ui)
| view_other : forall t, discr_construct t -> construct_view t.
Equations construct_viewc t : construct_view t :=
construct_viewc (tConstruct ind n ui) := view_construct ind n ui ;
construct_viewc t := view_other t I.
(* Tailored view for _reduce_stack *)
Equations red_discr (t : term) (π : stack) : Prop :=
red_discr (tRel _) _ := False ;
red_discr (tLetIn _ _ _ _) _ := False ;
red_discr (tConst _ _) _ := False ;
red_discr (tApp _ _) _ := False ;
red_discr (tLambda _ _ _) (App_l _ :: _) := False ;
red_discr (tFix _ _) _ := False ;
red_discr (tCase _ _ _ _) _ := False ;
red_discr (tProj _ _) _ := False ;
red_discr _ _ := True.
Inductive red_view : term -> stack -> Type :=
| red_view_Rel c π : red_view (tRel c) π
| red_view_LetIn A b B c π : red_view (tLetIn A b B c) π
| red_view_Const c u π : red_view (tConst c u) π
| red_view_App f a π : red_view (tApp f a) π
| red_view_Lambda na A t a args : red_view (tLambda na A t) (App_l a :: args)
| red_view_Fix mfix idx π : red_view (tFix mfix idx) π
| red_view_Case ci p c brs π : red_view (tCase ci p c brs) π
| red_view_Proj p c π : red_view (tProj p c) π
| red_view_other t π : red_discr t π -> red_view t π.
Equations red_viewc t π : red_view t π :=
red_viewc (tRel c) π := red_view_Rel c π ;
red_viewc (tLetIn A b B c) π := red_view_LetIn A b B c π ;
red_viewc (tConst c u) π := red_view_Const c u π ;
red_viewc (tApp f a) π := red_view_App f a π ;
red_viewc (tLambda na A t) (App_l a :: args) := red_view_Lambda na A t a args ;
red_viewc (tFix mfix idx) π := red_view_Fix mfix idx π ;
red_viewc (tCase ci p c brs) π := red_view_Case ci p c brs π ;
red_viewc (tProj p c) π := red_view_Proj p c π ;
red_viewc t π := red_view_other t π I.
Equations discr_construct_cofix (t : term) : Prop :=
discr_construct_cofix (tConstruct ind n ui) := False ;
discr_construct_cofix (tCoFix mfix idx) := False ;
discr_construct_cofix _ := True.
Inductive construct_cofix_view : term -> Type :=
| ccview_construct : forall ind n ui, construct_cofix_view (tConstruct ind n ui)
| ccview_cofix : forall mfix idx, construct_cofix_view (tCoFix mfix idx)
| ccview_other : forall t, discr_construct_cofix t -> construct_cofix_view t.
Equations cc_viewc t : construct_cofix_view t :=
cc_viewc (tConstruct ind n ui) := ccview_construct ind n ui ;
cc_viewc (tCoFix mfix idx) := ccview_cofix mfix idx ;
cc_viewc t := ccview_other t I.
Equations discr_construct0_cofix (t : term) : Prop :=
discr_construct0_cofix (tConstruct ind n ui) := n <> 0 ;
discr_construct0_cofix (tCoFix mfix idx) := False ;
discr_construct0_cofix _ := True.
Inductive construct0_cofix_view : term -> Type :=
| cc0view_construct : forall ind ui, construct0_cofix_view (tConstruct ind 0 ui)
| cc0view_cofix : forall mfix idx, construct0_cofix_view (tCoFix mfix idx)
| cc0view_other : forall t, discr_construct0_cofix t -> construct0_cofix_view t.
Equations cc0_viewc t : construct0_cofix_view t :=
cc0_viewc (tConstruct ind 0 ui) := cc0view_construct ind ui ;
cc0_viewc (tCoFix mfix idx) := cc0view_cofix mfix idx ;
cc0_viewc t := cc0view_other t _.
Equations _reduce_stack (Γ : context) (t : term) (π : stack)
(h : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zip (t,π)))
(reduce : forall t' π', (forall Σ (wfΣ : abstract_env_ext_rel X Σ), R Σ Γ (t',π') (t,π)) ->
{ t'' : term * stack | forall Σ (wfΣ : abstract_env_ext_rel X Σ), Req Σ Γ t'' (t',π') /\ Pr t'' π' /\ Pr' t'' })
: { t' : term * stack | forall Σ (wfΣ : abstract_env_ext_rel X Σ), Req Σ Γ t' (t,π) /\ Pr t' π /\ Pr' t' } :=
_reduce_stack Γ t π h reduce with red_viewc t π := {
| red_view_Rel c π with RedFlags.zeta flags := {
| true with inspect (nth_error (Γ ,,, stack_context π) c) := {
| @exist None eq := False_rect _ _ ;
| @exist (Some d) eq with inspect d.(decl_body) := {
| @exist None _ := give (tRel c) π ;
| @exist (Some b) H := rec reduce (lift0 (S c) b) π
}
} ;
| false := give (tRel c) π
} ;
| red_view_LetIn A b B c π with RedFlags.zeta flags := {
| true := rec reduce (subst10 b c) π ;
| false := give (tLetIn A b B c) π
} ;
| red_view_Const c u π with RedFlags.delta flags := {
| true with inspect (abstract_env_lookup X c) := {
| @exist (Some (ConstantDecl {| cst_body := Some body |})) eq :=
let body' := subst_instance u body in
rec reduce body' π ;
| @exist (Some (InductiveDecl _)) eq := False_rect _ _ ;
| @exist (Some _) eq := give (tConst c u) π ;
| @exist None eq := False_rect _ _
} ;
| _ := give (tConst c u) π
} ;
| red_view_App f a π := rec reduce f (App_l a :: π) ;
| red_view_Lambda na A t a args with inspect (RedFlags.beta flags) := {
| @exist true eq1 := rec reduce (subst10 a t) args ;
| @exist false eq1 := give (tLambda na A t) (App_l a :: args)
} ;
| red_view_Fix mfix idx π with RedFlags.fix_ flags := {
| true with inspect (unfold_fix mfix idx) := {
| @exist (Some (narg, fn)) eq1 with inspect (decompose_stack_at π narg) := {
| @exist (Some (args, c, ρ)) eq2 with inspect (reduce c (Fix_app mfix idx args :: ρ) _) := {
| @exist (@exist (t, ρ') prf) eq3 with construct_viewc t := {
| view_construct ind n ui with inspect (decompose_stack ρ') := {
| @exist (l, θ) eq4 :=
rec reduce fn (appstack args (App_l (mkApps (tConstruct ind n ui) l) :: ρ))
} ;
| view_other t ht with inspect (decompose_stack ρ') := {
| @exist (l, θ) eq4 :=
give (tFix mfix idx) (appstack args (App_l (mkApps t l) :: ρ))
}
}
} ;
| _ := give (tFix mfix idx) π
} ;
| _ := give (tFix mfix idx) π
} ;
| false := give (tFix mfix idx) π
} ;
| red_view_Case ci p c brs π with RedFlags.iota flags := {
| true with inspect (reduce c (Case_discr ci p brs :: π) _) := {
| @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
| @exist (args, ρ) prf' with cc_viewc t := {
| ccview_construct ind' c' inst' with inspect (nth_error brs c') := {
| exist (Some br) eqbr := rec reduce (iota_red ci.(ci_npar) p args br) π ;
| exist None bot := False_rect _ _ } ;
| ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
| @exist (Some (narg, fn)) eq' :=
rec reduce (tCase ci p (mkApps fn args) brs) π ;
| @exist None bot := False_rect _ _
} ;
| ccview_other t ht := give (tCase ci p (mkApps t args) brs) π
}
}
} ;
| false := give (tCase ci p c brs) π
} ;
| red_view_Proj p c π with RedFlags.iota flags := {
| true with inspect (reduce c (Proj p :: π) _) := {
| @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
| @exist (args, ρ) prf' with cc0_viewc t := {
| cc0view_construct ind' _
with inspect (nth_error args (p.(proj_npars) + p.(proj_arg))) := {
| @exist (Some arg) eqa := rec reduce arg π ;
| @exist None eqa := False_rect _ _
} ;
| cc0view_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
| @exist (Some (rarg, fn)) eq' :=
rec reduce (tProj p (mkApps fn args)) π ;
| @exist None bot := False_rect _ _
} ;
| cc0view_other t ht := give (tProj p (mkApps t args)) π
}
}
} ;
| false := give (tProj p c) π
} ;
| red_view_other t π discr := give t π
}.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
pose proof (welltyped_context _ hΣ _ _ (h _ wfΣ)) as hc.
generalize (Γ ,,, stack_context π) as Δ.
induction Γ ; intros c hc eq.
apply inversion_Rel in h as hh ; auto.
destruct hh as [? [? [e ?]]].
eapply IHΓ ; try eassumption.
apply inversion_Rel in h as hh ; auto.
destruct hh as [? [? [e ?]]].
unfold declared_constant, declared_constant_gen.
rewrite (abstract_env_lookup_correct _ _ _ wfΣ).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [wΣ].
eapply welltyped_context in h ; auto.
apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
unfold declared_constant, declared_constant_gen in d.
rewrite (abstract_env_lookup_correct _ _ _ wfΣ), <- eq in d.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [wΣ].
eapply welltyped_context in h ; auto.
apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
unfold declared_constant, declared_constant_gen in d.
rewrite (abstract_env_lookup_correct _ _ _ wfΣ), <- eq in d.
rewrite stack_position_cons.
eapply positionR_poscat_nonil.
case_eq (decompose_stack π).
case_eq (decompose_stack args).
pose proof (decompose_stack_at_eq _ _ _ _ _ eq2).
rewrite !stack_position_appstack, !stack_position_cons.
case_eq (decompose_stack π).
pose proof (decompose_stack_eq _ _ _ e).
destruct prf as [r [p p0]].
pose proof (decompose_stack_at_eq _ _ _ _ _ eq2).
pose proof (decompose_stack_at_length _ _ _ _ _ eq2).
case_eq (decompose_stack ρ).
pose proof (decompose_stack_eq _ _ _ e').
rewrite decompose_stack_appstack in e.
case_eq (decompose_stack ρ').
pose proof (decompose_stack_eq _ _ _ e1).
instantiate (1 := (tFix mfix idx, appstack (args ++ (mkApps (tConstruct ind n ui) l) :: l') π')).
assert (forall args l u v, mkApps (tApp (mkApps u args) v) l = mkApps u (args ++ v :: l)) as thm.
induction args ; intros l u v.
rewrite nth_error_app2 by eauto.
replace (#|args| - #|args|) with 0 by auto with arith.
rewrite decompose_app_mkApps by reflexivity.
dependent destruction H0.
rewrite 2!zipc_appstack in H0.
rewrite decompose_stack_appstack in eq4.
case_eq (decompose_stack s).
rewrite app_nil_r in eq4.
pose proof (decompose_stack_eq _ _ _ e2) as ee.
match goal with
| |- ?A =>
let e := fresh "e" in
let B := type of H0 in
assert (A = B) as e ; [| rewrite e ; assumption ]
end.
set (t := tConstruct ind n ui).
set (f := tFix mfix idx).
induction args ; intros ll π' l' t f.
induction args ; intros π' l' c f.
pose proof (decompose_stack_eq _ _ _ e2) as ee.
eapply decompose_stack_not_app.
rewrite 2!zipc_appstack in H3.
rewrite zipc_appstack in H3.
apply PCUICAstUtils.mkApps_inj in H3.
rewrite decompose_stack_appstack in h.
case_eq (decompose_stack ρ).
pose proof (decompose_stack_eq _ _ _ e).
pose proof (decompose_stack_at_eq _ _ _ _ _ eq2).
rewrite decompose_stack_appstack.
case_eq (decompose_stack π).
pose proof (decompose_stack_eq _ _ _ e).
destruct prf as [r [p p0]].
pose proof (decompose_stack_at_eq _ _ _ _ _ eq2) as e2.
pose proof (decompose_stack_at_length _ _ _ _ _ eq2).
case_eq (decompose_stack ρ).
pose proof (decompose_stack_eq _ _ _ e').
rewrite decompose_stack_appstack in e.
apply decompose_stack_eq in eq4 as ?.
rewrite zipc_appstack in H.
rewrite !zipc_appstack in H.
rewrite !zipc_appstack in H2.
rewrite zipc_appstack in H2.
apply PCUICAstUtils.mkApps_inj in H2.
destruct prf as [r [p p0]].
rewrite decompose_stack_appstack.
case_eq (decompose_stack π).
pose proof (decompose_stack_eq _ _ _ e).
pose proof (decompose_stack_at_eq _ _ _ _ _ eq2) as e2.
pose proof (decompose_stack_at_length _ _ _ _ _ eq2).
case_eq (decompose_stack ρ).
pose proof (decompose_stack_eq _ _ _ e').
rewrite decompose_stack_appstack in e.
rewrite stack_position_cons.
eapply positionR_poscat_nonil.
pose proof (hΣ := hΣ _ wfΣ).
destruct prf as [r [p0 p1]].
apply eq_sym, decompose_stack_eq in prf'; subst.
apply Req_red in r; cbn in r.
rewrite zipc_appstack in r.
eapply red_welltyped in r' ; tea.
apply welltyped_context in r' as (?&typ); auto; cbn in *.
apply PCUICInductiveInversion.invert_Case_Construct in typ as H; auto.
destruct H as (?&?&nth&?); subst.
rewrite nth in eqbr; noconf eqbr.
eapply cored_red_cored; cycle 1.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [p0 p1]].
apply eq_sym, decompose_stack_eq in prf'; subst.
apply Req_red in r; cbn in r.
rewrite zipc_appstack in r.
eapply red_welltyped in r; eauto.
apply welltyped_context in r as (?&typ); auto; cbn in *.
apply PCUICInductiveInversion.invert_Case_Construct in typ as H; auto.
destruct H as (?&?&nth&?); subst.
rewrite nth in bot; congruence.
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [p0 p1]].
apply eq_sym, decompose_stack_eq in prf'; subst.
apply Req_red in r; cbn in r.
rewrite zipc_appstack in r.
eapply red_welltyped in r; eauto.
apply welltyped_context in r as (?&typ); auto; cbn in *.
eapply cored_red_cored; cycle 1.
zip fold in r'; exact r'.
eapply red_cofix_case; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [p0 p1]].
apply eq_sym, decompose_stack_eq in prf'; subst.
apply Req_red in r; cbn in r.
eapply red_welltyped in r; eauto.
apply welltyped_context in r as (?&typ); auto; cbn in *.
apply inversion_CoFix in typ as (?&?&?&?&?&?&?); auto.
unfold unfold_cofix in bot.
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [p0 p1]].
pose proof (decompose_stack_eq _ _ _ prf').
rewrite zipc_appstack in H.
pose proof (decompose_stack_eq _ _ _ prf').
rewrite zipc_appstack in H2.
rewrite stack_position_cons.
pose proof (hΣ := hΣ _ wfΣ).
destruct (prf Σ wfΣ) as [r [p' p0]].
apply Req_red in r as hr.
pose proof (red_welltyped _ hΣ (h _ wfΣ) hr) as hh.
eapply cored_red_cored ; try eassumption.
apply decompose_stack_eq in prf' as ?.
rewrite zipc_appstack in hh.
apply welltyped_context in hh.
apply Proj_Construct_ind_eq in hh.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [pr p0]].
apply decompose_stack_eq in prf' as ?.
apply Req_red in r as hr.
pose proof (red_welltyped _ hΣ (h _ wfΣ) hr) as hh.
rewrite zipc_appstack in hh.
apply welltyped_context in hh.
apply Proj_red_cond in hh.
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [pr p0]].
eapply red_cofix_proj with (args := []).
apply decompose_stack_eq in prf' as ?.
rewrite zipc_appstack in H.
eapply cored_trans' ; try eassumption.
apply decompose_stack_eq in prf' as ?.
rewrite zipc_appstack in H2.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [pr p0]].
assert (h' : welltyped Σ Γ (zip (tProj p (mkApps (tCoFix mfix idx) args), π))).
eapply red_welltyped ; eauto.
apply decompose_stack_eq in prf'.
rewrite zipc_appstack in r.
apply decompose_stack_eq in prf'.
rewrite zipc_appstack in H2.
replace (zip (tProj p (mkApps (tCoFix mfix idx) args), π))
with (zip (tCoFix mfix idx, appstack args (Proj p :: π)))
in h'.
apply welltyped_context in h' ; auto.
apply inversion_CoFix in h' ; auto.
destruct h' as [decl [? [e [? [? ?]]]]].
unfold unfold_cofix in bot.
destruct (hΣ _ wfΣ) as [hΣ].
destruct (prf Σ wfΣ) as [r [pr p0]].
pose proof (decompose_stack_eq _ _ _ prf').
rewrite zipc_appstack in H.
pose proof (decompose_stack_eq _ _ _ prf').
rewrite zipc_appstack in H2.
apply_funelim (red_discr t π).
apply_funelim (red_discr t π).
Lemma welltyped_R_pres Σ (wfΣ : abstract_env_ext_rel X Σ) Γ :
forall x y : term × stack, welltyped Σ Γ (zip x) -> R Σ Γ y x -> welltyped Σ Γ (zip y).
pose proof (heΣ := heΣ _ wfΣ).
pose proof (hΣ := hΣ _ wfΣ).
clear wfΣ X_type X normalization_in.
destruct x as [x πx], y as [y πy].
revert H1; intros [= H2 _].
Notation sigmaarg :=
(sigma (fun t => sigma (fun π => forall Σ, abstract_env_ext_rel X Σ -> welltyped Σ Γ (zipc t π)))).
Local Instance wf_proof : WellFounded (fun x y : sigmaarg =>
forall Σ, abstract_env_ext_rel X Σ -> R Σ Γ (pr1 x, pr1 (pr2 x)) (pr1 y, pr1 (pr2 y))).
Proof using normalization_in.
(* We fuel the accessibility proof to run reduction inside Coq. *)
unshelve eapply (Acc_intro_generator
(R:=fun x y : sigmaarg => forall Σ (wfΣ : abstract_env_ext_rel X Σ), R Σ Γ (x.(pr1), x.(pr2).(pr1)) (y.(pr1), y.(pr2).(pr1)))
(P:=fun x : sigmaarg => forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zip (x.(pr1), x.(pr2).(pr1))))
(fun x y Px Hy => _) 1000 _ {| pr1 := t; pr2 := {| pr1 := π; pr2 := wt |} |} wt).
destruct y as [t' [π' wt']].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (hΣ _ wfΣ) as [hΣ].
pose proof (R_Acc Γ (t0.(pr1), t0.(pr2).(pr1)) H).
destruct t0 as [t [π wt]].
Equations reduce_stack_full (t : term) (π : stack) (h : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zip (t,π))) :
{ t' : term * stack | forall Σ (wfΣ : abstract_env_ext_rel X Σ), Req Σ Γ t' (t, π) /\ Pr t' π /\ Pr' t' }
by wf (t, π) (fun (x y : term * stack) => forall Σ (wfΣ : abstract_env_ext_rel X Σ), R Σ Γ x y) :=
reduce_stack_full t π h := _reduce_stack Γ t π h (fun t' π' hr => reduce_stack_full t' π' (fun Σ wfΣ' => welltyped_R_pres Σ wfΣ' Γ _ _ (h Σ wfΣ') (hr Σ wfΣ'))).
Definition reduce_stack Γ t π h :=
let '(exist ts _) := reduce_stack_full Γ t π h in ts.
Lemma reduce_stack_Req :
forall Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h,
Req Σ Γ (reduce_stack Γ t π h) (t, π).
edestruct (reduce_stack_full Γ t π h) as [[t' π'] [r _]];
eassumption.
Theorem reduce_stack_sound :
forall Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h,
∥ Σ ;;; Γ ⊢ zip (t, π) ⇝ zip (reduce_stack Γ t π h) ∥.
assert (req := reduce_stack_Req Σ wfΣ _ _ _ h).
eapply into_closed_red; fvs.
Lemma reduce_stack_decompose :
forall Γ t π h,
snd (decompose_stack (snd (reduce_stack Γ t π h))) =
snd (decompose_stack π).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
edestruct (reduce_stack_full Γ t π h) as [[t' π'] [r [p p']]];
try eassumption.
Lemma reduce_stack_context :
forall Γ t π h,
stack_context (snd (reduce_stack Γ t π h)) =
stack_context π.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (reduce_stack_decompose Γ t π h) as hd.
case_eq (decompose_stack π).
case_eq (decompose_stack (snd (reduce_stack Γ t π h))).
pose proof (decompose_stack_eq _ _ _ e1).
pose proof (decompose_stack_eq _ _ _ e2) as eq.
rewrite 2!stack_context_appstack.
Definition isred (t : term * stack) :=
isApp (fst t) = false /\
(isLambda (fst t) -> isStackApp (snd t) = false).
Lemma reduce_stack_isred :
forall Γ t π h,
RedFlags.beta flags ->
isred (reduce_stack Γ t π h).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
edestruct (reduce_stack_full Γ t π h) as [[t' π'] [r [p [hApp hLam]]]]; eauto.
Lemma reduce_stack_noApp :
forall Γ t π h,
isApp (fst (reduce_stack Γ t π h)) = false.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
edestruct (reduce_stack_full Γ t π h) as [[t' π'] [r [p [hApp hLam]]]]; eauto.
Lemma reduce_stack_noLamApp :
forall Γ t π h,
RedFlags.beta flags ->
isLambda (fst (reduce_stack Γ t π h)) ->
isStackApp (snd (reduce_stack Γ t π h)) = false.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
edestruct (reduce_stack_full Γ t π h) as [[t' π'] [r [p [hApp hLam]]]]; eauto.
Definition reduce_term Γ t
(h : forall Σ, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) :=
zip (reduce_stack Γ t [] h).
Theorem reduce_term_sound :
forall Γ t (h : forall Σ, abstract_env_ext_rel X Σ -> welltyped Σ Γ t)
Σ, abstract_env_ext_rel X Σ ->
∥ Σ ;;; Γ ⊢ t ⇝ reduce_term Γ t h ∥.
refine (reduce_stack_sound _ _ _ _ [] _); eauto.
Scheme Acc_ind' := Induction for Acc Sort Prop.
Lemma Fix_F_prop :
forall A R P f (pred : forall x : A, P x -> Prop) x hx,
(forall x aux, (forall y hy, pred y (aux y hy)) -> pred x (f x aux)) ->
pred x (@Fix_F A R P f x hx).
intros A R P f pred x hx h.
induction hx using Acc_ind'.
Lemma reduce_stack_prop :
forall Γ t π h (P : term × stack -> term × stack -> Prop),
(forall t π h aux,
(forall t' π' hR, P (t', π') (` (aux t' π' hR))) ->
P (t, π) (` (_reduce_stack Γ t π h aux))) ->
P (t, π) (reduce_stack Γ t π h).
case_eq (reduce_stack_full Γ t π h).
apply_funelim (reduce_stack_full Γ t π h); clear -hP.
intros t π wt ih [t' ρ] ? e.
match type of e with
| _ = ?u =>
change (P (t, π) (` u))
end.
set (r := reduce_stack_full _ _ _ _) in *.
eapply (ih _ (proj2_sig r)).
Lemma decompose_stack_at_appstack_None l s n :
isStackApp s = false ->
nth_error l n = None <->
decompose_stack_at (appstack l s) n = None.
induction l in l, n |- *; cbn in *.
destruct s as [|[]]; cbn in *; easy.
now destruct decompose_stack_at as [((?&?)&?)|]; intros.
Lemma mkApps_tApp hd arg args :
mkApps (tApp hd arg) args = mkApps hd (arg :: args).
Lemma tApp_mkApps hd args arg :
tApp (mkApps hd args) arg = mkApps hd (args ++ [arg]).
change (tApp ?hd ?a) with (mkApps hd [a]).
Lemma whnf_non_ctor_finite_ind_typed Σ Γ t ind u args :
wf Σ ->
whnf flags Σ Γ t ->
isConstruct_app t = false ->
check_recursivity_kind (lookup_env Σ) (inductive_mind ind) CoFinite = false ->
Σ ;;; Γ |- t : mkApps (tInd ind u) args ->
whne flags Σ Γ t.
intros wf wh ctor fin typ.
apply inversion_Sort in typ as (?&?&?); auto.
exfalso; eapply invert_cumul_sort_ind; eauto.
apply inversion_Prod in typ as (?&?&?&?&?); auto.
exfalso; eapply invert_cumul_sort_ind; eauto.
apply inversion_Lambda in typ as (?&?&?&?&?); auto.
exfalso; eapply invert_cumul_prod_ind; eauto.
unfold isConstruct_app in ctor.
now rewrite decompose_app_mkApps in ctor.
exfalso; eapply invert_ind_ind; eauto.
exfalso; eapply invert_fix_ind; eauto.
destruct o as [[? [-> ?]] | ->]; eauto.
apply typing_cofix_coind in typ; auto.
unfold PCUICAst.PCUICEnvironment.fst_ctx in *.
eapply inversion_Prim in typ as (prim_ty & cdecl & [? ? ? [? []]]); tea.
now eapply invert_cumul_axiom_ind in w; tea.
Definition isCoFix_app t :=
match (decompose_app t).1 with
| tCoFix _ _ => true
| _ => false
end.
Lemma whnf_non_ctor_non_cofix_ind_typed Σ Γ t ind u args :
wf Σ ->
whnf flags Σ Γ t ->
isConstruct_app t = false ->
isCoFix_app t = false ->
Σ ;;; Γ |- t : mkApps (tInd ind u) args ->
whne flags Σ Γ t.
intros wf wh ctor cof typ.
apply inversion_Sort in typ as (?&?&?); auto.
exfalso; eapply invert_cumul_sort_ind; eauto.
apply inversion_Prod in typ as (?&?&?&?&?); auto.
exfalso; eapply invert_cumul_sort_ind; eauto.
apply inversion_Lambda in typ as (?&?&?&?&?); auto.
exfalso; eapply invert_cumul_prod_ind; eauto.
unfold isConstruct_app in ctor.
now rewrite decompose_app_mkApps in ctor.
exfalso; eapply invert_ind_ind; eauto.
exfalso; eapply invert_fix_ind; eauto.
destruct o as [[? [-> ?]] | ->]; eauto.
unfold isCoFix_app in cof.
now rewrite decompose_app_mkApps in cof.
eapply inversion_Prim in typ as [prim_ty [cdecl [? ? ? [? []]]]]; tea.
now eapply invert_cumul_axiom_ind in w; tea.
Lemma whnf_fix_arg_whne mfix idx body Σ Γ t before args aftr ty :
wf Σ ->
unfold_fix mfix idx = Some (#|before|, body) ->
match t with
| tConstruct _ _ _ => False
| tApp _ _ => False
| _ => True
end ->
whnf flags Σ Γ (mkApps t args) ->
Σ ;;; Γ |- mkApps (tFix mfix idx) (before ++ mkApps t args :: aftr) : ty ->
whne flags Σ Γ (mkApps t args).
intros wf uf shape wh typ.
apply inversion_mkApps in typ as (fix_ty & typ_fix & typ_args); auto.
apply inversion_Fix in typ_fix as (def&?&?&?&?&?&?); auto.
eapply All_nth_error in a; eauto.
eapply wf_fixpoint_spine in i; eauto.
eapply PCUICSpine.typing_spine_strengthen; eauto.
rewrite nth_error_snoc in i by congruence.
destruct i as (?&?&?&typ&fin).
eapply whnf_non_ctor_finite_ind_typed; try eassumption.
rewrite decompose_app_mkApps by (now destruct t).
destruct check_recursivity_kind eqn:cofin in |- *; [|easy].
eapply check_recursivity_kind_inj in fin; [|exact cofin].
Lemma whnf_case_arg_whne Σ Γ hd args ci p brs T :
wf Σ ->
match hd with
| tApp _ _
| tConstruct _ _ _
| tCoFix _ _ => False
| _ => True
end ->
whnf flags Σ Γ (mkApps hd args) ->
Σ;;; Γ |- tCase ci p (mkApps hd args) brs : T ->
whne flags Σ Γ (mkApps hd args).
apply inversion_Case in typ as (?&?&isdecl&?&[]&?); auto.
eapply whnf_non_ctor_finite_ind_typed; try eassumption.
now rewrite decompose_app_mkApps; destruct hd.
unfold isCoFinite in not_cofinite.
unfold check_recursivity_kind.
unshelve eapply declared_inductive_to_gen in isdecl; eauto.
unfold declared_inductive, declared_minductive in isdecl.
Lemma whnf_proj_arg_whne Σ Γ hd args p T :
wf Σ ->
match hd with
| tApp _ _
| tCoFix _ _ => False
| tConstruct _ c _ => c <> 0
| _ => True
end ->
whnf flags Σ Γ (mkApps hd args) ->
Σ ;;; Γ |- tProj p (mkApps hd args) : T ->
whne flags Σ Γ (mkApps hd args).
apply inversion_Proj in typ as (?&?&?&?&?&?&?&?&?); auto.
eapply whnf_non_ctor_non_cofix_ind_typed; try eassumption.
rewrite decompose_app_mkApps by (now destruct hd).
eapply PCUICInductiveInversion.invert_Proj_Construct in typ' as (?&?&?); auto.
now rewrite decompose_app_mkApps; destruct hd.
Lemma reduce_stack_whnf :
forall Γ t π h Σ (wfΣ : abstract_env_ext_rel X Σ),
let '(u, ρ) := reduce_stack Γ t π h in
∥whnf flags Σ (Γ ,,, stack_context ρ) (zipp u ρ)∥.
eapply reduce_stack_prop
with (P := fun x y =>
let '(u, ρ) := y in
∥whnf flags Σ (Γ ,,, stack_context ρ) (zipp u ρ)∥
).
apply_funelim (_reduce_stack Γ t π h aux); clear -wfΣ.
all: repeat match goal with
[ |- (forall (t' : term) (π' : stack)
(hR : forall Σ,
abstract_env_ext_rel X Σ -> R Σ _ _ _), { _ : _ | _ }) -> _ ] => intros reduce
| [ |- (forall (t' : term) (π' : stack)
(hR : forall Σ,
abstract_env_ext_rel X Σ -> R Σ _ _ _), _) -> _ ] => intros haux
| [ |- _ ] => intros ?
end.
all: try match goal with
| |- context[False_rect _ ?f] => destruct f
end.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
revert h reduce haux; apply_funelim (red_discr t π); clear -wfΣ.
all: intros; try destruct discr.
all: try solve [ constructor ; constructor ].
all: try solve [
unfold zipp ; case_eq (decompose_stack π) ; intros ;
do 2 constructor ; eapply whne_mkApps ; constructor
].
case_eq (decompose_stack π).
apply decompose_stack_eq in e.
destruct (hΣ _ wfΣ) as [hΣ].
apply welltyped_context in h; auto.
rewrite stack_context_appstack in h.
apply inversion_App in h as (?&?&?&?&?); auto.
apply inversion_Sort in t0 as (?&?&?); auto.
eapply PCUICConversion.ws_cumul_pb_Sort_Prod_inv; eauto.
case_eq (decompose_stack π).
apply decompose_stack_eq in e.
destruct (hΣ _ wfΣ) as [hΣ].
apply welltyped_context in h; auto.
rewrite stack_context_appstack in h.
apply inversion_App in h as (?&?&?&?&?); auto.
apply inversion_Prod in t0 as (?&?&?&?&?); auto.
eapply PCUICConversion.ws_cumul_pb_Sort_Prod_inv; eauto.
case_eq (decompose_stack π).
apply decompose_stack_eq in e.
destruct (hΣ _ wfΣ) as [hΣ].
apply welltyped_context in h; auto.
rewrite stack_context_appstack in h.
apply inversion_App in h as (?&?&?&?&?); auto.
apply inversion_Prim in t0 as (prim_ty & cdecl & [? ? ? [s []]]); auto.
eapply PCUICClassification.invert_cumul_axiom_prod; eauto.
case_eq (decompose_stack π).
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
case_eq (decompose_stack π).
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
case_eq (decompose_stack π).
eapply whne_letin_nozeta.
case_eq (decompose_stack π).
eapply whne_const_nodelta.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
case_eq (decompose_stack π).
erewrite abstract_env_lookup_correct'; eauto.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
destruct decompose_stack eqn:eq.
apply decompose_stack_noStackApp in eq as ?.
apply decompose_stack_eq in eq.
now apply whne_lam_nobeta.
destruct decompose_stack.
now apply whne_fix_nofix.
destruct decompose_stack.
destruct decompose_stack eqn:eq.
apply decompose_stack_noStackApp in eq as ?.
apply decompose_stack_eq in eq.
unfold unfold_fix in eq1.
apply <- decompose_stack_at_appstack_None in e ; eauto.
destruct (nth_error mfix idx) ; [left | now right].
eexists; split ; now eauto.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
specialize (haux x y z) as ?;
destruct (reduce x y z)
end.
destruct (a _ wfΣ) as (?&?&?&?).
match type of eq3 with
| context [ reduce ?x ?y ?z ] =>
specialize (haux x y z);
destruct (reduce x y z)
end.
pose proof (hΣ _ wfΣ) as [hΣ].
clear -wfΣ hΣ eq4 ht eq2 eq1 h prf haux.
destruct (prf _ wfΣ) as (r&stacks&?).
rewrite <- eq4 in stacks.
assert (narg = #|args|) as -> by (now apply decompose_stack_at_length in eq2).
eapply decompose_stack_at_eq in eq2 as ->.
apply decompose_stack_eq in eq4.
rewrite zipc_appstack in h.
apply Req_red in r as [r].
eapply red_welltyped in h; eauto.
rewrite zipc_appstack in h.
rewrite tApp_mkApps in h.
apply welltyped_zipc_zipp in h; auto.
rewrite decompose_stack_appstack in *.
destruct (decompose_stack ρ) eqn:decomp.
apply decompose_stack_eq in decomp as ->.
rewrite <-mkApps_app in h.
repeat (try rewrite stack_context_appstack;
try rewrite stack_context_appstack in typ;
try rewrite stack_context_appstack in haux;
try rewrite stack_context_appstack in H;
cbn in * ).
destruct H as (noapp&_); cbn in *.
rewrite <- app_assoc in *.
unfold unfold_fix in eq1.
case_eq (nth_error mfix idx); [intros d e | intro e]; rewrite e in eq1; inversion eq1.
now apply nth_error_snoc.
eapply whnf_fix_arg_whne; eauto.
destruct decompose_stack.
now apply whne_case_noiota.
match type of eq with
| _ = reduce ?x ?y ?z =>
specialize (haux x y z);
destruct (reduce x y z)
end.
pose proof (hΣ _ wfΣ) as [hΣ].
clear -hΣ wfΣ ht prf' h prf haux.
destruct (prf _ wfΣ) as (r&stacks&?).
rewrite <- prf' in stacks.
apply decompose_stack_eq in prf' as ->.
apply Req_red in r as [r].
eapply red_welltyped in h; eauto using sq.
rewrite zipc_appstack in h.
apply welltyped_context in h; auto.
rewrite decompose_stack_appstack in haux; cbn in *.
destruct decompose_stack eqn:decomp.
apply decompose_stack_eq in decomp as ->.
repeat (try rewrite stack_context_appstack;
try rewrite stack_context_appstack in typ;
try rewrite stack_context_appstack in haux;
try rewrite stack_context_appstack in H;
cbn in * ).
apply whnf_mkApps, whne_case.
eapply whnf_case_arg_whne; eauto.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
case_eq (decompose_stack π).
match type of eq with
| _ = reduce ?x ?y ?z =>
specialize (haux x y z);
destruct (reduce x y z)
end.
pose proof (hΣ _ wfΣ) as [hΣ].
clear -hΣ wfΣ ht prf' h prf haux.
destruct (prf _ wfΣ) as (r&stacks&?).
rewrite <- prf' in stacks.
apply decompose_stack_eq in prf' as ->.
apply Req_red in r as [r].
eapply red_welltyped in h; eauto using sq.
rewrite zipc_appstack in h.
apply welltyped_context in h; auto.
rewrite decompose_stack_appstack in haux; cbn in *.
destruct decompose_stack eqn:decomp.
apply decompose_stack_eq in decomp as ->.
repeat (try rewrite stack_context_appstack;
try rewrite stack_context_appstack in typ;
try rewrite stack_context_appstack in haux;
try rewrite stack_context_appstack in H;
cbn in * ).
apply whnf_mkApps, whne_proj.
eapply whnf_proj_arg_whne; eauto.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
match goal with
| |- context [ reduce ?x ?y ?z ] =>
case_eq (reduce x y z) ;
specialize (haux x y z)
end.
Theorem reduce_term_complete Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t h :
∥whnf flags Σ Γ (reduce_term Γ t h)∥.
pose proof (reduce_stack_whnf Γ t [] h _ wfΣ) as H.
unfold reduce_stack in *.
destruct reduce_stack_full.
destruct (a _ wfΣ) as (_&stack_eq&_).
destruct decompose_stack eqn:decomp.
apply decompose_stack_eq in decomp.
rewrite stack_context_appstack, decompose_stack_appstack in H.
now rewrite app_nil_r in H.
Context {cf : checker_flags} {no : normalizing_flags}
{X_type : abstract_env_impl} {X : X_type.π2.π1} {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ}.
(* We get stack overflow on Qed after Equations definitions when this is transparent *)
Opaque reduce_stack_full.
Definition hnf := reduce_term RedFlags.default X_type X.
Theorem hnf_sound {Γ t h} Σ (wfΣ : abstract_env_ext_rel X Σ) : ∥ Σ ;;; Γ ⊢ t ⇝ hnf Γ t h ∥.
destruct (reduce_term_sound RedFlags.default _ X _ _ h Σ wfΣ).
eapply into_closed_red; fvs.
Theorem hnf_complete {Γ t h} Σ (wfΣ : abstract_env_ext_rel X Σ) : ∥whnf RedFlags.default Σ Γ (hnf Γ t h)∥.
apply reduce_term_complete; eauto.
Equations? reduce_to_sort (Γ : context) (t : term)
(h : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t)
: typing_result_comp (∑ u, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ t ⇝ tSort u ∥) :=
reduce_to_sort Γ t h with view_sortc t := {
| view_sort_sort s => Checked_comp (s; _);
| view_sort_other t _ with inspect (hnf Γ t h) :=
| exist hnft eq with view_sortc hnft := {
| view_sort_sort s => Checked_comp (s; _);
| view_sort_other hnft r => TypeError_comp (NotASort hnft) _
}
}.
destruct (h _ wfΣ) as [? hs].
pose proof (hΣ := hΣ _ X _ wfΣ).
eapply (wt_closed_red_refl hs).
pose proof (hnf_sound (h:=h)).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (hΣ := hΣ _ X _ wfΣ).
edestruct (@hnf_complete Γ t h) as [wh]; eauto.
edestruct (@hnf_sound Γ t h) as [r']; eauto.
eapply PCUICContextConversion.closed_red_confluence in X1 as (?&r1&r2); eauto.
apply invert_red_sort in r2 as ->.
eapply whnf_red_inv in r1; eauto.
Lemma reduce_to_sort_complete {Γ t wt} Σ (wfΣ : abstract_env_ext_rel X Σ)
e p :
reduce_to_sort Γ t wt = TypeError_comp e p ->
(forall s, red Σ Γ t (tSort s) -> False).
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
pose proof (hΣ := hΣ _ X _ wfΣ).
eapply into_closed_red in r ; fvs.
Equations? reduce_to_prod (Γ : context) (t : term)
(h : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t)
: typing_result_comp (∑ na a b, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ t ⇝ tProd na a b ∥) :=
reduce_to_prod Γ t h with view_prodc t := {
| view_prod_prod na a b => Checked_comp (na; a; b; _);
| view_prod_other t _ with inspect (hnf Γ t h) :=
| exist hnft eq with view_prodc hnft := {
| view_prod_prod na a b => Checked_comp (na; a; b; _);
| view_prod_other hnft _ => TypeError_comp (NotAProduct t hnft) _
}
}.
destruct (h _ wfΣ) as [? hs].
pose proof (hΣ := hΣ _ _ _ wfΣ).
now eapply wt_closed_red_refl.
pose proof (hnf_sound (h:=h)).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
edestruct (@hnf_complete Γ t h) as [wh]; eauto.
edestruct (@hnf_sound Γ t h) as [r']; eauto.
eapply PCUICContextConversion.closed_red_confluence in X3 as (?&r1&r2); eauto.
apply invert_red_prod in r2 as (?&?&[-> ? ?]); auto.
eapply whnf_red_inv in r1; auto.
Lemma reduce_to_prod_complete {Γ t wt} Σ (wfΣ : abstract_env_ext_rel X Σ)
e p :
reduce_to_prod Γ t wt = TypeError_comp e p ->
(forall na a b, red Σ Γ t (tProd na a b) -> False).
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
pose proof (hΣ := hΣ _ _ _ wfΣ).
eapply into_closed_red; fvs.
Equations? reduce_to_ind (Γ : context) (t : term)
(h : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t)
: typing_result_comp (∑ i u l, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ t ⇝ mkApps (tInd i u) l ∥) :=
reduce_to_ind Γ t h with inspect (decompose_app t) := {
| exist (thd, args) eq_decomp with view_indc thd := {
| view_ind_tInd i u => Checked_comp (i; u; args; _);
| view_ind_other thd _ with inspect (reduce_stack RedFlags.default _ X Γ t [] h) := {
| exist (hnft, π) eq with view_indc hnft := {
| view_ind_tInd i' u with inspect (decompose_stack π) := {
| exist (l, _) eq_decomp' => Checked_comp (i'; u; l; _)
};
| view_ind_other _ _ => TypeError_comp (NotAnInductive t) _
}
}
}
}.
assert (Xeq : mkApps (tInd i u) args = t).
2: symmetry; eapply mkApps_decompose_app.
now rewrite <- eq_decomp.
pose proof (hΣ := hΣ _ _ _ wfΣ); sq; eapply (wt_closed_red_refl h).
pose proof (reduce_stack_sound RedFlags.default _ X _ wfΣ _ _ [] h).
assert (π = appstack l []) as ->.
now rewrite zipc_appstack in H.
unfold reduce_stack in eq.
edestruct reduce_stack_full as (?&_&stack_val&?); eauto.
assert (decomp: decompose_stack π = ((decompose_stack π).1, [])).
now destruct decompose_stack.
apply decompose_stack_eq in decomp as ->.
now rewrite <- eq_decomp'.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (hΣ := hΣ _ _ _ wfΣ).
pose proof (reduce_stack_whnf RedFlags.default _ X Γ t [] h _ wfΣ) as wh.
unfold reduce_stack in *.
edestruct reduce_stack_full as ((hd&π')&r'&stack_valid&(notapp&_)); eauto.
apply Req_red in r' as [r'].
unfold Pr in stack_valid.
eapply into_closed_red in r'; fvs.
eapply PCUICContextConversion.closed_red_confluence in r' as (?&r1&r2).
assert (exists args, π' = appstack args []) as (?&->).
exists ((decompose_stack π').1).
assert (decomp: decompose_stack π' = ((decompose_stack π').1, [])).
now rewrite stack_valid; destruct decompose_stack; cbn.
now apply decompose_stack_eq in decomp.
rewrite stack_context_appstack, decompose_stack_appstack in wh.
rewrite zipc_appstack in r2.
eapply whnf_red_inv in r2; eauto.
apply invert_red_mkApps_tInd in r1 as (?&[-> _ ?]); auto.
apply whnf_red_mkApps_inv in r2 as (?&?); auto.
Lemma reduce_to_ind_complete Σ (wfΣ : abstract_env_ext_rel X Σ) Γ ty wat e p :
reduce_to_ind Γ ty wat = TypeError_comp e p ->
forall ind u args,
red Σ Γ ty (mkApps (tInd ind u) args) ->
False.
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
pose proof (hΣ := hΣ _ _ _ wfΣ).
eapply into_closed_red ; fvs.
(* Definition of assumption-only arities (without lets) *)
Definition arity_ass := aname * term.
Fixpoint mkAssumArity (l : list arity_ass) (s : Universe.t) : term :=
match l with
| [] => tSort s
| (na, A) :: l => tProd na A (mkAssumArity l s)
end.
Definition arity_ass_context := rev_map (fun '(na, A) => vass na A).
Lemma assumption_context_arity_ass_context l :
assumption_context (arity_ass_context l).
unfold arity_ass_context.
induction l using MCList.rev_ind; cbn.
rewrite map_app, rev_app_distr.
Lemma mkAssumArity_it_mkProd_or_LetIn (l : list arity_ass) (s : Universe.t) :
mkAssumArity l s = it_mkProd_or_LetIn (arity_ass_context l) (tSort s).
unfold arity_ass_context.
rewrite IHl, it_mkProd_or_LetIn_app; auto.
Lemma isArity_mkAssumArity l s :
isArity (mkAssumArity l s).
induction l as [|(na & A) l IH]; cbn; auto.
Record conv_arity {Γ T} : Type :=
build_conv_arity {
conv_ar_context : list arity_ass;
conv_ar_univ : Universe.t;
conv_ar_red : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ T ⇝ mkAssumArity conv_ar_context conv_ar_univ ∥
}.
Global Arguments conv_arity : clear implicits.
Lemma conv_arity_Is_conv_to_Arity {Γ T} :
is_closed_context Γ ->
is_open_term Γ T ->
conv_arity Γ T ->
forall Σ (wfΣ : abstract_env_ext_rel X Σ), Is_conv_to_Arity Σ Γ T.
intros clΓ clT [asses univ r] Σ wfΣ.
apply isArity_mkAssumArity.
Lemma isArity_red Σ Γ u v :
isArity u ->
red Σ Γ u v ->
isArity v.
induction r using red_rect_n1; [easy|].
eapply isArity_red1; eassumption.
Lemma Is_conv_to_Arity_red Σ {wfΣ : wf Σ} Γ T T' :
Is_conv_to_Arity Σ Γ T ->
Σ ;;; Γ ⊢ T ⇝ T' ->
Is_conv_to_Arity Σ Γ T'.
intros [T'' (redT'' & is_arity)] red.
destruct (PCUICContextConversion.closed_red_confluence red redT'') as (a & reda' & reda'').
eapply isArity_red; eauto.
Local Instance wellfounded Σ wfΣ {normalization:NormalizationIn Σ} : WellFounded (@hnf_subterm_rel _ Σ) :=
@wf_hnf_subterm _ _ _ normalization (heΣ _ X Σ wfΣ).