Library MetaCoq.PCUIC.PCUICConfluence
Lemma red1_eq_context_upto_l Σ Re Γ Δ u v :
RelationClasses.Reflexive Re →
SubstUnivPreserving Re →
red1 Σ Γ u v →
eq_context_upto Re Γ Δ →
∑ v', red1 Σ Δ u v' ×
eq_term_upto_univ Re Re v v'.
Lemma red1_eq_term_upto_univ_l Σ Re Rle Γ u v u' :
RelationClasses.Reflexive Re →
SubstUnivPreserving Re →
RelationClasses.Reflexive Rle →
RelationClasses.Transitive Re →
RelationClasses.Transitive Rle →
RelationClasses.subrelation Re Rle →
eq_term_upto_univ Re Rle u u' →
red1 Σ Γ u v →
∑ v', red1 Σ Γ u' v' ×
eq_term_upto_univ Re Rle v v'.
Lemma red1_eq_context_upto_r Σ Re Γ Δ u v :
RelationClasses.Reflexive Re →
RelationClasses.Symmetric Re →
SubstUnivPreserving Re →
red1 Σ Γ u v →
eq_context_upto Re Δ Γ →
∑ v', red1 Σ Δ u v' ×
eq_term_upto_univ Re Re v' v.
Lemma red1_eq_term_upto_univ_r Σ Re Rle Γ u v u' :
RelationClasses.Reflexive Re →
SubstUnivPreserving Re →
RelationClasses.Reflexive Rle →
RelationClasses.Symmetric Re →
RelationClasses.Transitive Re →
RelationClasses.Transitive Rle →
RelationClasses.subrelation Re Rle →
eq_term_upto_univ Re Rle u' u →
red1 Σ Γ u v →
∑ v', red1 Σ Γ u' v' ×
eq_term_upto_univ Re Rle v' v.
Section RedEq.
Context (Σ : global_env_ext).
Context {Re Rle : universe → universe → Prop}
{refl : RelationClasses.Reflexive Re}
{refl': RelationClasses.Reflexive Rle}
{pres : SubstUnivPreserving Re}
{sym : RelationClasses.Symmetric Re}
{trre : RelationClasses.Transitive Re}
{trle : RelationClasses.Transitive Rle}.
Context (inclre : RelationClasses.subrelation Re Rle).
Lemma red_eq_term_upto_univ_r {Γ T V U} :
eq_term_upto_univ Re Rle T U → red Σ Γ U V →
∑ T', red Σ Γ T T' × eq_term_upto_univ Re Rle T' V.
Lemma red_eq_term_upto_univ_l {Γ u v u'} :
eq_term_upto_univ Re Rle u u' →
red Σ Γ u v →
∑ v',
red Σ Γ u' v' ×
eq_term_upto_univ Re Rle v v'.
End RedEq.
FIXME Equations Derive Bug
Definition clos_refl_trans_sig@{i j} (A : Type@{i}) (R : Relation.relation A)
(index : sigma (fun _ : A ⇒ A)) : Type@{j} :=
Relation.clos_refl_trans@{i j} R (pr1 index) (pr2 index).
Definition clos_refl_trans_sig_pack@{i j} (A : Type@{i}) (R : Relation.relation A) (x H : A)
(clos_refl_trans_var : Relation.clos_refl_trans R x H) :
sigma@{i} (fun index : sigma (fun _ : A ⇒ A) ⇒ Relation.clos_refl_trans@{i j} R (pr1 index) (pr2 index)) :=
({| pr1 := {| pr1 := x; pr2 := H |}; pr2 := clos_refl_trans_var |}).
Instance clos_refl_trans_Signature (A : Type) (R : Relation.relation A) (x H : A)
: Signature (Relation.clos_refl_trans R x H) (sigma (fun _ : A ⇒ A)) (clos_refl_trans_sig A R) :=
clos_refl_trans_sig_pack A R x H.
Definition red1_sig@{} (Σ : global_env) (index : sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term))) :=
let Γ := pr1 index in let H := pr1 (pr2 index) in let H0 := pr2 (pr2 index) in red1 Σ Γ H H0.
Definition red1_sig_pack@{} (Σ : global_env) (Γ : context) (H H0 : term) (red1_var : red1 Σ Γ H H0)
: sigma@{red1u} (fun index : sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term)) ⇒
red1 Σ (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
:=
{| pr1 := {| pr1 := Γ; pr2 := {| pr1 := H; pr2 := H0 |} |}; pr2 := red1_var |}.
Instance red1_Signature@{} (Σ : global_env) (Γ : context) (H H0 : term)
: Signature@{red1u} (red1 Σ Γ H H0) (sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term))) (red1_sig Σ) :=
red1_sig_pack Σ Γ H H0.
(index : sigma (fun _ : A ⇒ A)) : Type@{j} :=
Relation.clos_refl_trans@{i j} R (pr1 index) (pr2 index).
Definition clos_refl_trans_sig_pack@{i j} (A : Type@{i}) (R : Relation.relation A) (x H : A)
(clos_refl_trans_var : Relation.clos_refl_trans R x H) :
sigma@{i} (fun index : sigma (fun _ : A ⇒ A) ⇒ Relation.clos_refl_trans@{i j} R (pr1 index) (pr2 index)) :=
({| pr1 := {| pr1 := x; pr2 := H |}; pr2 := clos_refl_trans_var |}).
Instance clos_refl_trans_Signature (A : Type) (R : Relation.relation A) (x H : A)
: Signature (Relation.clos_refl_trans R x H) (sigma (fun _ : A ⇒ A)) (clos_refl_trans_sig A R) :=
clos_refl_trans_sig_pack A R x H.
Definition red1_sig@{} (Σ : global_env) (index : sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term))) :=
let Γ := pr1 index in let H := pr1 (pr2 index) in let H0 := pr2 (pr2 index) in red1 Σ Γ H H0.
Definition red1_sig_pack@{} (Σ : global_env) (Γ : context) (H H0 : term) (red1_var : red1 Σ Γ H H0)
: sigma@{red1u} (fun index : sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term)) ⇒
red1 Σ (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
:=
{| pr1 := {| pr1 := Γ; pr2 := {| pr1 := H; pr2 := H0 |} |}; pr2 := red1_var |}.
Instance red1_Signature@{} (Σ : global_env) (Γ : context) (H H0 : term)
: Signature@{red1u} (red1 Σ Γ H H0) (sigma (fun _ : context ⇒ sigma (fun _ : term ⇒ term))) (red1_sig Σ) :=
red1_sig_pack Σ Γ H H0.
FIXME Equations
Lemma local_env_telescope P Γ Γ' Δ Δ' :
All2_telescope (on_decl P) Γ Γ' Δ Δ' →
All2_local_env_over P Γ Γ' (List.rev Δ) (List.rev Δ').
Lemma mapi_rec_compose {A B C} (g : nat → B → C) (f : nat → A → B) k l :
mapi_rec g (mapi_rec f l k) k = mapi_rec (fun k x ⇒ g k (f k x)) l k.
Lemma mapi_compose {A B C} (g : nat → B → C) (f : nat → A → B) l :
mapi g (mapi f l) = mapi (fun k x ⇒ g k (f k x)) l.
Lemma mapi_cst_map {A B} (f : A → B) l : mapi (fun _ ⇒ f) l = map f l.
Lemma All_All2_telescopei_gen P (Γ Γ' Δ Δ' : context) (m m' : mfixpoint term) :
(∀ Δ Δ' x y,
All2_local_env_over P Γ Γ' Δ Δ' →
P Γ Γ' x y →
P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y)) →
All2 (on_Trel_eq (P Γ Γ') dtype dname) m m' →
All2_local_env_over P Γ Γ' Δ Δ' →
All2_telescope_n (on_decl P) (fun n : nat ⇒ lift0 n)
(Γ ,,, Δ) (Γ' ,,, Δ') #|Δ|
(map (fun def : def term ⇒ vass (dname def) (dtype def)) m)
(map (fun def : def term ⇒ vass (dname def) (dtype def)) m').
Lemma All_All2_telescopei P (Γ Γ' : context) (m m' : mfixpoint term) :
(∀ Δ Δ' x y,
All2_local_env_over P Γ Γ' Δ Δ' →
P Γ Γ' x y →
P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y)) →
All2 (on_Trel_eq (P Γ Γ') dtype dname) m m' →
All2_telescope_n (on_decl P) (λ n : nat, lift0 n)
Γ Γ' 0
(map (λ def : def term, vass (dname def) (dtype def)) m)
(map (λ def : def term, vass (dname def) (dtype def)) m').
Lemma All2_All2_local_env_fix_context P (Γ Γ' : context) (m m' : mfixpoint term) :
(∀ Δ Δ' x y,
All2_local_env_over P Γ Γ' Δ Δ' →
P Γ Γ' x y →
P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y)) →
All2 (on_Trel_eq (P Γ Γ') dtype dname) m m' →
All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context m) (fix_context m').
Section RedPred.
Context {cf : checker_flags}.
Context {Σ : global_env}.
Context (wfΣ : wf Σ).
Strong substitutivity gives context conversion of reduction!
It cannot be strenghtened to deal with let-ins: pred1 is
precisely not closed by arbitrary reductions in contexts with let-ins.
Lemma pred1_ctx_pred1 Γ Δ Δ' t u :
pred1 Σ (Γ ,,, Δ) (Γ ,,, Δ) t u →
assumption_context Δ →
pred1_ctx Σ (Γ ,,, Δ) (Γ ,,, Δ') →
pred1 Σ (Γ ,,, Δ) (Γ ,,, Δ') t u.
Lemma red1_pred1 Γ : ∀ M N, red1 Σ Γ M N → pred1 Σ Γ Γ M N.
End RedPred.
Section PredRed.
Context {cf : checker_flags}.
Context {Σ : global_env}.
Context (wfΣ : wf Σ).
Lemma weakening_red_0 Γ Γ' M N n :
n = #|Γ'| →
red Σ Γ M N →
red Σ (Γ ,,, Γ') (lift0 n M) (lift0 n N).
Lemma red_abs_alt Γ na M M' N N' : red Σ Γ M M' → red Σ (Γ ,, vass na M) N N' →
red Σ Γ (tLambda na M N) (tLambda na M' N').
Lemma red_letin_alt Γ na d0 d1 t0 t1 b0 b1 :
red Σ Γ d0 d1 → red Σ Γ t0 t1 → red Σ (Γ ,, vdef na d0 t0) b0 b1 →
red Σ Γ (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1).
Lemma red_prod_alt Γ na M M' N N' :
red Σ Γ M M' → red Σ (Γ ,, vass na M') N N' →
red Σ Γ (tProd na M N) (tProd na M' N').
Parallel reduction is included in the reflexive transitive closure of 1-step reduction
Lemma pred1_red Γ Γ' : ∀ M N, pred1 Σ Γ Γ' M N → red Σ Γ M N.
End PredRed.
Lemma clos_t_rt {A} {R : A → A → Type} x y : trans_clos R x y → clos_refl_trans R x y.
Definition commutes {A} (R S : relation A) :=
∀ x y z, R x y → S x z → ∑ w, S y w × R z w.
Section Relations.
Definition clos_rt_monotone {A} (R S : relation A) :
inclusion R S → inclusion (clos_refl_trans R) (clos_refl_trans S).
Lemma relation_equivalence_inclusion {A} (R S : relation A) :
inclusion R S → inclusion S R → relation_equivalence R S.
Lemma clos_rt_disjunction_left {A} (R S : relation A) :
inclusion (clos_refl_trans R)
(clos_refl_trans (relation_disjunction R S)).
Lemma clos_rt_disjunction_right {A} (R S : relation A) :
inclusion (clos_refl_trans S)
(clos_refl_trans (relation_disjunction R S)).
Global Instance clos_rt_trans A R : Transitive (@clos_refl_trans A R).
Global Instance clos_rt_refl A R : Reflexive (@clos_refl_trans A R).
Lemma clos_refl_trans_prod_l {A B} (R : relation A) (S : relation (A × B)) :
(∀ x y b, R x y → S (x, b) (y, b)) →
∀ (x y : A) b,
clos_refl_trans R x y →
clos_refl_trans S (x, b) (y, b).
Lemma clos_refl_trans_prod_r {A B} (R : relation B) (S : relation (A × B)) a :
(∀ x y, R x y → S (a, x) (a, y)) →
∀ (x y : B),
clos_refl_trans R x y →
clos_refl_trans S (a, x) (a, y).
Lemma clos_rt_t_incl {A} {R : relation A} `{Reflexive A R} :
inclusion (clos_refl_trans R) (trans_clos R).
Lemma clos_t_rt_incl {A} {R : relation A} `{Reflexive A R} :
inclusion (trans_clos R) (clos_refl_trans R).
Lemma clos_t_rt_equiv {A} {R} `{Reflexive A R} :
relation_equivalence (trans_clos R) (clos_refl_trans R).
Global Instance relation_disjunction_refl_l {A} {R S : relation A} :
Reflexive R → Reflexive (relation_disjunction R S).
Global Instance relation_disjunction_refl_r {A} {R S : relation A} :
Reflexive S → Reflexive (relation_disjunction R S).
End Relations.
Section AbstractConfluence.
Section Definitions.
Context {A : Type}.
Definition joinable (R : A → A → Type) (x y : A) := ∑ z, R x z × R y z.
Definition diamond (R : A → A → Type) := ∀ x y z, R x y → R x z → joinable R y z.
Definition confluent (R : relation A) := diamond (clos_refl_trans R).
End Definitions.
Global Instance joinable_proper A :
CMorphisms.Proper (relation_equivalence ==> relation_equivalence)%signature (@joinable A).
Global Instance diamond_proper A : CMorphisms.Proper (relation_equivalence ==> iffT)%signature (@diamond A).
Lemma clos_rt_proper A : CMorphisms.Proper (relation_equivalence ==> relation_equivalence) (@clos_refl_trans A).
Global Instance confluent_proper A : CMorphisms.Proper (relation_equivalence ==> iffT)%signature (@confluent A).
Lemma sandwich {A} (R S : A → A → Type) :
inclusion R S → inclusion S (clos_refl_trans R) →
(iffT (confluent S) (confluent R)).
Section Diamond.
Context {A} {R S : relation A}.
Context (sc : diamond R).
Lemma diamond_t1n_t_confluent t u v :
trans_clos_1n R t u →
R t v →
∑ t', trans_clos_1n R u t' × trans_clos_1n R v t'.
Lemma diamond_t1n_t1n_confluent {t u v} :
trans_clos_1n R t u →
trans_clos_1n R t v →
∑ t', trans_clos_1n R u t' × trans_clos_1n R v t'.
Lemma diamond_t_t_confluent {t u v} :
trans_clos R t u →
trans_clos R t v →
∑ t', trans_clos R u t' × trans_clos R v t'.
Lemma commutes_diamonds_diamond :
commutes R S → diamond S → diamond (relation_disjunction R S).
Lemma commutes_disj_joinable :
commutes R S → confluent R → confluent S →
∀ x y z, relation_disjunction R S x y →
relation_disjunction R S x z →
joinable (clos_refl_trans (relation_disjunction R S)) y z.
End Diamond.
Theorem diamond_confluent `{Hrefl : Reflexive A R} : diamond R → confluent R.
Corollary confluent_union {A} {R S : relation A} :
Reflexive R →
commutes R S → diamond R → diamond S → confluent (relation_disjunction R S).
End AbstractConfluence.
Lemma red_pred {cf:checker_flags} {Σ Γ t u} : wf Σ → clos_refl_trans (red1 Σ Γ) t u → clos_refl_trans (pred1 Σ Γ Γ) t u.
Section RedConfluence.
Context {cf : checker_flags}.
Context {Σ} (wfΣ : wf Σ).
Instance pred1_refl Γ : Reflexive (pred1 Σ Γ Γ).
Definition pred1_rel : (context × term) → (context × term) → Type :=
fun t u ⇒ pred1 Σ (fst t) (fst u) (snd t) (snd u).
Instance pred1_rel_refl : Reflexive pred1_rel.
Lemma red1_weak_confluence Γ t u v :
red1 Σ Γ t u → red1 Σ Γ t v →
∑ t', red Σ Γ u t' × red Σ Γ v t'.
Lemma diamond_pred1_rel : diamond pred1_rel.
Lemma pred1_rel_confluent : confluent pred1_rel.
Lemma red_trans_clos_pred1 Γ t u :
red Σ Γ t u →
trans_clos pred1_rel (Γ, t) (Γ, u).
Definition on_one_decl (P : context → term → term → Type) (Γ : context) (b : option (term × term)) (t t' : term) :=
match b with
| Some (b0, b') ⇒ ((P Γ b0 b' × (t = t')) + (P Γ t t' × (b0 = b')))%type
| None ⇒ P Γ t t'
end.
Section OnOne_local_2.
Context (P : ∀ (Γ : context), option (term × term) → term → term → Type).
End PredRed.
Lemma clos_t_rt {A} {R : A → A → Type} x y : trans_clos R x y → clos_refl_trans R x y.
Definition commutes {A} (R S : relation A) :=
∀ x y z, R x y → S x z → ∑ w, S y w × R z w.
Section Relations.
Definition clos_rt_monotone {A} (R S : relation A) :
inclusion R S → inclusion (clos_refl_trans R) (clos_refl_trans S).
Lemma relation_equivalence_inclusion {A} (R S : relation A) :
inclusion R S → inclusion S R → relation_equivalence R S.
Lemma clos_rt_disjunction_left {A} (R S : relation A) :
inclusion (clos_refl_trans R)
(clos_refl_trans (relation_disjunction R S)).
Lemma clos_rt_disjunction_right {A} (R S : relation A) :
inclusion (clos_refl_trans S)
(clos_refl_trans (relation_disjunction R S)).
Global Instance clos_rt_trans A R : Transitive (@clos_refl_trans A R).
Global Instance clos_rt_refl A R : Reflexive (@clos_refl_trans A R).
Lemma clos_refl_trans_prod_l {A B} (R : relation A) (S : relation (A × B)) :
(∀ x y b, R x y → S (x, b) (y, b)) →
∀ (x y : A) b,
clos_refl_trans R x y →
clos_refl_trans S (x, b) (y, b).
Lemma clos_refl_trans_prod_r {A B} (R : relation B) (S : relation (A × B)) a :
(∀ x y, R x y → S (a, x) (a, y)) →
∀ (x y : B),
clos_refl_trans R x y →
clos_refl_trans S (a, x) (a, y).
Lemma clos_rt_t_incl {A} {R : relation A} `{Reflexive A R} :
inclusion (clos_refl_trans R) (trans_clos R).
Lemma clos_t_rt_incl {A} {R : relation A} `{Reflexive A R} :
inclusion (trans_clos R) (clos_refl_trans R).
Lemma clos_t_rt_equiv {A} {R} `{Reflexive A R} :
relation_equivalence (trans_clos R) (clos_refl_trans R).
Global Instance relation_disjunction_refl_l {A} {R S : relation A} :
Reflexive R → Reflexive (relation_disjunction R S).
Global Instance relation_disjunction_refl_r {A} {R S : relation A} :
Reflexive S → Reflexive (relation_disjunction R S).
End Relations.
Section AbstractConfluence.
Section Definitions.
Context {A : Type}.
Definition joinable (R : A → A → Type) (x y : A) := ∑ z, R x z × R y z.
Definition diamond (R : A → A → Type) := ∀ x y z, R x y → R x z → joinable R y z.
Definition confluent (R : relation A) := diamond (clos_refl_trans R).
End Definitions.
Global Instance joinable_proper A :
CMorphisms.Proper (relation_equivalence ==> relation_equivalence)%signature (@joinable A).
Global Instance diamond_proper A : CMorphisms.Proper (relation_equivalence ==> iffT)%signature (@diamond A).
Lemma clos_rt_proper A : CMorphisms.Proper (relation_equivalence ==> relation_equivalence) (@clos_refl_trans A).
Global Instance confluent_proper A : CMorphisms.Proper (relation_equivalence ==> iffT)%signature (@confluent A).
Lemma sandwich {A} (R S : A → A → Type) :
inclusion R S → inclusion S (clos_refl_trans R) →
(iffT (confluent S) (confluent R)).
Section Diamond.
Context {A} {R S : relation A}.
Context (sc : diamond R).
Lemma diamond_t1n_t_confluent t u v :
trans_clos_1n R t u →
R t v →
∑ t', trans_clos_1n R u t' × trans_clos_1n R v t'.
Lemma diamond_t1n_t1n_confluent {t u v} :
trans_clos_1n R t u →
trans_clos_1n R t v →
∑ t', trans_clos_1n R u t' × trans_clos_1n R v t'.
Lemma diamond_t_t_confluent {t u v} :
trans_clos R t u →
trans_clos R t v →
∑ t', trans_clos R u t' × trans_clos R v t'.
Lemma commutes_diamonds_diamond :
commutes R S → diamond S → diamond (relation_disjunction R S).
Lemma commutes_disj_joinable :
commutes R S → confluent R → confluent S →
∀ x y z, relation_disjunction R S x y →
relation_disjunction R S x z →
joinable (clos_refl_trans (relation_disjunction R S)) y z.
End Diamond.
Theorem diamond_confluent `{Hrefl : Reflexive A R} : diamond R → confluent R.
Corollary confluent_union {A} {R S : relation A} :
Reflexive R →
commutes R S → diamond R → diamond S → confluent (relation_disjunction R S).
End AbstractConfluence.
Lemma red_pred {cf:checker_flags} {Σ Γ t u} : wf Σ → clos_refl_trans (red1 Σ Γ) t u → clos_refl_trans (pred1 Σ Γ Γ) t u.
Section RedConfluence.
Context {cf : checker_flags}.
Context {Σ} (wfΣ : wf Σ).
Instance pred1_refl Γ : Reflexive (pred1 Σ Γ Γ).
Definition pred1_rel : (context × term) → (context × term) → Type :=
fun t u ⇒ pred1 Σ (fst t) (fst u) (snd t) (snd u).
Instance pred1_rel_refl : Reflexive pred1_rel.
Lemma red1_weak_confluence Γ t u v :
red1 Σ Γ t u → red1 Σ Γ t v →
∑ t', red Σ Γ u t' × red Σ Γ v t'.
Lemma diamond_pred1_rel : diamond pred1_rel.
Lemma pred1_rel_confluent : confluent pred1_rel.
Lemma red_trans_clos_pred1 Γ t u :
red Σ Γ t u →
trans_clos pred1_rel (Γ, t) (Γ, u).
Definition on_one_decl (P : context → term → term → Type) (Γ : context) (b : option (term × term)) (t t' : term) :=
match b with
| Some (b0, b') ⇒ ((P Γ b0 b' × (t = t')) + (P Γ t t' × (b0 = b')))%type
| None ⇒ P Γ t t'
end.
Section OnOne_local_2.
Context (P : ∀ (Γ : context), option (term × term) → term → term → Type).
We allow alpha-conversion
Inductive OnOne2_local_env : context → context → Type :=
| localenv2_cons_abs Γ na t t' :
P Γ None t t' →
OnOne2_local_env (Γ ,, vass na t) (Γ ,, vass na t')
| localenv2_cons_def Γ na b b' t t' :
P Γ (Some (b, b')) t t' →
OnOne2_local_env (Γ ,, vdef na b t) (Γ ,, vdef na b' t')
| localenv2_cons_tl Γ Γ' d :
OnOne2_local_env Γ Γ' →
OnOne2_local_env (Γ ,, d) (Γ' ,, d).
End OnOne_local_2.
Inductive clos_refl_trans_ctx_decl (R : relation context_decl) (x : context_decl) : context_decl → Type :=
rt_ctx_decl_step : ∀ y, R x y → clos_refl_trans_ctx_decl R x y
| rt_ctx_decl_refl y : decl_body x = decl_body y → decl_type x = decl_type y → clos_refl_trans_ctx_decl R x y
| rt_ctx_decl_trans : ∀ y z, clos_refl_trans_ctx_decl R x y → clos_refl_trans_ctx_decl R y z →
clos_refl_trans_ctx_decl R x z.
Inductive eq_context_upto_names : context → context → Type :=
| eq_context_nil : eq_context_upto_names [] []
| eq_context_decl x y Γ Γ' :
decl_body x = decl_body y → decl_type x = decl_type y →
eq_context_upto_names Γ Γ' →
eq_context_upto_names (Γ ,, x) (Γ' ,, y).
Global Instance eq_context_upto_names_refl : Reflexive eq_context_upto_names.
Global Instance eq_context_upto_names_sym : Symmetric eq_context_upto_names.
Global Instance eq_context_upto_names_trans : Transitive eq_context_upto_names.
Inductive clos_refl_trans_ctx (R : relation context) (x : context) : context → Type :=
| rt_ctx_step : ∀ y, R x y → clos_refl_trans_ctx R x y
| rt_ctx_refl y : eq_context_upto_names x y → clos_refl_trans_ctx R x y
| rt_ctx_trans : ∀ y z, clos_refl_trans_ctx R x y → clos_refl_trans_ctx R y z → clos_refl_trans_ctx R x z.
Global Instance clos_refl_trans_ctx_refl R :
Reflexive (clos_refl_trans_ctx R).
Global Instance clos_refl_trans_ctx_trans R : Transitive (clos_refl_trans_ctx R).
Definition red1_ctx := (OnOne2_local_env (on_one_decl (fun Δ t t' ⇒ red1 Σ Δ t t'))).
Definition red1_rel : relation (context × term) :=
relation_disjunction (fun '(Γ, t) '(Δ, u) ⇒ (red1 Σ Γ t u × (Γ = Δ)))%type
(fun '(Γ, t) '(Δ, u) ⇒ (red1_ctx Γ Δ × (t = u)))%type.
Definition red_ctx : relation context :=
All2_local_env (on_decl (fun Γ Δ t u ⇒ red Σ Γ t u)).
Lemma red1_ctx_pred1_ctx Γ Γ' : red1_ctx Γ Γ' → pred1_ctx Σ Γ Γ'.
Lemma pred1_ctx_red_ctx Γ Γ' : pred1_ctx Σ Γ Γ' → red_ctx Γ Γ'.
Definition red_rel_ctx :=
fun '(Γ, t) '(Δ, u) ⇒
(red Σ Γ t u × red_ctx Γ Δ)%type.
Lemma pred1_red' Γ Γ' : ∀ M N, pred1 Σ Γ Γ' M N → red_rel_ctx (Γ, M) (Γ', N).
Lemma clos_rt_OnOne2_local_env_incl R :
inclusion (OnOne2_local_env (on_one_decl (fun Δ ⇒ clos_refl_trans (R Δ))))
(clos_refl_trans (OnOne2_local_env (on_one_decl R))).
Lemma clos_rt_OnOne2_local_env_ctx_incl R :
inclusion (clos_refl_trans (OnOne2_local_env (on_one_decl R)))
(clos_refl_trans_ctx (OnOne2_local_env (on_one_decl R))).
Lemma OnOne2_local_env_impl R S :
(∀ Δ, inclusion (R Δ) (S Δ)) →
inclusion (OnOne2_local_env (on_one_decl R))
(OnOne2_local_env (on_one_decl S)).
Lemma red_ctx_clos_rt_red1_ctx : inclusion red_ctx (clos_refl_trans_ctx red1_ctx).
Inductive clos_refl_trans_ctx_t (R : relation (context × term)) (x : context × term) : context × term → Type :=
| rt_ctx_t_step : ∀ y, R x y → clos_refl_trans_ctx_t R x y
| rt_ctx_t_refl y : eq_context_upto_names (fst x) (fst y) → snd x = snd y → clos_refl_trans_ctx_t R x y
| rt_ctx_t_trans : ∀ y z, clos_refl_trans_ctx_t R x y → clos_refl_trans_ctx_t R y z → clos_refl_trans_ctx_t R x z.
Global Instance clos_refl_trans_ctx_t_refl R :
Reflexive (clos_refl_trans_ctx_t R).
Global Instance clos_refl_trans_ctx_t_trans R : Transitive (clos_refl_trans_ctx_t R).
Definition clos_rt_ctx_t_monotone (R S : relation _) :
inclusion R S → inclusion (clos_refl_trans_ctx_t R) (clos_refl_trans_ctx_t S).
Lemma clos_rt_ctx_t_disjunction_left (R S : relation _) :
inclusion (clos_refl_trans_ctx_t R)
(clos_refl_trans_ctx_t (relation_disjunction R S)).
Lemma clos_rt_ctx_t_disjunction_right (R S : relation _) :
inclusion (clos_refl_trans_ctx_t S)
(clos_refl_trans_ctx_t (relation_disjunction R S)).
Lemma clos_refl_trans_ctx_t_prod_l (R : relation _) (S : relation _) :
(∀ x y b, R x y → S (x, b) (y, b)) →
∀ x y b,
clos_refl_trans_ctx R x y →
clos_refl_trans_ctx_t S (x, b) (y, b).
Lemma clos_refl_trans_ctx_t_prod_r (R : relation term) (S : relation (context × term)) a :
(∀ x y, R x y → S (a, x) (a, y)) →
∀ x y,
clos_refl_trans R x y →
clos_refl_trans_ctx_t S (a, x) (a, y).
Lemma clos_rt_red1_rel_ctx_rt_ctx_red1_rel : inclusion red_rel_ctx (clos_refl_trans_ctx_t red1_rel).
Definition red1_rel_alpha : relation (context × term) :=
relation_disjunction (fun '(Γ, t) '(Δ, u) ⇒ (red1 Σ Γ t u × (Γ = Δ)))%type
(relation_disjunction
(fun '(Γ, t) '(Δ, u) ⇒ ((red1_ctx Γ Δ × (t = u))))
(fun '(Γ, t) '(Δ, u) ⇒ ((eq_context_upto_names Γ Δ × (t = u)))))%type.
Lemma clos_rt_red1_rel_rt_ctx : inclusion (clos_refl_trans red1_rel) (clos_refl_trans_ctx_t red1_rel).
Lemma red1_rel_alpha_pred1_rel : inclusion red1_rel_alpha pred1_rel.
Lemma pred1_rel_red1_rel_alpha : inclusion pred1_rel (clos_refl_trans red1_rel_alpha).
Lemma pred_rel_confluent : confluent red1_rel_alpha.
Lemma clos_refl_trans_out Γ x y :
clos_refl_trans (red1 Σ Γ) x y → clos_refl_trans red1_rel (Γ, x) (Γ, y).
Lemma red_red_ctx Γ Δ t u :
red Σ Γ t u →
red_ctx Δ Γ →
red Σ Δ t u.
Lemma clos_red_rel_out x y :
clos_refl_trans red1_rel x y →
clos_refl_trans pred1_rel x y.
Lemma red1_rel_alpha_red1_rel : inclusion (clos_refl_trans red1_rel_alpha) (clos_refl_trans_ctx_t red1_rel).
Lemma red1_rel_alpha_red1_rel_inv : inclusion (clos_refl_trans_ctx_t red1_rel) (clos_refl_trans red1_rel_alpha).
Lemma clos_red_rel_out_inv x y :
clos_refl_trans pred1_rel x y →
clos_refl_trans red1_rel_alpha x y.
Global Instance red_ctx_refl : Reflexive red_ctx.
Global Instance red_ctx_trans : Transitive red_ctx.
Lemma clos_rt_red1_rel_red1 x y :
clos_refl_trans red1_rel x y →
red_ctx (fst x) (fst y) ×
clos_refl_trans (red1 Σ (fst x)) (snd x) (snd y).
Lemma decl_body_eq_context_upto_names Γ Γ' n d :
option_map decl_body (nth_error Γ n) = Some d →
eq_context_upto_names Γ Γ' →
option_map decl_body (nth_error Γ' n) = Some d.
Lemma decl_type_eq_context_upto_names Γ Γ' n d :
option_map decl_type (nth_error Γ n) = Some d →
eq_context_upto_names Γ Γ' →
option_map decl_type (nth_error Γ' n) = Some d.
Lemma eq_context_upto_names_app Γ Γ' Δ :
eq_context_upto_names Γ Γ' →
eq_context_upto_names (Γ ,,, Δ) (Γ' ,,, Δ).
Lemma red1_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
red1 Σ Γ t u →
red1 Σ Γ' t u.
Lemma clos_rt_red1_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
clos_refl_trans (red1 Σ Γ) t u →
clos_refl_trans (red1 Σ Γ') t u.
Lemma red_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
red Σ Γ t u →
red Σ Γ' t u.
Lemma eq_context_upto_names_red_ctx Γ Δ Γ' Δ' :
eq_context_upto_names Γ Γ' →
eq_context_upto_names Δ Δ' →
red_ctx Γ Δ →
red_ctx Γ' Δ'.
Instance proper_red_ctx :
Proper (eq_context_upto_names ==> eq_context_upto_names ==> isEquiv) red_ctx.
Lemma clos_rt_red1_alpha_out x y :
clos_refl_trans red1_rel_alpha x y →
red_ctx (fst x) (fst y) ×
clos_refl_trans (red1 Σ (fst x)) (snd x) (snd y).
Lemma clos_rt_red1_red1_rel_alpha Γ x y :
clos_refl_trans (red1 Σ Γ) x y → clos_refl_trans red1_rel_alpha (Γ, x) (Γ, y).
Lemma red1_confluent Γ : confluent (red1 Σ Γ).
Lemma pred_red {Γ t u} :
clos_refl_trans (pred1 Σ Γ Γ) t u →
clos_refl_trans (red1 Σ Γ) t u.
End RedConfluence.
Section ConfluenceFacts.
Context {cf : checker_flags}.
Context (Σ : global_env) (wfΣ : wf Σ).
Lemma red_mkApps_tConstruct (Γ : context)
ind pars k (args : list term) c :
red Σ Γ (mkApps (tConstruct ind pars k) args) c →
∑ args' : list term,
(c = mkApps (tConstruct ind pars k) args') × (All2 (red Σ Γ) args args').
Lemma red_mkApps_tInd (Γ : context)
ind u (args : list term) c :
red Σ Γ (mkApps (tInd ind u) args) c →
∑ args' : list term,
(c = mkApps (tInd ind u) args') × (All2 (red Σ Γ) args args').
Lemma red_mkApps_tConst_axiom (Γ : context)
cst u (args : list term) cb c :
declared_constant Σ cst cb → cst_body cb = None →
red Σ Γ (mkApps (tConst cst u) args) c →
∑ args' : list term,
(c = mkApps (tConst cst u) args') × (All2 (red Σ Γ) args args').
Lemma clos_rt_red1_ctx_red_ctx :
inclusion (clos_refl_trans (@red1_ctx Σ)) (@red_ctx Σ).
Lemma red_confluence {Γ t u v} :
red Σ Γ t u → red Σ Γ t v →
∑ v', red Σ Γ u v' × red Σ Γ v v'.
End ConfluenceFacts.
| localenv2_cons_abs Γ na t t' :
P Γ None t t' →
OnOne2_local_env (Γ ,, vass na t) (Γ ,, vass na t')
| localenv2_cons_def Γ na b b' t t' :
P Γ (Some (b, b')) t t' →
OnOne2_local_env (Γ ,, vdef na b t) (Γ ,, vdef na b' t')
| localenv2_cons_tl Γ Γ' d :
OnOne2_local_env Γ Γ' →
OnOne2_local_env (Γ ,, d) (Γ' ,, d).
End OnOne_local_2.
Inductive clos_refl_trans_ctx_decl (R : relation context_decl) (x : context_decl) : context_decl → Type :=
rt_ctx_decl_step : ∀ y, R x y → clos_refl_trans_ctx_decl R x y
| rt_ctx_decl_refl y : decl_body x = decl_body y → decl_type x = decl_type y → clos_refl_trans_ctx_decl R x y
| rt_ctx_decl_trans : ∀ y z, clos_refl_trans_ctx_decl R x y → clos_refl_trans_ctx_decl R y z →
clos_refl_trans_ctx_decl R x z.
Inductive eq_context_upto_names : context → context → Type :=
| eq_context_nil : eq_context_upto_names [] []
| eq_context_decl x y Γ Γ' :
decl_body x = decl_body y → decl_type x = decl_type y →
eq_context_upto_names Γ Γ' →
eq_context_upto_names (Γ ,, x) (Γ' ,, y).
Global Instance eq_context_upto_names_refl : Reflexive eq_context_upto_names.
Global Instance eq_context_upto_names_sym : Symmetric eq_context_upto_names.
Global Instance eq_context_upto_names_trans : Transitive eq_context_upto_names.
Inductive clos_refl_trans_ctx (R : relation context) (x : context) : context → Type :=
| rt_ctx_step : ∀ y, R x y → clos_refl_trans_ctx R x y
| rt_ctx_refl y : eq_context_upto_names x y → clos_refl_trans_ctx R x y
| rt_ctx_trans : ∀ y z, clos_refl_trans_ctx R x y → clos_refl_trans_ctx R y z → clos_refl_trans_ctx R x z.
Global Instance clos_refl_trans_ctx_refl R :
Reflexive (clos_refl_trans_ctx R).
Global Instance clos_refl_trans_ctx_trans R : Transitive (clos_refl_trans_ctx R).
Definition red1_ctx := (OnOne2_local_env (on_one_decl (fun Δ t t' ⇒ red1 Σ Δ t t'))).
Definition red1_rel : relation (context × term) :=
relation_disjunction (fun '(Γ, t) '(Δ, u) ⇒ (red1 Σ Γ t u × (Γ = Δ)))%type
(fun '(Γ, t) '(Δ, u) ⇒ (red1_ctx Γ Δ × (t = u)))%type.
Definition red_ctx : relation context :=
All2_local_env (on_decl (fun Γ Δ t u ⇒ red Σ Γ t u)).
Lemma red1_ctx_pred1_ctx Γ Γ' : red1_ctx Γ Γ' → pred1_ctx Σ Γ Γ'.
Lemma pred1_ctx_red_ctx Γ Γ' : pred1_ctx Σ Γ Γ' → red_ctx Γ Γ'.
Definition red_rel_ctx :=
fun '(Γ, t) '(Δ, u) ⇒
(red Σ Γ t u × red_ctx Γ Δ)%type.
Lemma pred1_red' Γ Γ' : ∀ M N, pred1 Σ Γ Γ' M N → red_rel_ctx (Γ, M) (Γ', N).
Lemma clos_rt_OnOne2_local_env_incl R :
inclusion (OnOne2_local_env (on_one_decl (fun Δ ⇒ clos_refl_trans (R Δ))))
(clos_refl_trans (OnOne2_local_env (on_one_decl R))).
Lemma clos_rt_OnOne2_local_env_ctx_incl R :
inclusion (clos_refl_trans (OnOne2_local_env (on_one_decl R)))
(clos_refl_trans_ctx (OnOne2_local_env (on_one_decl R))).
Lemma OnOne2_local_env_impl R S :
(∀ Δ, inclusion (R Δ) (S Δ)) →
inclusion (OnOne2_local_env (on_one_decl R))
(OnOne2_local_env (on_one_decl S)).
Lemma red_ctx_clos_rt_red1_ctx : inclusion red_ctx (clos_refl_trans_ctx red1_ctx).
Inductive clos_refl_trans_ctx_t (R : relation (context × term)) (x : context × term) : context × term → Type :=
| rt_ctx_t_step : ∀ y, R x y → clos_refl_trans_ctx_t R x y
| rt_ctx_t_refl y : eq_context_upto_names (fst x) (fst y) → snd x = snd y → clos_refl_trans_ctx_t R x y
| rt_ctx_t_trans : ∀ y z, clos_refl_trans_ctx_t R x y → clos_refl_trans_ctx_t R y z → clos_refl_trans_ctx_t R x z.
Global Instance clos_refl_trans_ctx_t_refl R :
Reflexive (clos_refl_trans_ctx_t R).
Global Instance clos_refl_trans_ctx_t_trans R : Transitive (clos_refl_trans_ctx_t R).
Definition clos_rt_ctx_t_monotone (R S : relation _) :
inclusion R S → inclusion (clos_refl_trans_ctx_t R) (clos_refl_trans_ctx_t S).
Lemma clos_rt_ctx_t_disjunction_left (R S : relation _) :
inclusion (clos_refl_trans_ctx_t R)
(clos_refl_trans_ctx_t (relation_disjunction R S)).
Lemma clos_rt_ctx_t_disjunction_right (R S : relation _) :
inclusion (clos_refl_trans_ctx_t S)
(clos_refl_trans_ctx_t (relation_disjunction R S)).
Lemma clos_refl_trans_ctx_t_prod_l (R : relation _) (S : relation _) :
(∀ x y b, R x y → S (x, b) (y, b)) →
∀ x y b,
clos_refl_trans_ctx R x y →
clos_refl_trans_ctx_t S (x, b) (y, b).
Lemma clos_refl_trans_ctx_t_prod_r (R : relation term) (S : relation (context × term)) a :
(∀ x y, R x y → S (a, x) (a, y)) →
∀ x y,
clos_refl_trans R x y →
clos_refl_trans_ctx_t S (a, x) (a, y).
Lemma clos_rt_red1_rel_ctx_rt_ctx_red1_rel : inclusion red_rel_ctx (clos_refl_trans_ctx_t red1_rel).
Definition red1_rel_alpha : relation (context × term) :=
relation_disjunction (fun '(Γ, t) '(Δ, u) ⇒ (red1 Σ Γ t u × (Γ = Δ)))%type
(relation_disjunction
(fun '(Γ, t) '(Δ, u) ⇒ ((red1_ctx Γ Δ × (t = u))))
(fun '(Γ, t) '(Δ, u) ⇒ ((eq_context_upto_names Γ Δ × (t = u)))))%type.
Lemma clos_rt_red1_rel_rt_ctx : inclusion (clos_refl_trans red1_rel) (clos_refl_trans_ctx_t red1_rel).
Lemma red1_rel_alpha_pred1_rel : inclusion red1_rel_alpha pred1_rel.
Lemma pred1_rel_red1_rel_alpha : inclusion pred1_rel (clos_refl_trans red1_rel_alpha).
Lemma pred_rel_confluent : confluent red1_rel_alpha.
Lemma clos_refl_trans_out Γ x y :
clos_refl_trans (red1 Σ Γ) x y → clos_refl_trans red1_rel (Γ, x) (Γ, y).
Lemma red_red_ctx Γ Δ t u :
red Σ Γ t u →
red_ctx Δ Γ →
red Σ Δ t u.
Lemma clos_red_rel_out x y :
clos_refl_trans red1_rel x y →
clos_refl_trans pred1_rel x y.
Lemma red1_rel_alpha_red1_rel : inclusion (clos_refl_trans red1_rel_alpha) (clos_refl_trans_ctx_t red1_rel).
Lemma red1_rel_alpha_red1_rel_inv : inclusion (clos_refl_trans_ctx_t red1_rel) (clos_refl_trans red1_rel_alpha).
Lemma clos_red_rel_out_inv x y :
clos_refl_trans pred1_rel x y →
clos_refl_trans red1_rel_alpha x y.
Global Instance red_ctx_refl : Reflexive red_ctx.
Global Instance red_ctx_trans : Transitive red_ctx.
Lemma clos_rt_red1_rel_red1 x y :
clos_refl_trans red1_rel x y →
red_ctx (fst x) (fst y) ×
clos_refl_trans (red1 Σ (fst x)) (snd x) (snd y).
Lemma decl_body_eq_context_upto_names Γ Γ' n d :
option_map decl_body (nth_error Γ n) = Some d →
eq_context_upto_names Γ Γ' →
option_map decl_body (nth_error Γ' n) = Some d.
Lemma decl_type_eq_context_upto_names Γ Γ' n d :
option_map decl_type (nth_error Γ n) = Some d →
eq_context_upto_names Γ Γ' →
option_map decl_type (nth_error Γ' n) = Some d.
Lemma eq_context_upto_names_app Γ Γ' Δ :
eq_context_upto_names Γ Γ' →
eq_context_upto_names (Γ ,,, Δ) (Γ' ,,, Δ).
Lemma red1_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
red1 Σ Γ t u →
red1 Σ Γ' t u.
Lemma clos_rt_red1_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
clos_refl_trans (red1 Σ Γ) t u →
clos_refl_trans (red1 Σ Γ') t u.
Lemma red_eq_context_upto_names Γ Γ' t u :
eq_context_upto_names Γ Γ' →
red Σ Γ t u →
red Σ Γ' t u.
Lemma eq_context_upto_names_red_ctx Γ Δ Γ' Δ' :
eq_context_upto_names Γ Γ' →
eq_context_upto_names Δ Δ' →
red_ctx Γ Δ →
red_ctx Γ' Δ'.
Instance proper_red_ctx :
Proper (eq_context_upto_names ==> eq_context_upto_names ==> isEquiv) red_ctx.
Lemma clos_rt_red1_alpha_out x y :
clos_refl_trans red1_rel_alpha x y →
red_ctx (fst x) (fst y) ×
clos_refl_trans (red1 Σ (fst x)) (snd x) (snd y).
Lemma clos_rt_red1_red1_rel_alpha Γ x y :
clos_refl_trans (red1 Σ Γ) x y → clos_refl_trans red1_rel_alpha (Γ, x) (Γ, y).
Lemma red1_confluent Γ : confluent (red1 Σ Γ).
Lemma pred_red {Γ t u} :
clos_refl_trans (pred1 Σ Γ Γ) t u →
clos_refl_trans (red1 Σ Γ) t u.
End RedConfluence.
Section ConfluenceFacts.
Context {cf : checker_flags}.
Context (Σ : global_env) (wfΣ : wf Σ).
Lemma red_mkApps_tConstruct (Γ : context)
ind pars k (args : list term) c :
red Σ Γ (mkApps (tConstruct ind pars k) args) c →
∑ args' : list term,
(c = mkApps (tConstruct ind pars k) args') × (All2 (red Σ Γ) args args').
Lemma red_mkApps_tInd (Γ : context)
ind u (args : list term) c :
red Σ Γ (mkApps (tInd ind u) args) c →
∑ args' : list term,
(c = mkApps (tInd ind u) args') × (All2 (red Σ Γ) args args').
Lemma red_mkApps_tConst_axiom (Γ : context)
cst u (args : list term) cb c :
declared_constant Σ cst cb → cst_body cb = None →
red Σ Γ (mkApps (tConst cst u) args) c →
∑ args' : list term,
(c = mkApps (tConst cst u) args') × (All2 (red Σ Γ) args args').
Lemma clos_rt_red1_ctx_red_ctx :
inclusion (clos_refl_trans (@red1_ctx Σ)) (@red_ctx Σ).
Lemma red_confluence {Γ t u v} :
red Σ Γ t u → red Σ Γ t v →
∑ v', red Σ Γ u v' × red Σ Γ v v'.
End ConfluenceFacts.
We can now derive transitivity of the conversion relation