Library MetaCoq.PCUIC.PCUICEquality
Section CRelationLemmas.
Context {A : Type} (R : crelation A).
Lemma flip_Reflexive : Reflexive R → Reflexive (flip R).
Lemma flip_Symmetric : Symmetric R → Symmetric (flip R).
Lemma flip_Transitive : Transitive R → Transitive (flip R).
End CRelationLemmas.
Definition R_universe_instance R
:= fun u u' ⇒ Forall2 R (List.map Universe.make u) (List.map Universe.make u').
Lemma R_universe_instance_impl R R' :
RelationClasses.subrelation R R' →
RelationClasses.subrelation (R_universe_instance R) (R_universe_instance R').
Lemma R_universe_instance_impl' R R' :
RelationClasses.subrelation R R' →
∀ u u', R_universe_instance R u u' → R_universe_instance R' u u'.
Inductive eq_term_upto_univ (Re Rle : universe → universe → Prop) : term → term → Type :=
| eq_Rel n :
eq_term_upto_univ Re Rle (tRel n) (tRel n)
| eq_Evar e args args' :
All2 (eq_term_upto_univ Re Re) args args' →
eq_term_upto_univ Re Rle (tEvar e args) (tEvar e args')
| eq_Var id :
eq_term_upto_univ Re Rle (tVar id) (tVar id)
| eq_Sort s s' :
Rle s s' →
eq_term_upto_univ Re Rle (tSort s) (tSort s')
| eq_App t t' u u' :
eq_term_upto_univ Re Rle t t' →
eq_term_upto_univ Re Re u u' →
eq_term_upto_univ Re Rle (tApp t u) (tApp t' u')
| eq_Const c u u' :
R_universe_instance Re u u' →
eq_term_upto_univ Re Rle (tConst c u) (tConst c u')
| eq_Ind i u u' :
R_universe_instance Re u u' →
eq_term_upto_univ Re Rle (tInd i u) (tInd i u')
| eq_Construct i k u u' :
R_universe_instance Re u u' →
eq_term_upto_univ Re Rle (tConstruct i k u) (tConstruct i k u')
| eq_Lambda na na' ty ty' t t' :
eq_term_upto_univ Re Re ty ty' →
eq_term_upto_univ Re Rle t t' →
eq_term_upto_univ Re Rle (tLambda na ty t) (tLambda na' ty' t')
| eq_Prod na na' a a' b b' :
eq_term_upto_univ Re Re a a' →
eq_term_upto_univ Re Rle b b' →
eq_term_upto_univ Re Rle (tProd na a b) (tProd na' a' b')
| eq_LetIn na na' t t' ty ty' u u' :
eq_term_upto_univ Re Re t t' →
eq_term_upto_univ Re Re ty ty' →
eq_term_upto_univ Re Rle u u' →
eq_term_upto_univ Re Rle (tLetIn na t ty u) (tLetIn na' t' ty' u')
| eq_Case indn p p' c c' brs brs' :
eq_term_upto_univ Re Re p p' →
eq_term_upto_univ Re Re c c' →
All2 (fun x y ⇒
(fst x = fst y) ×
eq_term_upto_univ Re Re (snd x) (snd y)
) brs brs' →
eq_term_upto_univ Re Rle (tCase indn p c brs) (tCase indn p' c' brs')
| eq_Proj p c c' :
eq_term_upto_univ Re Re c c' →
eq_term_upto_univ Re Rle (tProj p c) (tProj p c')
| eq_Fix mfix mfix' idx :
All2 (fun x y ⇒
eq_term_upto_univ Re Re x.(dtype) y.(dtype) ×
eq_term_upto_univ Re Re x.(dbody) y.(dbody) ×
(x.(rarg) = y.(rarg))
) mfix mfix' →
eq_term_upto_univ Re Rle (tFix mfix idx) (tFix mfix' idx)
| eq_CoFix mfix mfix' idx :
All2 (fun x y ⇒
eq_term_upto_univ Re Re x.(dtype) y.(dtype) ×
eq_term_upto_univ Re Re x.(dbody) y.(dbody) ×
(x.(rarg) = y.(rarg))
) mfix mfix' →
eq_term_upto_univ Re Rle (tCoFix mfix idx) (tCoFix mfix' idx).
Definition eq_term `{checker_flags} φ :=
eq_term_upto_univ (eq_universe φ) (eq_universe φ).
Definition leq_term `{checker_flags} φ :=
eq_term_upto_univ (eq_universe φ) (leq_universe φ).
Lemma Forall2_same :
∀ A (P : A → A → Prop) l,
(∀ x, P x x) →
Forall2 P l l.
Instance eq_term_upto_univ_refl Re Rle :
RelationClasses.Reflexive Re →
RelationClasses.Reflexive Rle →
Reflexive (eq_term_upto_univ Re Rle).
Instance eq_term_refl `{checker_flags} φ : Reflexive (eq_term φ).
Instance leq_term_refl `{checker_flags} φ : Reflexive (leq_term φ).
Instance Forall2_symP :
∀ A (P : A → A → Prop),
RelationClasses.Symmetric P →
Symmetric (Forall2 P).
Instance eq_term_upto_univ_sym Re Rle :
RelationClasses.Symmetric Re →
RelationClasses.Symmetric Rle →
Symmetric (eq_term_upto_univ Re Rle).
Instance eq_term_sym `{checker_flags} φ : Symmetric (eq_term φ).
Instance eq_term_upto_univ_trans Re Rle :
RelationClasses.Transitive Re →
RelationClasses.Transitive Rle →
Transitive (eq_term_upto_univ Re Rle).
Instance eq_term_trans {cf:checker_flags} φ : Transitive (eq_term φ).
Instance leq_term_trans {cf:checker_flags} φ : Transitive (leq_term φ).
Instance eq_term_upto_univ_equiv Re (hRe : RelationClasses.Equivalence Re)
: Equivalence (eq_term_upto_univ Re Re).
Instance eq_term_equiv {cf:checker_flags} φ : Equivalence (eq_term φ) :=
{| Equivalence_Reflexive := eq_term_refl _;
Equivalence_Symmetric := eq_term_sym _;
Equivalence_Transitive := eq_term_trans _ |}.
Instance leq_term_preorder {cf:checker_flags} φ : PreOrder (leq_term φ) :=
{| PreOrder_Reflexive := leq_term_refl _;
PreOrder_Transitive := leq_term_trans _ |}.
Lemma Forall2_sym :
∀ A (P : A → A → Prop) l l',
Forall2 P l l' →
Forall2 (fun x y ⇒ P y x) l' l.
Instance R_universe_instance_equiv R (hR : RelationClasses.Equivalence R)
: RelationClasses.Equivalence (R_universe_instance R).
Lemma R_universe_instance_antisym Re Rle (hRe : RelationClasses.Equivalence Re) :
RelationClasses.Antisymmetric _ Re Rle →
RelationClasses.Antisymmetric _ (R_universe_instance Re) (R_universe_instance Rle).
Lemma eq_term_upto_univ_antisym Re Rle (hRe : RelationClasses.Equivalence Re) :
RelationClasses.Antisymmetric _ Re Rle →
Antisymmetric (eq_term_upto_univ Re Re) (eq_term_upto_univ Re Rle).
Instance leq_term_antisym {cf:checker_flags} φ
: Antisymmetric (eq_term φ) (leq_term φ).
Instance eq_term_upto_univ_impl Re Re' Rle Rle' :
RelationClasses.subrelation Re Re' →
RelationClasses.subrelation Rle Rle' →
subrelation (eq_term_upto_univ Re Rle) (eq_term_upto_univ Re' Rle').
Instance eq_term_upto_univ_leq Re Rle :
RelationClasses.subrelation Re Rle →
subrelation (eq_term_upto_univ Re Re) (eq_term_upto_univ Re Rle).
Instance eq_term_leq_term {cf:checker_flags} φ
: subrelation (eq_term φ) (leq_term φ).
Instance leq_term_partial_order {cf:checker_flags} φ
: PartialOrder (eq_term φ) (leq_term φ).
Lemma eq_term_upto_univ_lift Re Rle n k :
Proper (eq_term_upto_univ Re Rle ==> eq_term_upto_univ Re Rle) (lift n k).
Lemma lift_eq_term {cf:checker_flags} φ n k T U :
eq_term φ T U → eq_term φ (lift n k T) (lift n k U).
Lemma lift_leq_term {cf:checker_flags} φ n k T U :
leq_term φ T U → leq_term φ (lift n k T) (lift n k U).
Lemma eq_term_upto_univ_substs Re Rle :
RelationClasses.subrelation Re Rle →
∀ u v n l l',
eq_term_upto_univ Re Rle u v →
All2 (eq_term_upto_univ Re Re) l l' →
eq_term_upto_univ Re Rle (subst l n u) (subst l' n v).
Lemma eq_term_upto_univ_subst Re Rle :
RelationClasses.subrelation Re Rle →
∀ u v n x y,
eq_term_upto_univ Re Rle u v →
eq_term_upto_univ Re Re x y →
eq_term_upto_univ Re Rle (u{n := x}) (v{n := y}).
Lemma subst_eq_term {cf:checker_flags} φ l k T U :
eq_term φ T U →
eq_term φ (subst l k T) (subst l k U).
Lemma subst_leq_term {cf:checker_flags} φ l k T U :
leq_term φ T U →
leq_term φ (subst l k T) (subst l k U).
Fixpoint eqb_term_upto_univ (equ lequ : universe → universe → bool) (u v : term) : bool :=
match u, v with
| tRel n, tRel m ⇒
eqb n m
| tEvar e args, tEvar e' args' ⇒
eqb e e' &&
forallb2 (eqb_term_upto_univ equ equ) args args'
| tVar id, tVar id' ⇒
eqb id id'
| tSort u, tSort u' ⇒
lequ u u'
| tApp u v, tApp u' v' ⇒
eqb_term_upto_univ equ lequ u u' &&
eqb_term_upto_univ equ equ v v'
| tConst c u, tConst c' u' ⇒
eqb c c' &&
forallb2 equ (map Universe.make u) (map Universe.make u')
| tInd i u, tInd i' u' ⇒
eqb i i' &&
forallb2 equ (map Universe.make u) (map Universe.make u')
| tConstruct i k u, tConstruct i' k' u' ⇒
eqb i i' &&
eqb k k' &&
forallb2 equ (map Universe.make u) (map Universe.make u')
| tLambda na A t, tLambda na' A' t' ⇒
eqb_term_upto_univ equ equ A A' &&
eqb_term_upto_univ equ lequ t t'
| tProd na A B, tProd na' A' B' ⇒
eqb_term_upto_univ equ equ A A' &&
eqb_term_upto_univ equ lequ B B'
| tLetIn na B b u, tLetIn na' B' b' u' ⇒
eqb_term_upto_univ equ equ B B' &&
eqb_term_upto_univ equ equ b b' &&
eqb_term_upto_univ equ lequ u u'
| tCase indp p c brs, tCase indp' p' c' brs' ⇒
eqb indp indp' &&
eqb_term_upto_univ equ equ p p' &&
eqb_term_upto_univ equ equ c c' &&
forallb2 (fun x y ⇒
eqb (fst x) (fst y) &&
eqb_term_upto_univ equ equ (snd x) (snd y)
) brs brs'
| tProj p c, tProj p' c' ⇒
eqb p p' &&
eqb_term_upto_univ equ equ c c'
| tFix mfix idx, tFix mfix' idx' ⇒
eqb idx idx' &&
forallb2 (fun x y ⇒
eqb_term_upto_univ equ equ x.(dtype) y.(dtype) &&
eqb_term_upto_univ equ equ x.(dbody) y.(dbody) &&
eqb x.(rarg) y.(rarg)
) mfix mfix'
| tCoFix mfix idx, tCoFix mfix' idx' ⇒
eqb idx idx' &&
forallb2 (fun x y ⇒
eqb_term_upto_univ equ equ x.(dtype) y.(dtype) &&
eqb_term_upto_univ equ equ x.(dbody) y.(dbody) &&
eqb x.(rarg) y.(rarg)
) mfix mfix'
| _, _ ⇒ false
end.
Lemma forallb2_Forall2 :
∀ A (p : A → A → bool) l l',
forallb2 p l l' →
Forall2 (fun x y ⇒ p x y) l l'.
Lemma eqb_term_upto_univ_impl (equ lequ : _ → _ → bool) Re Rle :
RelationClasses.subrelation equ Re →
RelationClasses.subrelation lequ Rle →
subrelation (eqb_term_upto_univ equ lequ) (eq_term_upto_univ Re Rle).
Lemma reflect_eq_term_upto_univ equ lequ (Re Rle : universe → universe → Prop) :
(∀ u u', reflectT (Re u u') (equ u u')) →
(∀ u u', reflectT (Rle u u') (lequ u u')) →
∀ t t', reflectT (eq_term_upto_univ Re Rle t t')
(eqb_term_upto_univ equ lequ t t').
Lemma eq_term_upto_univ_mkApps Re Rle u1 l1 u2 l2 :
eq_term_upto_univ Re Rle u1 u2 →
All2 (eq_term_upto_univ Re Re) l1 l2 →
eq_term_upto_univ Re Rle (mkApps u1 l1) (mkApps u2 l2).
Lemma eq_term_upto_univ_mkApps_l_inv Re Rle u l t :
eq_term_upto_univ Re Rle (mkApps u l) t →
∑ u' l',
eq_term_upto_univ Re Rle u u' ×
All2 (eq_term_upto_univ Re Re) l l' ×
(t = mkApps u' l').
Lemma eq_term_upto_univ_mkApps_r_inv Re Rle u l t :
eq_term_upto_univ Re Rle t (mkApps u l) →
∑ u' l',
eq_term_upto_univ Re Rle u' u ×
All2 (eq_term_upto_univ Re Re) l' l ×
(t = mkApps u' l').
Lemma eq_term_upto_univ_it_mkLambda_or_LetIn Re Rle Γ :
RelationClasses.Reflexive Re →
respectful (eq_term_upto_univ Re Rle) (eq_term_upto_univ Re Rle)
(it_mkLambda_or_LetIn Γ) (it_mkLambda_or_LetIn Γ).
Lemma eq_term_it_mkLambda_or_LetIn {cf:checker_flags} φ Γ :
respectful (eq_term φ) (eq_term φ)
(it_mkLambda_or_LetIn Γ) (it_mkLambda_or_LetIn Γ).
Lemma eq_term_upto_univ_it_mkProd_or_LetIn Re Rle Γ :
RelationClasses.Reflexive Re →
respectful (eq_term_upto_univ Re Rle) (eq_term_upto_univ Re Rle)
(it_mkProd_or_LetIn Γ) (it_mkProd_or_LetIn Γ).
Lemma eq_term_it_mkProd_or_LetIn {cf:checker_flags} φ Γ:
respectful (eq_term φ) (eq_term φ)
(it_mkProd_or_LetIn Γ) (it_mkProd_or_LetIn Γ).
Lemma eq_term_it_mkLambda_or_LetIn_inv {cf:checker_flags} φ Γ u v :
eq_term φ (it_mkLambda_or_LetIn Γ u) (it_mkLambda_or_LetIn Γ v) →
eq_term φ u v.
Definition upto_names := eq_term_upto_univ eq eq.
Infix "≡" := upto_names (at level 60).
Infix "≡'" := (eq_term_upto_univ eq eq) (at level 60).
Notation upto_names' := (eq_term_upto_univ eq eq).
Instance upto_names_ref : Reflexive upto_names.
Instance upto_names_sym : Symmetric upto_names.
Instance upto_names_trans : Transitive upto_names.
Definition nleq_term t t' :=
eqb_term_upto_univ eqb eqb t t'.
Corollary reflect_upto_names :
∀ t t', reflectT (upto_names t t') (nleq_term t t').
Lemma upto_names_impl Re Rle :
RelationClasses.Reflexive Re →
RelationClasses.Reflexive Rle →
subrelation upto_names (eq_term_upto_univ Re Rle).
Lemma upto_names_impl_eq_term {cf:checker_flags} φ u v :
u ≡ v → eq_term φ u v.
Lemma upto_names_impl_leq_term {cf:checker_flags} φ u v :
u ≡ v → leq_term φ u v.
Lemma eq_term_upto_univ_isApp Re Rle u v :
eq_term_upto_univ Re Rle u v →
isApp u = isApp v.
Inductive eq_context_upto (Re : universe → universe → Prop) : context → context → Type :=
| eq_context_nil : eq_context_upto Re [] []
| eq_context_vass na A Γ nb B Δ :
eq_term_upto_univ Re Re A B →
eq_context_upto Re Γ Δ →
eq_context_upto Re (Γ ,, vass na A) (Δ ,, vass nb B)
| eq_context_vdef na u A Γ nb v B Δ :
eq_term_upto_univ Re Re u v →
eq_term_upto_univ Re Re A B →
eq_context_upto Re Γ Δ →
eq_context_upto Re (Γ ,, vdef na u A) (Δ ,, vdef nb v B).
Definition eq_def_upto Re d d' : Type :=
(eq_term_upto_univ Re Re d.(dtype) d'.(dtype)) ×
(eq_term_upto_univ Re Re d.(dbody) d'.(dbody)) ×
(d.(rarg) = d'.(rarg)).
Inductive rel_option {A B} (R : A → B → Type) : option A → option B → Type :=
| rel_some : ∀ a b, R a b → rel_option R (Some a) (Some b)
| rel_none : rel_option R None None.
Definition eq_decl_upto Re d d' : Type :=
rel_option (eq_term_upto_univ Re Re) d.(decl_body) d'.(decl_body) ×
eq_term_upto_univ Re Re d.(decl_type) d'.(decl_type).
Lemma All2_eq_context_upto Re :
subrelation (All2 (eq_decl_upto Re)) (eq_context_upto Re).
Lemma eq_context_upto_refl Re :
RelationClasses.Reflexive Re →
Reflexive (eq_context_upto Re).
Lemma eq_context_upto_sym Re :
RelationClasses.Symmetric Re →
Symmetric (eq_context_upto Re).
Lemma eq_context_upto_cat Re Γ Δ Γ' Δ' :
eq_context_upto Re Γ Γ' →
eq_context_upto Re Δ Δ' →
eq_context_upto Re (Γ ,,, Δ) (Γ' ,,, Δ').
Lemma eq_context_upto_rev Re Γ Δ :
eq_context_upto Re Γ Δ →
eq_context_upto Re (rev Γ) (rev Δ).
Lemma eq_context_upto_rev' :
∀ Γ Δ Re,
eq_context_upto Re Γ Δ →
eq_context_upto Re (List.rev Γ) (List.rev Δ).
Lemma eq_context_impl :
∀ Re Re',
RelationClasses.subrelation Re Re' →
subrelation (eq_context_upto Re) (eq_context_upto Re').
Lemma eq_context_upto_length :
∀ Re Γ Δ,
eq_context_upto Re Γ Δ →
#|Γ| = #|Δ|.
Section ContextUpTo.
Context (Re : universe → universe → Prop).
Context (ReR : RelationClasses.Reflexive Re).
Context (ReS : RelationClasses.Symmetric Re).
Context (ReT : RelationClasses.Transitive Re).
Notation eq_ctx := (eq_context_upto Re).
Global Instance eq_ctx_refl : Reflexive eq_ctx.
Global Instance eq_ctx_sym : Symmetric eq_ctx.
Global Instance eq_ctx_trans : Transitive eq_ctx.
End ContextUpTo.
Definition eq_opt_term `{checker_flags} φ (t u : option term) :=
match t, u with
| Some t, Some u ⇒ eq_term φ t u
| None, None ⇒ True
| _, _ ⇒ False
end.
Definition eq_decl `{checker_flags} φ (d d' : context_decl) :=
eq_opt_term φ d.(decl_body) d'.(decl_body) × eq_term φ d.(decl_type) d'.(decl_type).
Definition eq_context `{checker_flags} φ (Γ Δ : context) :=
All2 (eq_decl φ) Γ Δ.
Lemma lift_eq_decl `{checker_flags} ϕ n k d d' :
eq_decl ϕ d d' → eq_decl ϕ (lift_decl n k d) (lift_decl n k d').
Lemma lift_eq_context `{checker_flags} φ l l' n k :
eq_context φ l l' →
eq_context φ (lift_context n k l) (lift_context n k l').
Lemma subst_instance_level_val u l v v'
(H1 : ∀ s, valuation_mono v s = valuation_mono v' s)
(H2 : ∀ n, val0 v (nth n u Level.lSet) = Z.of_nat (valuation_poly v' n))
: val0 v (subst_instance_level u l) = val0 v' l.
Lemma eq_val v v'
(H1 : ∀ s, valuation_mono v s = valuation_mono v' s)
(H2 : ∀ n, valuation_poly v n = valuation_poly v' n)
: ∀ u, val v u = val v' u.
Lemma is_prop_subst_instance_level u l
(Hu : forallb (negb ∘ Level.is_prop) u)
: Level.is_prop (subst_instance_level u l) = Level.is_prop l.
Lemma subst_instance_univ_val u l v v'
(Hu : forallb (negb ∘ Level.is_prop) u)
(H1 : ∀ s, valuation_mono v s = valuation_mono v' s)
(H2 : ∀ n, val0 v (nth n u Level.lSet) = Z.of_nat (valuation_poly v' n))
: val v (subst_instance_univ u l) = val v' l.
Definition subst_instance_valuation (u : universe_instance) (v : valuation) :=
{| valuation_mono := valuation_mono v ;
valuation_poly := fun i ⇒ Z.to_nat (val0 v (nth i u Level.lSet)) |}.
Lemma subst_instance_univ_val' u l v
(Hu : forallb (negb ∘ Level.is_prop) u)
: val v (subst_instance_univ u l) = val (subst_instance_valuation u v) l.
Class SubstUnivPreserving Re := Build_SubstUnivPreserving :
∀ s u1 u2, R_universe_instance Re u1 u2 →
Re (subst_instance_univ u1 s) (subst_instance_univ u2 s).
Lemma subst_equal_inst_inst Re :
SubstUnivPreserving Re →
∀ u u1 u2, R_universe_instance Re u1 u2 →
R_universe_instance Re (subst_instance_instance u1 u)
(subst_instance_instance u2 u).
Lemma eq_term_upto_univ_subst_instance_constr Re :
RelationClasses.Reflexive Re →
SubstUnivPreserving Re →
∀ t u1 u2,
R_universe_instance Re u1 u2 →
eq_term_upto_univ Re Re (subst_instance_constr u1 t)
(subst_instance_constr u2 t).
Instance leq_term_SubstUnivPreserving {cf:checker_flags} φ :
SubstUnivPreserving (eq_universe φ).
Lemma eq_term_upto_univ_mkApps_inv Re u l u' l' :
isApp u = false →
isApp u' = false →
eq_term_upto_univ Re Re (mkApps u l) (mkApps u' l') →
eq_term_upto_univ Re Re u u' × All2 (eq_term_upto_univ Re Re) l l'.
Lemma isLambda_eq_term_l Re u v :
isLambda u →
eq_term_upto_univ Re Re u v →
isLambda v.
Lemma isLambda_eq_term_r Re u v :
isLambda v →
eq_term_upto_univ Re Re u v →
isLambda u.
Lemma isConstruct_app_eq_term_l Re u v :
isConstruct_app u →
eq_term_upto_univ Re Re u v →
isConstruct_app v.
Lemma isConstruct_app_eq_term_r :
∀ Re u v,
isConstruct_app v →
eq_term_upto_univ Re Re u v →
isConstruct_app u.
Instance subrelation_same :
∀ A (R : A → A → Prop),
RelationClasses.subrelation R R.
Lemma eq_term_upto_univ_flip (Re Rle Rle' : universe → universe → Prop) u v :
RelationClasses.Reflexive Re →
RelationClasses.Reflexive Rle →
RelationClasses.Symmetric Re →
RelationClasses.Transitive Re →
RelationClasses.Transitive Rle →
RelationClasses.subrelation Re Rle →
(∀ x y, Rle x y → Rle' y x) →
eq_term_upto_univ Re Rle u v →
eq_term_upto_univ Re Rle' v u.