Library MetaCoq.PCUIC.PCUICConversion
Instance cumul_trans {cf:checker_flags} (Σ : global_env_ext) Γ :
wf Σ → Transitive (cumul Σ Γ).
Instance conv_trans {cf:checker_flags} (Σ : global_env_ext) Γ :
wf Σ → Transitive (PCUICTyping.conv Σ Γ).
Instance conv_sym {cf:checker_flags} (Σ : global_env_ext) Γ :
wf Σ → Symmetric (PCUICTyping.conv Σ Γ).
Instance conv_alt_reflexive {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Reflexive (conv_alt Σ Γ).
Instance conv_alt_symmetric {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Symmetric (conv_alt Σ Γ).
Instance conv_alt_transitive {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Transitive (conv_alt Σ Γ).
Instance cumul_reflexive {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Reflexive (cumul Σ Γ).
Instance cumul_transitive {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Transitive (cumul Σ Γ).
Lemma congr_cumul_prod : ∀ `{checker_flags} Σ Γ na na' M1 M2 N1 N2,
Σ ;;; Γ |- M1 == N1 →
Σ ;;; (Γ ,, vass na M1) |- M2 ≤ N2 →
Σ ;;; Γ |- (tProd na M1 M2) ≤ (tProd na' N1 N2).
Lemma cumul_Sort_inv {cf:checker_flags} Σ Γ s s' :
Σ ;;; Γ |- tSort s ≤ tSort s' → leq_universe (global_ext_constraints Σ) s s'.
Lemma cumul_Sort_Prod_inv {cf:checker_flags} Σ Γ s na dom codom :
Σ ;;; Γ |- tSort s ≤ tProd na dom codom → False.
Lemma cumul_Sort_l_inv {cf:checker_flags} Σ Γ s T :
Σ ;;; Γ |- tSort s ≤ T →
∑ s', red Σ Γ T (tSort s') × leq_universe Σ s s'.
Lemma cumul_Sort_r_inv {cf:checker_flags} Σ Γ s T :
Σ ;;; Γ |- T ≤ tSort s →
∑ s', red Σ Γ T (tSort s') × leq_universe Σ s' s.
Lemma cumul_LetIn_l_inv {cf:checker_flags} (Σ : global_env_ext) Γ na b B codom T :
wf Σ →
Σ ;;; Γ |- tLetIn na b B codom ≤ T →
∑ codom', red Σ Γ T codom' ×
(Σ ;;; Γ |- codom {0 := b} ≤ codom').
Lemma cumul_LetIn_r_inv {cf:checker_flags} (Σ : global_env_ext) Γ na b B codom T :
wf Σ →
Σ ;;; Γ |- T ≤ tLetIn na b B codom →
∑ codom', red Σ Γ T codom' ×
(Σ ;;; Γ |- codom' ≤ codom {0 := b}).
Lemma cumul_Prod_l_inv {cf:checker_flags} (Σ : global_env_ext) Γ na dom codom T :
wf Σ →
Σ ;;; Γ |- tProd na dom codom ≤ T →
∑ na' dom' codom', red Σ Γ T (tProd na' dom' codom') ×
(Σ ;;; Γ |- dom == dom') × (Σ ;;; Γ ,, vass na dom |- codom ≤ codom').
Lemma cumul_Prod_r_inv {cf:checker_flags} (Σ : global_env_ext) Γ na' dom' codom' T :
wf Σ →
Σ ;;; Γ |- T ≤ tProd na' dom' codom' →
∑ na dom codom, red Σ Γ T (tProd na dom codom) ×
(Σ ;;; Γ |- dom == dom') × (Σ ;;; Γ ,, vass na' dom' |- codom ≤ codom').
Lemma cumul_Prod_Sort_inv {cf:checker_flags} Σ Γ s na dom codom :
Σ ;;; Γ |- tProd na dom codom ≤ tSort s → False.
Lemma cumul_Prod_Prod_inv {cf:checker_flags} (Σ : global_env_ext) Γ na na' dom dom' codom codom' : wf Σ →
Σ ;;; Γ |- tProd na dom codom ≤ tProd na' dom' codom' →
((Σ ;;; Γ |- dom == dom') × (Σ ;;; Γ ,, vass na' dom' |- codom ≤ codom'))%type.
Lemma assumption_context_app Γ Γ' :
assumption_context (Γ' ,,, Γ) →
assumption_context Γ × assumption_context Γ'.
Lemma it_mkProd_or_LetIn_ass_inv {cf : checker_flags} (Σ : global_env_ext) Γ ctx ctx' s s' :
wf Σ →
assumption_context ctx →
assumption_context ctx' →
Σ ;;; Γ |- it_mkProd_or_LetIn ctx (tSort s) ≤ it_mkProd_or_LetIn ctx' (tSort s') →
conv_context Σ ctx ctx' × leq_term Σ (tSort s) (tSort s').
Injectivity of products, the essential property of cumulativity needed for subject reduction.
Lemma cumul_Prod_inv {cf:checker_flags} Σ Γ na na' A B A' B' :
wf Σ.1 → wf_local Σ Γ →
Σ ;;; Γ |- tProd na A B ≤ tProd na' A' B' →
((Σ ;;; Γ |- A == A') × (Σ ;;; Γ ,, vass na' A' |- B ≤ B'))%type.
Lemma tProd_it_mkProd_or_LetIn na A B ctx s :
tProd na A B = it_mkProd_or_LetIn ctx (tSort s) →
{ ctx' & ctx = (ctx' ++ [vass na A])%list ∧
destArity [] B = Some (ctx', s) }.
Section Inversions.
Context {cf : checker_flags}.
Context (Σ : global_env_ext) (wfΣ : wf Σ).
Lemma conv_trans_reg : ∀ Γ u v w,
Σ ;;; Γ |- u = v →
Σ ;;; Γ |- v = w →
Σ ;;; Γ |- u = w.
Lemma cumul_App_r {Γ f u v} :
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tApp f u ≤ tApp f v.
Lemma conv_App_r {Γ f x y} :
Σ ;;; Γ |- x == y →
Σ ;;; Γ |- tApp f x == tApp f y.
Lemma conv_Prod_l:
∀ {Γ na na' A1 A2 B},
Σ ;;; Γ |- A1 == A2 →
Σ ;;; Γ |- tProd na A1 B == tProd na' A2 B.
Lemma conv_Prod_r :
∀ {Γ na A B1 B2},
Σ ;;; Γ ,, vass na A |- B1 == B2 →
Σ ;;; Γ |- tProd na A B1 == tProd na A B2.
Lemma cumul_Prod_r :
∀ {Γ na A B1 B2},
Σ ;;; Γ ,, vass na A |- B1 ≤ B2 →
Σ ;;; Γ |- tProd na A B1 ≤ tProd na A B2.
Lemma conv_cumul_l :
∀ Γ u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- u ≤ v.
Lemma conv_refl' :
∀ leq Γ t,
conv leq Σ Γ t t.
Lemma conv_conv :
∀ {Γ leq u v},
∥ Σ ;;; Γ |- u == v ∥ →
conv leq Σ Γ u v.
Lemma eq_term_conv :
∀ {Γ u v},
eq_term (global_ext_constraints Σ) u v →
Σ ;;; Γ |- u = v.
Global Instance conv_trans' :
∀ leq Γ, Transitive (conv leq Σ Γ).
Lemma red_conv_l :
∀ leq Γ u v,
red (fst Σ) Γ u v →
conv leq Σ Γ u v.
Lemma red_conv_r :
∀ leq Γ u v,
red (fst Σ) Γ u v →
conv leq Σ Γ v u.
Lemma conv_Prod leq Γ na1 na2 A1 A2 B1 B2 :
Σ ;;; Γ |- A1 == A2 →
conv leq Σ (Γ,, vass na1 A1) B1 B2 →
conv leq Σ Γ (tProd na1 A1 B1) (tProd na2 A2 B2).
Lemma cumul_Case_c :
∀ Γ indn p brs u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tCase indn p u brs ≤ tCase indn p v brs.
Lemma cumul_Proj_c :
∀ Γ p u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tProj p u ≤ tProj p v.
Lemma conv_App_l :
∀ {Γ f g x},
Σ ;;; Γ |- f == g →
Σ ;;; Γ |- tApp f x == tApp g x.
Lemma App_conv :
∀ Γ t1 t2 u1 u2,
Σ ;;; Γ |- t1 == t2 →
Σ ;;; Γ |- u1 == u2 →
Σ ;;; Γ |- tApp t1 u1 == tApp t2 u2.
Lemma conv_Case_c :
∀ Γ indn p brs u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tCase indn p u brs == tCase indn p v brs.
Lemma conv_Proj_c :
∀ Γ p u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tProj p u == tProj p v.
Lemma conv_Lambda_l :
∀ Γ na A b na' A',
Σ ;;; Γ |- A == A' →
Σ ;;; Γ |- tLambda na A b == tLambda na' A' b.
Lemma conv_Lambda_r :
∀ Γ na A b b',
Σ ;;; Γ,, vass na A |- b == b' →
Σ ;;; Γ |- tLambda na A b == tLambda na A b'.
Lemma cumul_LetIn_bo :
∀ Γ na ty t u u',
Σ ;;; Γ ,, vdef na ty t |- u ≤ u' →
Σ ;;; Γ |- tLetIn na ty t u ≤ tLetIn na ty t u'.
Lemma cumul_Lambda_r :
∀ Γ na A b b',
Σ ;;; Γ,, vass na A |- b ≤ b' →
Σ ;;; Γ |- tLambda na A b ≤ tLambda na A b'.
Lemma cumul_it_mkLambda_or_LetIn :
∀ Δ Γ u v,
Σ ;;; (Δ ,,, Γ) |- u ≤ v →
Σ ;;; Δ |- it_mkLambda_or_LetIn Γ u ≤ it_mkLambda_or_LetIn Γ v.
Lemma cumul_it_mkProd_or_LetIn :
∀ Δ Γ B B',
Σ ;;; (Δ ,,, Γ) |- B ≤ B' →
Σ ;;; Δ |- it_mkProd_or_LetIn Γ B ≤ it_mkProd_or_LetIn Γ B'.
Lemma mkApps_conv_weak :
∀ Γ u1 u2 l,
Σ ;;; Γ |- u1 == u2 →
Σ ;;; Γ |- mkApps u1 l == mkApps u2 l.
Lemma context_relation_length P Γ Γ' :
context_relation P Γ Γ' → #|Γ| = #|Γ'|.
Lemma conv_Lambda leq Γ na1 na2 A1 A2 t1 t2 :
Σ ;;; Γ |- A1 == A2 →
conv leq Σ (Γ ,, vass na1 A1) t1 t2 →
conv leq Σ Γ (tLambda na1 A1 t1) (tLambda na2 A2 t2).
Lemma conva_LetIn_tm Γ na na' ty t t' u :
Σ ;;; Γ |- t == t' →
Σ ;;; Γ |- tLetIn na t ty u == tLetIn na' t' ty u.
Lemma conva_LetIn_ty Γ na na' ty ty' t u :
Σ ;;; Γ |- ty == ty' →
Σ ;;; Γ |- tLetIn na t ty u == tLetIn na' t ty' u.
Lemma conva_LetIn_bo Γ na ty t u u' :
Σ ;;; Γ ,, vdef na ty t |- u == u' →
Σ ;;; Γ |- tLetIn na ty t u == tLetIn na ty t u'.
Lemma conv_LetIn leq Γ na1 na2 t1 t2 A1 A2 u1 u2 :
Σ;;; Γ |- t1 == t2 →
Σ;;; Γ |- A1 == A2 →
conv leq Σ (Γ ,, vdef na1 t1 A1) u1 u2 →
conv leq Σ Γ (tLetIn na1 t1 A1 u1) (tLetIn na2 t2 A2 u2).
Lemma conv_conv_ctx leq Γ Γ' T U :
conv leq Σ Γ T U →
conv_context Σ Γ Γ' →
conv leq Σ Γ' T U.
Lemma it_mkLambda_or_LetIn_conv' leq Γ Δ1 Δ2 t1 t2 :
conv_context Σ (Γ ,,, Δ1) (Γ ,,, Δ2) →
conv leq Σ (Γ ,,, Δ1) t1 t2 →
conv leq Σ Γ (it_mkLambda_or_LetIn Δ1 t1) (it_mkLambda_or_LetIn Δ2 t2).
Lemma it_mkLambda_or_LetIn_conv Γ Δ1 Δ2 t1 t2 :
conv_context Σ (Γ ,,, Δ1) (Γ ,,, Δ2) →
Σ ;;; Γ ,,, Δ1 |- t1 == t2 →
Σ ;;; Γ |- it_mkLambda_or_LetIn Δ1 t1 == it_mkLambda_or_LetIn Δ2 t2.
Lemma red_lambda_inv Γ na A1 b1 T :
red Σ Γ (tLambda na A1 b1) T →
∑ A2 b2, (T = tLambda na A2 b2) ×
red Σ Γ A1 A2 × red Σ (Γ ,, vass na A1) b1 b2.
Lemma Lambda_conv_inv :
∀ leq Γ na1 na2 A1 A2 b1 b2,
wf_local Σ Γ →
conv leq Σ Γ (tLambda na1 A1 b1) (tLambda na2 A2 b2) →
∥ Σ ;;; Γ |- A1 == A2 ∥ ∧ conv leq Σ (Γ ,, vass na1 A1) b1 b2.
End Inversions.
wf Σ.1 → wf_local Σ Γ →
Σ ;;; Γ |- tProd na A B ≤ tProd na' A' B' →
((Σ ;;; Γ |- A == A') × (Σ ;;; Γ ,, vass na' A' |- B ≤ B'))%type.
Lemma tProd_it_mkProd_or_LetIn na A B ctx s :
tProd na A B = it_mkProd_or_LetIn ctx (tSort s) →
{ ctx' & ctx = (ctx' ++ [vass na A])%list ∧
destArity [] B = Some (ctx', s) }.
Section Inversions.
Context {cf : checker_flags}.
Context (Σ : global_env_ext) (wfΣ : wf Σ).
Lemma conv_trans_reg : ∀ Γ u v w,
Σ ;;; Γ |- u = v →
Σ ;;; Γ |- v = w →
Σ ;;; Γ |- u = w.
Lemma cumul_App_r {Γ f u v} :
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tApp f u ≤ tApp f v.
Lemma conv_App_r {Γ f x y} :
Σ ;;; Γ |- x == y →
Σ ;;; Γ |- tApp f x == tApp f y.
Lemma conv_Prod_l:
∀ {Γ na na' A1 A2 B},
Σ ;;; Γ |- A1 == A2 →
Σ ;;; Γ |- tProd na A1 B == tProd na' A2 B.
Lemma conv_Prod_r :
∀ {Γ na A B1 B2},
Σ ;;; Γ ,, vass na A |- B1 == B2 →
Σ ;;; Γ |- tProd na A B1 == tProd na A B2.
Lemma cumul_Prod_r :
∀ {Γ na A B1 B2},
Σ ;;; Γ ,, vass na A |- B1 ≤ B2 →
Σ ;;; Γ |- tProd na A B1 ≤ tProd na A B2.
Lemma conv_cumul_l :
∀ Γ u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- u ≤ v.
Lemma conv_refl' :
∀ leq Γ t,
conv leq Σ Γ t t.
Lemma conv_conv :
∀ {Γ leq u v},
∥ Σ ;;; Γ |- u == v ∥ →
conv leq Σ Γ u v.
Lemma eq_term_conv :
∀ {Γ u v},
eq_term (global_ext_constraints Σ) u v →
Σ ;;; Γ |- u = v.
Global Instance conv_trans' :
∀ leq Γ, Transitive (conv leq Σ Γ).
Lemma red_conv_l :
∀ leq Γ u v,
red (fst Σ) Γ u v →
conv leq Σ Γ u v.
Lemma red_conv_r :
∀ leq Γ u v,
red (fst Σ) Γ u v →
conv leq Σ Γ v u.
Lemma conv_Prod leq Γ na1 na2 A1 A2 B1 B2 :
Σ ;;; Γ |- A1 == A2 →
conv leq Σ (Γ,, vass na1 A1) B1 B2 →
conv leq Σ Γ (tProd na1 A1 B1) (tProd na2 A2 B2).
Lemma cumul_Case_c :
∀ Γ indn p brs u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tCase indn p u brs ≤ tCase indn p v brs.
Lemma cumul_Proj_c :
∀ Γ p u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tProj p u ≤ tProj p v.
Lemma conv_App_l :
∀ {Γ f g x},
Σ ;;; Γ |- f == g →
Σ ;;; Γ |- tApp f x == tApp g x.
Lemma App_conv :
∀ Γ t1 t2 u1 u2,
Σ ;;; Γ |- t1 == t2 →
Σ ;;; Γ |- u1 == u2 →
Σ ;;; Γ |- tApp t1 u1 == tApp t2 u2.
Lemma conv_Case_c :
∀ Γ indn p brs u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tCase indn p u brs == tCase indn p v brs.
Lemma conv_Proj_c :
∀ Γ p u v,
Σ ;;; Γ |- u == v →
Σ ;;; Γ |- tProj p u == tProj p v.
Lemma conv_Lambda_l :
∀ Γ na A b na' A',
Σ ;;; Γ |- A == A' →
Σ ;;; Γ |- tLambda na A b == tLambda na' A' b.
Lemma conv_Lambda_r :
∀ Γ na A b b',
Σ ;;; Γ,, vass na A |- b == b' →
Σ ;;; Γ |- tLambda na A b == tLambda na A b'.
Lemma cumul_LetIn_bo :
∀ Γ na ty t u u',
Σ ;;; Γ ,, vdef na ty t |- u ≤ u' →
Σ ;;; Γ |- tLetIn na ty t u ≤ tLetIn na ty t u'.
Lemma cumul_Lambda_r :
∀ Γ na A b b',
Σ ;;; Γ,, vass na A |- b ≤ b' →
Σ ;;; Γ |- tLambda na A b ≤ tLambda na A b'.
Lemma cumul_it_mkLambda_or_LetIn :
∀ Δ Γ u v,
Σ ;;; (Δ ,,, Γ) |- u ≤ v →
Σ ;;; Δ |- it_mkLambda_or_LetIn Γ u ≤ it_mkLambda_or_LetIn Γ v.
Lemma cumul_it_mkProd_or_LetIn :
∀ Δ Γ B B',
Σ ;;; (Δ ,,, Γ) |- B ≤ B' →
Σ ;;; Δ |- it_mkProd_or_LetIn Γ B ≤ it_mkProd_or_LetIn Γ B'.
Lemma mkApps_conv_weak :
∀ Γ u1 u2 l,
Σ ;;; Γ |- u1 == u2 →
Σ ;;; Γ |- mkApps u1 l == mkApps u2 l.
Lemma context_relation_length P Γ Γ' :
context_relation P Γ Γ' → #|Γ| = #|Γ'|.
Lemma conv_Lambda leq Γ na1 na2 A1 A2 t1 t2 :
Σ ;;; Γ |- A1 == A2 →
conv leq Σ (Γ ,, vass na1 A1) t1 t2 →
conv leq Σ Γ (tLambda na1 A1 t1) (tLambda na2 A2 t2).
Lemma conva_LetIn_tm Γ na na' ty t t' u :
Σ ;;; Γ |- t == t' →
Σ ;;; Γ |- tLetIn na t ty u == tLetIn na' t' ty u.
Lemma conva_LetIn_ty Γ na na' ty ty' t u :
Σ ;;; Γ |- ty == ty' →
Σ ;;; Γ |- tLetIn na t ty u == tLetIn na' t ty' u.
Lemma conva_LetIn_bo Γ na ty t u u' :
Σ ;;; Γ ,, vdef na ty t |- u == u' →
Σ ;;; Γ |- tLetIn na ty t u == tLetIn na ty t u'.
Lemma conv_LetIn leq Γ na1 na2 t1 t2 A1 A2 u1 u2 :
Σ;;; Γ |- t1 == t2 →
Σ;;; Γ |- A1 == A2 →
conv leq Σ (Γ ,, vdef na1 t1 A1) u1 u2 →
conv leq Σ Γ (tLetIn na1 t1 A1 u1) (tLetIn na2 t2 A2 u2).
Lemma conv_conv_ctx leq Γ Γ' T U :
conv leq Σ Γ T U →
conv_context Σ Γ Γ' →
conv leq Σ Γ' T U.
Lemma it_mkLambda_or_LetIn_conv' leq Γ Δ1 Δ2 t1 t2 :
conv_context Σ (Γ ,,, Δ1) (Γ ,,, Δ2) →
conv leq Σ (Γ ,,, Δ1) t1 t2 →
conv leq Σ Γ (it_mkLambda_or_LetIn Δ1 t1) (it_mkLambda_or_LetIn Δ2 t2).
Lemma it_mkLambda_or_LetIn_conv Γ Δ1 Δ2 t1 t2 :
conv_context Σ (Γ ,,, Δ1) (Γ ,,, Δ2) →
Σ ;;; Γ ,,, Δ1 |- t1 == t2 →
Σ ;;; Γ |- it_mkLambda_or_LetIn Δ1 t1 == it_mkLambda_or_LetIn Δ2 t2.
Lemma red_lambda_inv Γ na A1 b1 T :
red Σ Γ (tLambda na A1 b1) T →
∑ A2 b2, (T = tLambda na A2 b2) ×
red Σ Γ A1 A2 × red Σ (Γ ,, vass na A1) b1 b2.
Lemma Lambda_conv_inv :
∀ leq Γ na1 na2 A1 A2 b1 b2,
wf_local Σ Γ →
conv leq Σ Γ (tLambda na1 A1 b1) (tLambda na2 A2 b2) →
∥ Σ ;;; Γ |- A1 == A2 ∥ ∧ conv leq Σ (Γ ,, vass na1 A1) b1 b2.
End Inversions.