Library MetaCoq.PCUIC.PCUICParallelReductionConfluence
Notation "'∃' x .. y , P" := (sigT (fun x ⇒ .. (sigT (fun y ⇒ P%type)) ..))
(at level 200, x binder, y binder, right associativity,
format "'[ ' '[ ' ∃ x .. y ']' , '/' P ']'") : type_scope.
Instance ren_ext : Morphisms.Proper (`=1` ==> `=1`)%signature ren.
Lemma shiftn0 r : shiftn 0 r =1 r.
Lemma shiftnS n r : shiftn (S n) r =1 shiftn 1 (shiftn n r).
Definition rename_context r Γ :=
fold_context (fun k ⇒ rename (shiftn k r)) Γ.
Definition inst_context s Γ :=
fold_context (fun k ⇒ inst (⇑^k s)) Γ.
Definition rename_context_snoc0 r Γ d : rename_context r (d :: Γ) = rename_context r Γ ,, map_decl (rename (shiftn #|Γ| r)) d.
Lemma rename_context_snoc r Γ d : rename_context r (Γ ,, d) = rename_context r Γ ,, map_decl (rename (shiftn #|Γ| r)) d.
Lemma rename_context_alt r Γ :
rename_context r Γ =
mapi (fun k' d ⇒ map_decl (rename (shiftn (Nat.pred #|Γ| - k') r)) d) Γ.
Definition inst_context_snoc0 s Γ d :
inst_context s (d :: Γ) =
inst_context s Γ ,, map_decl (inst (⇑^#|Γ| s)) d.
Lemma inst_context_snoc s Γ d : inst_context s (Γ ,, d) = inst_context s Γ ,, map_decl (inst (⇑^#|Γ| s)) d.
Lemma inst_context_alt s Γ :
inst_context s Γ =
mapi (fun k' d ⇒ map_decl (inst (⇑^(Nat.pred #|Γ| - k') s)) d) Γ.
Lemma inst_context_length s Γ : #|inst_context s Γ| = #|Γ|.
Lemma subst_consn_shiftn n l σ : #|l| = n → ↑^n ∘ (l ⋅n σ) =1 σ.
Lemma shiftn_consn_idsn n σ : ↑^n ∘ ⇑^n σ =1 σ ∘ ↑^n.
Lemma subst10_inst a b τ : b {0 := a}.[τ] = (b.[⇑ τ] {0 := a.[τ]}).
Lemma lift_renaming_0 k : ren (lift_renaming k 0) = ren (Nat.add k).
Lemma lift0_inst n t : lift0 n t = t.[↑^n].
Lemma map_vass_map_def g l r :
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
(map (map_def (rename r) g) l)) =
(mapi (fun i d ⇒ map_decl (rename (shiftn i r)) d)
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).
Lemma rename_fix_context r :
∀ (mfix : list (def term)),
fix_context (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix) =
rename_context r (fix_context mfix).
Lemma map_vass_map_def_inst g l s :
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
(map (map_def (inst s) g) l)) =
(mapi (fun i d ⇒ map_decl (inst (⇑^i s)) d)
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).
Lemma inst_fix_context:
∀ (mfix : list (def term)) s,
fix_context (map (map_def (inst s) (inst (⇑^#|mfix| s))) mfix) =
inst_context s (fix_context mfix).
Lemma mkApps_eq_decompose_app_rec {f args t l} :
mkApps f args = t →
~~ isApp f →
match decompose_app_rec t l with
| (f', args') ⇒ f' = f ∧ mkApps t l = mkApps f' args'
end.
Lemma mkApps_eq_decompose' {f args t} :
mkApps f args = t →
~~ isApp f →
match decompose_app t with
| (f', args') ⇒ f' = f ∧ t = mkApps f' args'
end.
Lemma fst_decompose_app_rec t l : fst (decompose_app_rec t l) = fst (decompose_app t).
Section FoldFix.
Context (rho : context → term → term).
Context (Γ : context).
Fixpoint fold_fix_context acc m :=
match m with
| [] ⇒ acc
| def :: fixd ⇒
fold_fix_context (vass def.(dname) (lift0 #|acc| (rho Γ def.(dtype))) :: acc) fixd
end.
Fixpoint fold_ctx_over Γ' :=
match Γ' with
| [] ⇒ []
| {| decl_name := na; decl_body := None; decl_type := T |} :: Γ' ⇒
let Γ'' := fold_ctx_over Γ' in
vass na (rho (Γ ,,, Γ'') T) :: Γ''
| {| decl_name := na; decl_body := Some b; decl_type := T |} :: Γ' ⇒
let Γ'' := fold_ctx_over Γ' in
vdef na (rho (Γ ,,, Γ'') b) (rho (Γ ,,, Γ'') T) :: Γ''
end.
End FoldFix.
Lemma term_forall_ctx_list_ind :
∀ (P : term → Type),
(∀ (n : nat), P (tRel n)) →
(∀ (i : ident), P (tVar i)) →
(∀ (n : nat) (l : list term), All (P) l → P (tEvar n l)) →
(∀ s, P (tSort s)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
(∀ (n : name) (t : term),
P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 →
P (tLetIn n t t0 t1)) →
(∀ (t u : term),
(∀ t', size t' < size (tApp t u) → P t') →
P t → P u → P (tApp t u)) →
(∀ (s : String.string) (u : list Level.t), P (tConst s u)) →
(∀ (i : inductive) (u : list Level.t), P (tInd i u)) →
(∀ (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) →
(∀ (p : inductive × nat) (t : term),
P t → ∀ t0 : term, P t0 → ∀ l : list (nat × term),
tCaseBrsProp (P) l → P (tCase p t t0 l)) →
(∀ (s : projection) (t : term), P t → P (tProj s t)) →
(∀ (m : mfixpoint term) (n : nat),
tFixProp P P m → P (tFix m n)) →
(∀ (m : mfixpoint term) (n : nat),
tFixProp (P) P m → P (tCoFix m n)) →
∀ (t : term), P t.
Lemma atom_mkApps {t l} : atom (mkApps t l) → atom t ∧ l = [].
Lemma pred_atom_mkApps {t l} : pred_atom (mkApps t l) → pred_atom t ∧ l = [].
Definition application_atom t :=
match t with
| tVar _
| tSort _
| tInd _ _
| tConstruct _ _ _
| tLambda _ _ _ ⇒ true
| _ ⇒ false
end.
Lemma application_atom_mkApps {t l} : application_atom (mkApps t l) → application_atom t ∧ l = [].
Section Confluence.
Lemma pred_mkApps Σ Γ Δ M0 M1 N0 N1 :
pred1 Σ Γ Δ M0 M1 →
All2 (pred1 Σ Γ Δ) N0 N1 →
pred1 Σ Γ Δ (mkApps M0 N0) (mkApps M1 N1).
Lemma pred_snd_nth:
∀ (Σ : global_env) (Γ Δ : context) (c : nat) (brs1 brs' : list (nat × term)),
All2
(on_Trel (pred1 Σ Γ Δ) snd) brs1
brs' →
pred1_ctx Σ Γ Δ →
pred1 Σ Γ Δ
(snd (nth c brs1 (0, tDummy)))
(snd (nth c brs' (0, tDummy))).
Lemma mkApps_eq_decompose_app {t t' l l'} :
mkApps t l = mkApps t' l' →
decompose_app_rec t l = decompose_app_rec t' l'.
Lemma pred1_mkApps_tConstruct (Σ : global_env) (Γ Δ : context)
ind pars k (args : list term) c :
pred1 Σ Γ Δ (mkApps (tConstruct ind pars k) args) c →
{args' : list term & (c = mkApps (tConstruct ind pars k) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
Lemma pred1_mkApps_refl_tConstruct (Σ : global_env) Γ Δ i k u l l' :
pred1 Σ Γ Δ (mkApps (tConstruct i k u) l) (mkApps (tConstruct i k u) l') →
All2 (pred1 Σ Γ Δ) l l'.
Lemma pred1_mkApps_tInd (Σ : global_env) (Γ Δ : context)
ind u (args : list term) c :
pred1 Σ Γ Δ (mkApps (tInd ind u) args) c →
{args' : list term & (c = mkApps (tInd ind u) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
Lemma pred1_mkApps_tConst_axiom (Σ : global_env) (Γ Δ : context)
cst u (args : list term) cb c :
declared_constant Σ cst cb → cst_body cb = None →
pred1 Σ Γ Δ (mkApps (tConst cst u) args) c →
{args' : list term & (c = mkApps (tConst cst u) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
Lemma pred1_mkApps_tFix_inv (Σ : global_env) (Γ Δ : context)
mfix0 idx (args0 : list term) c :
pred1 Σ Γ Δ (mkApps (tFix mfix0 idx) args0) c →
({ mfix1 & { args1 : list term &
(c = mkApps (tFix mfix1 idx) args1) ×
All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1)
dtype dbody
(fun x ⇒ (dname x, rarg x))
(pred1 Σ) mfix0 mfix1 ×
(All2 (pred1 Σ Γ Δ) ) args0 args1 } }%type) +
({ mfix1 & { args1 & { narg & { fn &
((unfold_fix mfix1 idx = Some (narg, fn)) ×
All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1)
dtype dbody
(fun x ⇒ (dname x, rarg x))
(pred1 Σ) mfix0 mfix1 ×
(is_constructor narg args1 = true) ×
(All2 (pred1 Σ Γ Δ) args0 args1) ×
(c = mkApps fn args1)) } } } })%type.
Lemma pred1_mkApps_tFix_refl_inv (Σ : global_env) (Γ Δ : context)
mfix0 mfix1 idx0 idx1 (args0 args1 : list term) :
pred1 Σ Γ Δ (mkApps (tFix mfix0 idx0) args0) (mkApps (tFix mfix1 idx1) args1) →
(All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1)
dtype dbody
(fun x ⇒ (dname x, rarg x))
(pred1 Σ) mfix0 mfix1 ×
(All2 (pred1 Σ Γ Δ) ) args0 args1).
Lemma pred1_mkApps_tCoFix_inv (Σ : global_env) (Γ Δ : context)
mfix0 idx (args0 : list term) c :
pred1 Σ Γ Δ (mkApps (tCoFix mfix0 idx) args0) c →
∃ mfix1 args1,
(c = mkApps (tCoFix mfix1 idx) args1) ×
All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1) dtype dbody
(fun x ⇒ (dname x, rarg x))
(pred1 Σ) mfix0 mfix1 ×
(All2 (pred1 Σ Γ Δ) ) args0 args1.
Lemma pred1_mkApps_tCoFix_refl_inv (Σ : global_env) (Γ Δ : context)
mfix0 mfix1 idx (args0 args1 : list term) :
pred1 Σ Γ Δ (mkApps (tCoFix mfix0 idx) args0) (mkApps (tCoFix mfix1 idx) args1) →
All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1) dtype dbody
(fun x ⇒ (dname x, rarg x))
(pred1 Σ) mfix0 mfix1 ×
(All2 (pred1 Σ Γ Δ)) args0 args1.
Lemma All2_prop_eq_All2 {A B} {Σ Γ Δ} {f : A → term} {g : A → B} args0 args1 args3 :
All2_prop_eq Γ Δ f g
(λ (Γ Δ : context) (x y : term),
(pred1 Σ Γ Δ x y ×
(∀ Δ' r, pred1 Σ Γ Δ' x r →
∃ Δ'' v, pred1 Σ Δ Δ'' y v × pred1 Σ Δ' Δ'' r v))%type)
args0 args1 →
All2 (on_Trel_eq (pred1 Σ Γ Δ) f g) args0 args3 →
All2 (fun x y ⇒
(∃ Δ'' v, (pred1 Σ Δ Δ'' (f x) v × pred1 Σ Δ Δ'' (f y) v)) × (g x = g y))%type args1 args3.
Lemma All2_prop_All2 {Σ Γ Δ} args0 args1 args3 :
All2_prop Γ
(λ (Γ : context) (x y : term),
(pred1 Σ Γ Δ x y ×
(∀ Δ' r, pred1 Σ Γ Δ' x r →
∃ Δ'' v, pred1 Σ Δ Δ'' y v × pred1 Σ Δ' Δ'' r v))%type)
args0 args1 →
All2 (pred1 Σ Γ Δ) args0 args3 →
All2 (fun x y ⇒
∃ Δ'' v, pred1 Σ Δ Δ'' x v × pred1 Σ Δ Δ'' y v)%type args1 args3.
Definition on_Trel2 {A B} (R : A → A → Type) (f : B → A) : B → A → Type :=
fun x y ⇒ R (f x) y.
Lemma All2_on_Trel_eq_impl {A B} Σ Γ Δ {f : A → term} {g : A → B} {x y} :
All2 (on_Trel_eq (pred1 Σ Γ Δ) f g) x y →
All2 (on_Trel (pred1 Σ Γ Δ) f) x y.
Lemma isConstruct_app_inv t :
isConstruct_app t = true →
∃ ind k u args, t = mkApps (tConstruct ind k u) args.
Lemma All2_nth_error_Some_right {A} {P : A → A → Type} {l l'} n t :
All2 P l l' →
nth_error l' n = Some t →
{ t' : A & (nth_error l n = Some t') × P t' t}%type.
Lemma All2_local_env_skipn P l l' n :
All2_local_env P l l' →
All2_local_env P (skipn n l) (skipn n l').
Equations construct_cofix_discr (t : term) : bool :=
construct_cofix_discr (tConstruct _ _ _) ⇒ true;
construct_cofix_discr (tCoFix _ _) ⇒ true;
construct_cofix_discr _ ⇒ false.
Equations discr_construct_cofix (t : term) : Prop :=
{ | tConstruct _ _ _ ⇒ False;
| tCoFix _ _ ⇒ False;
| _ ⇒ True }.
Inductive construct_cofix_view : term → Set :=
| construct_cofix_construct c u i : construct_cofix_view (tConstruct c u i)
| construct_cofix_cofix mfix idx : construct_cofix_view (tCoFix mfix idx)
| construct_cofix_other t : discr_construct_cofix t → construct_cofix_view t.
Equations view_construct_cofix (t : term) : construct_cofix_view t :=
{ | tConstruct ind u i ⇒ construct_cofix_construct ind u i;
| tCoFix mfix idx ⇒ construct_cofix_cofix mfix idx;
| t ⇒ construct_cofix_other t I }.
Equations isConstruct (t : term) : bool :=
isConstruct (tConstruct _ _ _) ⇒ true;
isConstruct _ ⇒ false.
Inductive construct_view : term → Set :=
| construct_construct c u i : construct_view (tConstruct c u i)
| construct_other t : ~~ isConstruct t → construct_view t.
Equations view_construct (t : term) : construct_view t :=
{ | tConstruct ind u i ⇒ construct_construct ind u i;
| t ⇒ construct_other t eq_refl }.
Fixpoint isFix_app (t : term) : bool :=
match t with
| tApp (tFix _ _) _ ⇒ true
| tApp f _ ⇒ isFix_app f
| _ ⇒ false
end.
Inductive fix_app_view : term → Set :=
| fix_app_fix mfix i l : l ≠ [] → fix_app_view (mkApps (tFix mfix i) l)
| fix_app_other t : ~~ isFix_app t → fix_app_view t.
Lemma view_fix_app (t : term) : fix_app_view t.
Definition isFixLambda (t : term) : bool :=
match t with
| tFix _ _ ⇒ true
| tLambda _ _ _ ⇒ true
| _ ⇒ false
end.
Inductive fix_lambda_view : term → Set :=
| fix_lambda_lambda na b t : fix_lambda_view (tLambda na b t)
| fix_lambda_fix mfix i : fix_lambda_view (tFix mfix i)
| fix_lambda_other t : ~~ isFixLambda t → fix_lambda_view t.
Lemma view_fix_lambda (t : term) : fix_lambda_view t.
Section All2_telescope.
Context (P : ∀ (Γ Γ' : context), option (term × term) → term → term → Type).
Definition telescope := context.
Inductive All2_telescope (Γ Γ' : context) : telescope → telescope → Type :=
| telescope2_nil : All2_telescope Γ Γ' [] []
| telescope2_cons_abs na t t' Δ Δ' :
P Γ Γ' None t t' →
All2_telescope (Γ ,, vass na t) (Γ' ,, vass na t') Δ Δ' →
All2_telescope Γ Γ' (vass na t :: Δ) (vass na t' :: Δ')
| telescope2_cons_def na b b' t t' Δ Δ' :
P Γ Γ' (Some (b, b')) t t' →
All2_telescope (Γ ,, vdef na b t) (Γ' ,, vdef na b' t') Δ Δ' →
All2_telescope Γ Γ' (vdef na b t :: Δ) (vdef na b' t' :: Δ').
End All2_telescope.
Section All2_telescope_n.
Context (P : ∀ (Γ Γ' : context), option (term × term) → term → term → Type).
Context (f : nat → term → term).
Inductive All2_telescope_n (Γ Γ' : context) (n : nat) : telescope → telescope → Type :=
| telescope_n_nil : All2_telescope_n Γ Γ' n [] []
| telescope_n_cons_abs na t t' Δ Δ' :
P Γ Γ' None (f n t) (f n t') →
All2_telescope_n (Γ ,, vass na (f n t)) (Γ' ,, vass na (f n t')) (S n) Δ Δ' →
All2_telescope_n Γ Γ' n (vass na t :: Δ) (vass na t' :: Δ')
| telescope_n_cons_def na b b' t t' Δ Δ' :
P Γ Γ' (Some (f n b, f n b')) (f n t) (f n t') →
All2_telescope_n (Γ ,, vdef na (f n b) (f n t)) (Γ' ,, vdef na (f n b') (f n t'))
(S n) Δ Δ' →
All2_telescope_n Γ Γ' n (vdef na b t :: Δ) (vdef na b' t' :: Δ').
End All2_telescope_n.
Lemma All2_telescope_mapi {P} Γ Γ' Δ Δ' (f : nat → term → term) k :
All2_telescope_n (on_decl P) f Γ Γ' k Δ Δ' →
All2_telescope (on_decl P) Γ Γ' (mapi_rec (fun n ⇒ map_decl (f n)) Δ k)
(mapi_rec (fun n ⇒ map_decl (f n)) Δ' k).
Lemma local_env_telescope P Γ Γ' Δ Δ' :
All2_telescope (on_decl P) Γ Γ' Δ Δ' →
All2_local_env_over P Γ Γ' (List.rev Δ) (List.rev Δ').
Lemma lookup_env_cst_inv {Σ c k cst} :
lookup_env Σ c = Some (ConstantDecl k cst) → c = k.
Definition isLambda_or_Fix_app t :=
match fst (decompose_app t) with
| tLambda _ _ _ ⇒ true
| tFix _ _ ⇒ true
| _ ⇒ false
end.
Lemma decompose_app_rec_head t l f : fst (decompose_app_rec t l) = f →
~~ isApp f.
Lemma isLambda_or_Fix_app_decompose_app t :
~~ isLambda_or_Fix_app t →
∀ l', ~~ isLambda_or_Fix_app (fst (decompose_app_rec t l')).
Section TriangleFn.
Context (Σ : global_env).
Definition map_fix (rho : context → term → term) Γ mfixctx (mfix : mfixpoint term) :=
(map (map_def (rho Γ) (rho (Γ ,,, mfixctx))) mfix).
Fixpoint rho Γ t : term :=
match t with
| tApp (tLambda na T b) u ⇒ (rho (vass na (rho Γ T) :: Γ) b) {0 := rho Γ u}
| tLetIn na d t b ⇒ (subst10 (rho Γ d) (rho (vdef na (rho Γ d) (rho Γ t) :: Γ) b))
| tRel i ⇒
match option_map decl_body (nth_error Γ i) with
| Some (Some body) ⇒ (lift0 (S i) body)
| Some None ⇒ tRel i
| None ⇒ tRel i
end
| tCase (ind, pars) p x brs ⇒
let p' := rho Γ p in
let x' := rho Γ x in
let brs' := List.map (fun x ⇒ (fst x, rho Γ (snd x))) brs in
match decompose_app x, decompose_app x' with
| (tConstruct ind' c u, args), (tConstruct ind'' c' u', args') ⇒
if eqb ind ind' then
iota_red pars c args' brs'
else tCase (ind, pars) p' x' brs'
| (tCoFix mfix idx, args), (tCoFix mfix' idx', args') ⇒
match unfold_cofix mfix' idx with
| Some (narg, fn) ⇒
tCase (ind, pars) p' (mkApps fn args') brs'
| None ⇒ tCase (ind, pars) p' (mkApps (tCoFix mfix' idx) args') brs'
end
| _, _ ⇒ tCase (ind, pars) p' x' brs'
end
| tProj ((i, pars, narg) as p) x ⇒
let x' := rho Γ x in
match decompose_app x, decompose_app x' with
| (tConstruct ind c u, args), (tConstruct ind' c' u', args') ⇒
match nth_error args' (pars + narg) with
| Some arg1 ⇒
if eqb i ind' then arg1
else tProj p x'
| None ⇒ tProj p x'
end
| (tCoFix mfix idx, args), (tCoFix mfix' idx', args') ⇒
match unfold_cofix mfix' idx with
| Some (narg, fn) ⇒ tProj p (mkApps fn args')
| None ⇒ tProj p (mkApps (tCoFix mfix' idx') args')
end
| _, _ ⇒ tProj p x'
end
| tConst c u ⇒
match lookup_env Σ c with
| Some (ConstantDecl id decl) ⇒
match decl.(cst_body) with
| Some body ⇒ subst_instance_constr u body
| None ⇒ tConst c u
end
| _ ⇒ tConst c u
end
| tApp t u ⇒
let t' := rho Γ t in
let u' := rho Γ u in
match decompose_app (tApp t u), decompose_app (tApp t' u') with
| (tFix mfix0 idx0, args0), (tFix mfix1 idx1, args1) ⇒
match unfold_fix mfix1 idx1 with
| Some (rarg, fn) ⇒
if is_constructor rarg args1 then
mkApps fn args1
else tApp t' u'
| None ⇒ tApp t' u'
end
| _, _ ⇒ tApp t' u'
end
| tLambda na t u ⇒ tLambda na (rho Γ t) (rho (vass na (rho Γ t) :: Γ) u)
| tProd na t u ⇒ tProd na (rho Γ t) (rho (vass na (rho Γ t) :: Γ) u)
| tVar i ⇒ tVar i
| tEvar n l ⇒ tEvar n (map (rho Γ) l)
| tSort s ⇒ tSort s
| tFix mfix idx ⇒
let mfixctx := fold_fix_context rho Γ [] mfix in
tFix (map_fix rho Γ mfixctx mfix) idx
| tCoFix mfix idx ⇒
let mfixctx := fold_fix_context rho Γ [] mfix in
tCoFix (map_fix rho Γ mfixctx mfix) idx
| tInd _ _ | tConstruct _ _ _ ⇒ t
end.
Section rho_ctx.
Context (Δ : context).
Fixpoint rho_ctx_over Γ :=
match Γ with
| [] ⇒ []
| {| decl_name := na; decl_body := None; decl_type := T |} :: Γ ⇒
let Γ' := rho_ctx_over Γ in
vass na (rho (Δ ,,, Γ') T) :: Γ'
| {| decl_name := na; decl_body := Some b; decl_type := T |} :: Γ ⇒
let Γ' := rho_ctx_over Γ in
vdef na (rho (Δ ,,, Γ') b) (rho (Δ ,,, Γ') T) :: Γ'
end.
End rho_ctx.
Definition rho_ctx Γ := (rho_ctx_over [] Γ).
Lemma rho_ctx_over_length Δ Γ : #|rho_ctx_over Δ Γ| = #|Γ|.
Lemma rho_ctx_over_app Γ' Γ Δ :
rho_ctx_over Γ' (Γ ,,, Δ) =
rho_ctx_over Γ' Γ ,,, rho_ctx_over (Γ' ,,, rho_ctx_over Γ' Γ) Δ.
Lemma rho_ctx_app Γ Δ : rho_ctx (Γ ,,, Δ) = rho_ctx Γ ,,, rho_ctx_over (rho_ctx Γ) Δ.
Lemma rho_triangle_All_All2_ind:
∀ (Γ : context) (brs : list (nat × term)),
pred1_ctx Σ Γ (rho_ctx Γ) →
All (λ x : nat × term, pred1_ctx Σ Γ (rho_ctx Γ) → pred1 Σ Γ (rho_ctx Γ) (snd x) (rho (rho_ctx Γ) (snd x)))
brs →
All2 (on_Trel_eq (pred1 Σ Γ (rho_ctx Γ)) snd fst) brs
(map (λ x : nat × term, (fst x, rho (rho_ctx Γ) (snd x))) brs).
Lemma rho_All_All2_local_env :
∀ Γ : context, pred1_ctx Σ Γ (rho_ctx Γ) → ∀ Δ : context,
All_local_env
(on_local_decl
(λ (Γ' : context) (t : term),
pred1_ctx Σ (Γ ,,, Γ') (rho_ctx (Γ ,,, Γ')) →
pred1 Σ (Γ ,,, Γ')
(rho_ctx (Γ ,,, Γ')) t
(rho (rho_ctx (Γ ,,, Γ')) t))
) Δ
→ All2_local_env (on_decl (on_decl_over (pred1 Σ) Γ (rho_ctx Γ))) Δ
(rho_ctx_over (rho_ctx Γ) Δ).
Lemma rho_All_All2_local_env' :
∀ Γ : context, pred1_ctx Σ Γ (rho_ctx Γ) → ∀ Δ Δ' : context,
All2_local_env
(on_decl
(λ (Γ' Γ'' : context) (t t' : term), pred1_ctx Σ (Γ ,,, Γ') (rho_ctx (Γ ,,, Γ''))
→ pred1 Σ (Γ ,,, Γ')
(rho_ctx (Γ ,,, Γ'')) t
(rho (rho_ctx (Γ ,,, Γ'')) t'))) Δ Δ'
→ All2_local_env (on_decl (on_decl_over (pred1 Σ) Γ (rho_ctx Γ))) Δ
(rho_ctx_over (rho_ctx Γ) Δ').
Lemma rho_All_All2_local_env_inv :
∀ Γ Γ' : context, pred1_ctx Σ Γ' (rho_ctx Γ) → ∀ Δ Δ' : context,
All2_local_env (on_decl (on_decl_over (pred1 Σ) Γ' (rho_ctx Γ))) Δ
(rho_ctx_over (rho_ctx Γ) Δ') →
All2_local_env
(on_decl
(λ (Δ Δ' : context) (t t' : term), pred1 Σ (Γ' ,,, Δ)
(rho_ctx (Γ ,,, Δ')) t
(rho (rho_ctx (Γ ,,, Δ')) t'))) Δ Δ'.
Lemma nth_error_rho_ctx {Γ n c} :
nth_error Γ n = Some c →
nth_error (rho_ctx Γ) n = Some (map_decl (rho (rho_ctx (skipn (S n) Γ))) c).
Lemma map_cofix_subst (f : context → term → term)
(f' : context → context → term → term) mfix Γ Γ' :
(∀ n, tCoFix (map (map_def (f Γ) (f' Γ Γ')) mfix) n = f Γ (tCoFix mfix n)) →
cofix_subst (map (map_def (f Γ) (f' Γ Γ')) mfix) =
map (f Γ) (cofix_subst mfix).
Lemma fold_fix_context_rev_mapi {Γ l m} :
fold_fix_context rho Γ l m =
List.rev (mapi (λ (i : nat) (x : def term),
vass (dname x) ((lift0 (#|l| + i)) (rho Γ (dtype x)))) m) ++ l.
Lemma fold_fix_context_rev {Γ m} :
fold_fix_context rho Γ [] m =
List.rev (mapi (λ (i : nat) (x : def term),
vass (dname x) (lift0 i (rho Γ (dtype x)))) m).
Lemma nth_error_map_fix i f Γ Δ m :
nth_error (map_fix f Γ Δ m) i = option_map (map_def (f Γ) (f (Γ ,,, Δ))) (nth_error m i).
Lemma fold_fix_context_length f Γ l m : #|fold_fix_context f Γ l m| = #|m| + #|l|.
Lemma All_local_env_Alli P ctx :
All_local_env (on_local_decl P) ctx →
Alli (fun n decl ⇒
P (skipn (S n) ctx) (decl_type decl)) 0 ctx.
Lemma All_local_env_fix_Alli P m :
All_local_env (on_local_decl P) (fix_context m) →
Alli (fun n def ⇒
P (skipn (S n) (fix_context m)) (lift0 (Nat.pred #|m| - n) (dtype def)))%type 0 (List.rev m).
Context `{cf : checker_flags} (wfΣ : wf Σ).
Lemma fold_ctx_over_eq Γ Γ' : rho_ctx_over Γ Γ' = fold_ctx_over rho Γ Γ'.
Section foldover.
Context (Γ Γ' : context).
Fixpoint fold_fix_context_over acc m :=
match m with
| [] ⇒ acc
| def :: fixd ⇒
fold_fix_context_over
(vass def.(dname) (lift #|acc| #|Γ'| (rho (Γ ,,, Γ') def.(dtype))) :: acc) fixd
end.
End foldover.
Lemma fold_fix_context_over2 Γ acc m :
fold_fix_context_over Γ [] acc m =
fold_fix_context rho Γ acc m.
Lemma fold_fix_context_over_acc' Γ Δ m :
(All (fun d ⇒
∀ Δ,
rho ( Δ ++ Γ) ((lift #|Δ| 0 ) (dtype d)) =
(lift #|Δ| 0) (rho (Γ ) (dtype d))) m) →
rho_ctx_over (Γ ,,, Δ )
((List.rev (mapi_rec (λ (i : nat) (d : def term),
vass (dname d) ((lift i 0) (dtype d))) m #|Δ|)))
++ Δ =
fold_fix_context_over Γ [] Δ m.
Lemma fold_fix_context_over' Γ m :
(All (fun d ⇒
∀ Δ,
rho (Δ ++ Γ) ((lift0 #|Δ|) (dtype d)) =
(lift0 #|Δ|) (rho Γ (dtype d))) m) →
rho_ctx_over Γ (fix_context m) =
fold_fix_context rho Γ [] m.
Lemma fold_fix_context_app Γ l acc acc' :
fold_fix_context rho Γ l (acc ++ acc') =
fold_fix_context rho Γ (fold_fix_context rho Γ l acc) acc'.
Definition ctxmap (Γ Δ : context) (s : nat → term) :=
∀ x d, nth_error Γ x = Some d →
match decl_body d return Type with
| Some b ⇒
∑ i b', s x = tRel i ∧
option_map decl_body (nth_error Δ i) = Some (Some b') ∧
b'.[↑^(S i)] = b.[↑^(S x) ∘ s]
| None ⇒ True
end.
Lemma simpl_pred Γ Γ' t t' u u' : t = t' → u = u' → pred1 Σ Γ Γ' t' u' → pred1 Σ Γ Γ' t u.
Lemma pred_atom_inst t σ : pred_atom t → t.[σ] = t.
Lemma All2_prop2_eq_split (Γ Γ' Γ2 Γ2' : context) (A B : Type) (f g : A → term)
(h : A → B) (rel : context → context → term → term → Type) x y :
All2_prop2_eq Γ Γ' Γ2 Γ2' f g h rel x y →
All2 (on_Trel (rel Γ Γ') f) x y ×
All2 (on_Trel (rel Γ2 Γ2') g) x y ×
All2 (on_Trel eq h) x y.
Lemma refine_pred Γ Δ t u u' : u = u' → pred1 Σ Γ Δ t u' → pred1 Σ Γ Δ t u.
Inductive assumption_context : context → Prop :=
| assumption_context_nil : assumption_context []
| assumption_context_vass na t Γ : assumption_context Γ → assumption_context (vass na t :: Γ).
Lemma fix_context_assumption_context m : assumption_context (fix_context m).
Lemma nth_error_assumption_context Γ n d :
assumption_context Γ → nth_error Γ n = Some d →
decl_body d = None.
Lemma ctxmap_ext Γ Δ : CMorphisms.Proper (CMorphisms.respectful (pointwise_relation _ eq) isEquiv) (ctxmap Γ Δ).
Lemma Up_ctxmap Γ Δ c c' σ :
ctxmap Γ Δ σ →
(decl_body c' = option_map (fun x ⇒ x.[σ]) (decl_body c)) →
ctxmap (Γ ,, c) (Δ ,, c') (⇑ σ).
Inductive All2i {A B : Type} (R : nat → A → B → Type) : list A → list B → Type :=
All2i_nil : All2i R [] []
| All2i_cons : ∀ (x : A) (y : B) (l : list A) (l' : list B),
R (List.length l) x y → All2i R l l' → All2i R (x :: l) (y :: l').
Definition pres_bodies Γ Δ σ :=
All2i (fun n decl decl' ⇒ (decl_body decl' = option_map (fun x ⇒ x.[⇑^n σ]) (decl_body decl)))
Γ Δ.
Lemma Upn_ctxmap Γ Δ Γ' Δ' σ :
pres_bodies Γ' Δ' σ →
ctxmap Γ Δ σ →
ctxmap (Γ ,,, Γ') (Δ ,,, Δ') (⇑^#|Γ'| σ).
Definition pred1_subst Γ Δ Δ' σ τ :=
∀ x, pred1 Σ Δ Δ' (σ x) (τ x) ×
match option_map decl_body (nth_error Γ x) return Type with
| Some (Some b) ⇒ σ x = τ x
| _ ⇒ True
end.
Lemma pred1_subst_pred1_ctx {Γ Δ Δ' σ τ} :
pred1_subst Γ Δ Δ' σ τ →
pred1_ctx Σ Δ Δ'.
Lemma pred1_subst_Up:
∀ (Γ : context) (na : name) (t0 t1 : term) (Δ Δ' : context) (σ τ : nat → term),
pred1 Σ Δ Δ' t0.[σ] t1.[τ] →
pred1_subst Γ Δ Δ' σ τ →
pred1_subst (Γ,, vass na t0) (Δ,, vass na t0.[σ]) (Δ',, vass na t1.[τ]) (⇑ σ) (⇑ τ).
Lemma pred1_subst_vdef_Up:
∀ (Γ : context) (na : name) (b0 b1 t0 t1 : term) (Δ Δ' : context) (σ τ : nat → term),
pred1 Σ Δ Δ' t0.[σ] t1.[τ] →
pred1 Σ Δ Δ' b0.[σ] b1.[τ] →
pred1_subst Γ Δ Δ' σ τ →
pred1_subst (Γ,, vdef na b0 t0) (Δ,, vdef na b0.[σ] t0.[σ]) (Δ',, vdef na b1.[τ] t1.[τ]) (⇑ σ) (⇑ τ).
Lemma pred1_subst_Upn:
∀ (Γ : context) (Δ Δ' : context) (σ τ : nat → term) (Γ' Δ0 Δ1 : context) n,
#|Γ'| = #|Δ0| → #|Δ0| = #|Δ1| → n = #|Δ0| →
pred1_subst Γ Δ Δ' σ τ →
All2_local_env_over (pred1 Σ) Δ Δ' Δ0 Δ1 →
pred1_subst (Γ ,,, Γ') (Δ ,,, Δ0) (Δ' ,,, Δ1) (⇑^n σ) (⇑^n τ).
Lemma inst_mkApps f l σ : (mkApps f l).[σ] = mkApps f.[σ] (map (inst σ) l).
Lemma inst_iota_red s pars c args brs :
inst s (iota_red pars c args brs) =
iota_red pars c (List.map (inst s) args) (List.map (on_snd (inst s)) brs).
Lemma All2_local_env_fold_context P f g Γ Δ :
All2_local_env (fun Γ Δ p T U ⇒ P (fold_context f Γ) (fold_context g Δ)
(option_map (fun '(b, b') ⇒ (f #|Γ| b, g #|Δ| b')) p)
(f #|Γ| T) (g #|Δ| U)) Γ Δ →
All2_local_env P (fold_context f Γ) (fold_context g Δ).
Lemma All2_local_env_fix_context P σ τ Γ Δ :
All2_local_env (fun Γ Δ p T U ⇒ P (inst_context σ Γ) (inst_context τ Δ)
(option_map (fun '(b, b') ⇒ (b.[⇑^#|Γ| σ], b'.[⇑^#|Δ| τ])) p)
(T.[⇑^#|Γ| σ]) (U.[⇑^#|Δ| τ])) Γ Δ →
All2_local_env P (inst_context σ Γ) (inst_context τ Δ).
Lemma All2_local_env_impl P Q Γ Δ :
All2_local_env P Γ Δ →
(∀ Γ Δ t T U, #|Γ| = #|Δ| → P Γ Δ t T U → Q Γ Δ t T U) →
All2_local_env Q Γ Δ.
Lemma decompose_app_rec_inst s t l :
let (f, a) := decompose_app_rec t l in
inst s f = f →
decompose_app_rec (inst s t) (map (inst s) l) = (f, map (inst s) a).
Lemma decompose_app_inst s t f a :
decompose_app t = (f, a) → inst s f = f →
decompose_app (inst s t) = (inst s f, map (inst s) a).
Lemma inst_is_constructor:
∀ (args : list term) (narg : nat) s,
is_constructor narg args = true → is_constructor narg (map (inst s) args) = true.
Lemma map_fix_subst f g mfix :
(∀ n, tFix (map (map_def f g) mfix) n = f (tFix mfix n)) →
fix_subst (map (map_def f g) mfix) =
map f (fix_subst mfix).
Lemma map_cofix_subst' f g mfix :
(∀ n, tCoFix (map (map_def f g) mfix) n = f (tCoFix mfix n)) →
cofix_subst (map (map_def f g) mfix) =
map f (cofix_subst mfix).
Lemma subst_consn_compose l σ' σ : l ⋅n σ' ∘ σ =1 (map (inst σ) l ⋅n (σ' ∘ σ)).
Lemma map_idsn_spec (f : term → term) (n : nat) :
map f (idsn n) = Nat.recursion [] (fun x l ⇒ l ++ [f (tRel x)]) n.
Lemma nat_recursion_ext {A} (x : A) f g n :
(∀ x l', x < n → f x l' = g x l') →
Nat.recursion x f n = Nat.recursion x g n.
Lemma id_nth_spec {A} (l : list A) :
l = Nat.recursion [] (fun x l' ⇒
match nth_error l x with
| Some a ⇒ l' ++ [a]
| None ⇒ l'
end) #|l|.
Lemma Upn_comp n l σ : n = #|l| → ⇑^n σ ∘ (l ⋅n ids) =1 l ⋅n σ.
Lemma shift_Up_comm σ : ↑ ∘ ⇑ σ =1 σ ∘ ↑.
Lemma pres_bodies_inst_context Γ σ : pres_bodies Γ (inst_context σ Γ) σ.
Lemma inst_closed0 σ t : closedn 0 t → t.[σ] = t.
Lemma isLambda_inst t σ : isLambda t → isLambda t.[σ].
Lemma isLambda_subst t s : isLambda t → isLambda (subst0 s t).
Lemma strong_substitutivity Γ Γ' Δ Δ' s t σ τ :
pred1 Σ Γ Γ' s t →
ctxmap Γ Δ σ →
ctxmap Γ' Δ' τ →
pred1_subst Γ Δ Δ' σ τ →
pred1 Σ Δ Δ' s.[σ] t.[τ].
Beta case
Definition rho_ctxmap φ (Γ Δ : context) (s : nat → term) :=
∀ x d, nth_error Γ x = Some d →
match decl_body d return Type with
| Some b ⇒ ∑ i, (s x = tRel i) ×
(option_map decl_body (nth_error Δ i) = Some (Some b.[↑^(S x) ∘ s]))
| None ⇒ (Σ, φ) ;;; Δ |- s x : d.(decl_type).[↑^(S x) ∘ s]
end.
Definition renaming Γ Δ r :=
∀ x, match nth_error Γ x with
| Some d ⇒
match decl_body d return Prop with
| Some b ⇒
∃ b', option_map decl_body (nth_error Δ (r x)) = Some (Some b') ∧
b'.[↑^(S (r x))] = b.[↑^(S x) ∘ ren r]
| None ⇒ option_map decl_body (nth_error Δ (r x)) = Some None
end
| None ⇒ nth_error Δ (r x) = None
end.
Instance renaming_ext Γ Δ : Morphisms.Proper (`=1` ==> iff)%signature (renaming Γ Δ).
Lemma shiftn1_renaming Γ Δ c c' r :
renaming Γ Δ r →
(decl_body c' = option_map (fun x ⇒ x.[ren r]) (decl_body c)) →
renaming (c :: Γ) (c' :: Δ) (shiftn 1 r).
Lemma shift_renaming Γ Δ ctx ctx' r :
All2i (fun n decl decl' ⇒ (decl_body decl' = option_map (fun x ⇒ x.[ren (shiftn n r)]) (decl_body decl)))
ctx ctx' →
renaming Γ Δ r →
renaming (Γ ,,, ctx) (Δ ,,, ctx') (shiftn #|ctx| r).
Definition isFix (t : term) : bool :=
match t with
| tFix _ _ ⇒ true
| _ ⇒ false
end.
Definition discr_fix (t : term) : Prop :=
match t with
| tFix _ _ ⇒ False
| _ ⇒ True
end.
Inductive fix_view : term → Set :=
| fix_fix mfix i : fix_view (tFix mfix i)
| fix_other t : discr_fix t → fix_view t.
Lemma view_fix (t : term) : fix_view t.
Lemma fold_mkApps_tApp f l a : mkApps (tApp f a) l = mkApps f (a :: l).
Lemma fold_tApp f a : tApp f a = mkApps f [a].
Lemma isFix_app_false mfix idx l : l ≠ [] → ~~ isFix_app (mkApps (tFix mfix idx) l) → False.
Definition lambda_app_discr (t : term) : bool :=
match t with
| tApp (tLambda _ _ _) _ ⇒ true
| _ ⇒ false
end.
Inductive lambda_app_view : term → Set :=
| lambda_app_fix na t b a : lambda_app_view (tApp (tLambda na t b) a)
| lambda_app_other t : ~~ lambda_app_discr t → lambda_app_view t.
Lemma view_lambda_app (t : term) : lambda_app_view t.
Lemma isFix_app_tapp f x : ~~ isFix_app (tApp f x) → ~~ isFix_app f.
Lemma discr_fix_match (P : Type)
(p : mfixpoint term → nat → P)
(q : P) :
∀ t l, l ≠ [] → ~~ isFix_app (mkApps t l) →
(match t with tFix mfix idx ⇒ p mfix idx | _ ⇒ q end) = q.
Definition rho_fix Γ t l :=
let t' := rho Γ t in
let u' := map (rho Γ) l in
match t' with
| tFix mfix1 idx1 ⇒
match unfold_fix mfix1 idx1 with
| Some (rarg, fn) ⇒
if is_constructor rarg u' then
mkApps fn u'
else mkApps t' u'
| None ⇒ mkApps t' u'
end
| _ ⇒ mkApps t' u'
end.
Lemma last_app {A} (l l' : list A) d : l' ≠ [] → last (l ++ l') d = last l' d.
Lemma mkApps_tApp_tApp f a l :
mkApps (tApp f a) l = tApp (mkApps f (removelast (a :: l))) (List.last l a).
Lemma decompose_app_rec_non_nil f l :
l ≠ [] →
∀ t' l', decompose_app_rec f l = (t', l') → l' ≠ [].
Lemma isLambda_nisApp t : isLambda t → ~~ isApp t.
Lemma rho_fix_unfold Γ mfix idx l :
rho Γ (mkApps (tFix mfix idx) l) = rho_fix Γ (tFix mfix idx) l.
Definition rho_fix_context Γ mfix :=
fold_fix_context rho Γ [] mfix.
Lemma rho_fix_context_length Γ mfix : #|rho_fix_context Γ mfix| = #|mfix|.
Lemma isLambda_rho Γ t : isLambda t → isLambda (rho Γ t).
Lemma nisLambda_rho Γ t : ~~ isLambda (rho Γ t) → ~~ isLambda t.
Lemma rho_fix_unfold_inv Γ mfix i l :
match nth_error mfix i with
| Some d ⇒
let fn := (subst0 (map (rho Γ) (fix_subst mfix))) (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) in
if isLambda (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) && is_constructor (rarg d) (map (rho Γ) l) then
(rho Γ (mkApps (tFix mfix i) l) = mkApps fn (map (rho Γ) l))
else
rho Γ (mkApps (tFix mfix i) l) = mkApps (rho Γ (tFix mfix i)) (map (rho Γ) l)
| None ⇒ rho Γ (mkApps (tFix mfix i) l) = mkApps (rho Γ (tFix mfix i)) (map (rho Γ) l)
end.
Inductive rho_fix_spec Γ mfix i l : term → Type :=
| rho_fix_red d :
let fn := (subst0 (map (rho Γ) (fix_subst mfix))) (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) in
nth_error mfix i = Some d →
isLambda (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) && is_constructor (rarg d) (map (rho Γ) l) →
rho_fix_spec Γ mfix i l (mkApps fn (map (rho Γ) l))
| rho_fix_stuck :
(match nth_error mfix i with
| None ⇒ True
| Some d ⇒
let fn := (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) in
~~ isLambda fn ∨ ~~ is_constructor (rarg d) (map (rho Γ) l)
end) →
rho_fix_spec Γ mfix i l (mkApps (rho Γ (tFix mfix i)) (map (rho Γ) l)).
Lemma rho_fix_elim Γ mfix i l :
rho_fix_spec Γ mfix i l (rho Γ (mkApps (tFix mfix i) l)).
Definition rho_app Γ t :=
let '(hd, args) := decompose_app t in
match hd with
| tLambda na dom b ⇒
match args with
| a :: args ⇒ mkApps (rho Γ (tApp hd a)) (map (rho Γ) args)
| [] ⇒ rho Γ t
end
| tFix _ _ ⇒ rho_fix Γ hd args
| _ ⇒ mkApps (rho Γ hd) (map (rho Γ) args)
end.
Lemma discr_fix_eq (A : Type) (a : mfixpoint term → nat → A) (b c : A) t :
~~ isFix t →
b = c →
match t with
| tFix mfix idx ⇒ a mfix idx
| _ ⇒ b
end = c.
Lemma is_constructor_app_ge n l l' : is_constructor n l → is_constructor n (l ++ l').
Lemma isLambda_nisFix t : isLambda t → ~~ isFix t.
Lemma rho_app_unfold Γ t : rho Γ t = rho_app Γ t.
Definition lambda_discr (t : term) : bool :=
match t with
| tLambda _ _ _ ⇒ true
| _ ⇒ false
end.
Lemma discr_lambda_fix_eq (A : Type) (a b c d : A) t :
¬ isFix t → ¬ lambda_discr t →
c = d →
match t with
| tFix _ _ ⇒ a
| tLambda _ _ _ ⇒ b
| _ ⇒ c
end = d.
Lemma rho_app_discr_aux Γ f a :
¬ isLambda f →
~~ isFix_app (tApp f a) →
rho_app Γ (tApp f a) = tApp (rho Γ f) (rho Γ a).
Lemma rho_mkApps_non_nil Γ f l :
~~ isLambda f → l ≠ nil → ~~ isApp f → ~~ isFix f →
rho Γ (mkApps f l) = mkApps (rho Γ f) (map (rho Γ) l).
Lemma rho_mkApps Γ f l :
~~ isApp f → ~~ isLambda f → ~~ isFix f →
rho Γ (mkApps f l) = mkApps (rho Γ f) (map (rho Γ) l).
Lemma decompose_app_rec_inv' f l hd args : decompose_app_rec f l = (hd, args) →
~~ isApp hd ∧ mkApps f l = mkApps hd args.
Lemma decompose_app_inv' f hd args : decompose_app f = (hd, args) →
~~ isApp hd ∧ f = mkApps hd args.
Lemma mkApps_eq_app f l f' a :
~~ isApp f →
mkApps f l = tApp f' a →
l ≠ nil ∧ a = last l a ∧ f' = mkApps f (removelast l).
Lemma discr_lambda_app_isLambda f a : ~~ lambda_app_discr (tApp f a) ↔ ¬ isLambda f.
Lemma rho_tApp_discr Γ f a :
~~ lambda_app_discr (tApp f a) →
~~ isFix_app (tApp f a) →
rho Γ (tApp f a) = tApp (rho Γ f) (rho Γ a).
Lemma discr_fix_app_mkApps f args : ~~ isApp f → ~~ isFix f → ~~ isFix_app (mkApps f args).
Lemma discr_lambda_app_rename r f :
lambda_app_discr f = lambda_app_discr (rename r f).
Lemma isFix_app_rename r f :
isFix_app f = isFix_app (rename r f).
Lemma isConstruct_app_rho Γ t : isConstruct_app t → isConstruct_app (rho Γ t).
Lemma rename_mkApps r f l: rename r (mkApps f l) = mkApps (rename r f) (map (rename r) l).
Lemma isConstruct_app_rename r t :
isConstruct_app t = isConstruct_app (rename r t).
Lemma mfixpoint_size_nth_error {mfix i d} :
nth_error mfix i = Some d →
size (dbody d) < mfixpoint_size size mfix.
Lemma All2i_app {A B} (P : nat → A → B → Type) l0 l0' l1 l1' :
All2i P l0' l1' →
All2i (fun n ⇒ P (n + #|l0'|)) l0 l1 →
All2i P (l0 ++ l0') (l1 ++ l1').
Lemma All2i_length {A B} (P : nat → A → B → Type) l l' :
All2i P l l' → #|l| = #|l'|.
Lemma All2i_impl {A B} (P Q : nat → A → B → Type) l l' :
All2i P l l' → (∀ n x y, P n x y → Q n x y) → All2i Q l l'.
Lemma All2i_rev {A B} (P : nat → A → B → Type) l l' :
All2i P l l' →
All2i (fun n ⇒ P (#|l| - S n)) (List.rev l) (List.rev l').
Inductive All2i_ctx {A B : Type} (R : nat → A → B → Type) (n : nat) : list A → list B → Type :=
All2i_ctx_nil : All2i_ctx R n [] []
| All2i_ctx_cons : ∀ (x : A) (y : B) (l : list A) (l' : list B),
R n x y → All2i_ctx R (S n) l l' → All2i_ctx R n (x :: l) (y :: l').
Lemma All2i_ctx_app {A B} (P : nat → A → B → Type) n l0 l0' l1 l1' :
All2i_ctx P (n + #|l0|) l0' l1' →
All2i_ctx P n l0 l1 →
All2i_ctx P n (l0 ++ l0') (l1 ++ l1').
Lemma All2i_rev_ctx {A B} (R : nat → A → B → Type) (n : nat) (l : list A) (l' : list B) :
All2i R l l' → All2i_ctx R 0 (List.rev l) (List.rev l').
Lemma All2i_rev_ctx_gen {A B} (R : nat → A → B → Type) (n : nat) (l : list A) (l' : list B) :
All2i_ctx R n l l' → All2i (fun m ⇒ R (n + m)) (List.rev l) (List.rev l').
Lemma All2i_rev_ctx_inv {A B} (R : nat → A → B → Type) (l : list A) (l' : list B) :
All2i_ctx R 0 l l' → All2i R (List.rev l) (List.rev l').
Lemma All2i_ctx_mapi {A B C D} (R : nat → A → B → Type)
(l : list C) (l' : list D) (f : nat → C → A) (g : nat → D → B) n :
All2i_ctx (fun n x y ⇒ R n (f n x) (g n y)) n l l' →
All2i_ctx R n (mapi_rec f l n) (mapi_rec g l' n).
Lemma All2i_ctx_trivial {A B} (R : nat → A → B → Type) (H : ∀ n x y, R n x y) n l l' :
#|l| = #|l'| → All2i_ctx R n l l'.
Lemma mfixpoint_size_In {mfix d} :
In d mfix →
size (dbody d) < mfixpoint_size size mfix ∧
size (dtype d) < mfixpoint_size size mfix.
Lemma renaming_shift_rho_fix_context:
∀ (mfix : mfixpoint term) (Γ Δ : list context_decl) (r : nat → nat),
renaming Γ Δ r →
renaming (Γ ,,, rho_fix_context Γ mfix)
(Δ ,,, rho_fix_context Δ (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix))
(shiftn #|mfix| r).
Lemma map_fix_rho_rename:
∀ (mfix : mfixpoint term) (i : nat) (l : list term),
(∀ t' : term, size t' < size (mkApps (tFix mfix i) l)
→ ∀ (Γ Δ : list context_decl) (r : nat → nat),
renaming Γ Δ r
→ rename r (rho Γ t') = rho Δ (rename r t'))
→ ∀ (Γ Δ : list context_decl) (r : nat → nat),
renaming Γ Δ r
→ map (map_def (rename r) (rename (shiftn #|mfix| r)))
(map_fix rho Γ (fold_fix_context rho Γ [] mfix) mfix) =
map_fix rho Δ (fold_fix_context rho Δ [] (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix))
(map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix).
Lemma decompose_app_rec_rename r t l :
∀ hd args,
decompose_app_rec t l = (hd, args) →
decompose_app_rec (rename r t) (map (rename r) l) = (rename r hd, map (rename r) args).
Lemma decompose_app_rename {r t hd args} :
decompose_app t = (hd, args) →
decompose_app (rename r t) = (rename r hd, map (rename r) args).
Lemma nisConstruct_elim {A} {t} {a : inductive → nat → universe_instance → A} {b : A} :
~~ isConstruct t →
match t with
| tConstruct ind n u ⇒ a ind n u
| _ ⇒ b
end = b.
Lemma isConstruct_rename {r t} : ~~ isConstruct t → ~~ isConstruct (rename r t).
Lemma isLambda_rename r t : isLambda (rename r t) = isLambda t.
Lemma nth_nth_error {A} {i} {l : list A} {d v} :
nth i l d = v →
(nth_error l i = Some v) +
(nth_error l i = None ∧ v = d).
Lemma rho_rename Γ Δ r t :
renaming Γ Δ r →
rename r (rho Γ t) = rho Δ (rename r t).
Lemma ren_lift_renaming n k : ren (lift_renaming n k) =1 (⇑^k ↑^n).
Lemma shiftk_compose n m : ↑^n ∘ ↑^m =1 ↑^(n + m).
Lemma rho_lift0 Γ Δ t : lift0 #|Δ| (rho Γ t) = rho (Γ ,,, Δ) (lift0 #|Δ| t).
Lemma fold_fix_context_over_acc Γ m acc :
rho_ctx_over (rho_ctx Γ ,,, acc)
(List.rev (mapi_rec (λ (i : nat) (d : def term), vass (dname d) ((lift0 i) (dtype d))) m #|acc|))
++ acc =
fold_fix_context rho (rho_ctx Γ) acc m.
Lemma fold_fix_context_rho_ctx Γ m :
rho_ctx_over (rho_ctx Γ) (fix_context m) =
fold_fix_context rho (rho_ctx Γ) [] m.
Definition fold_fix_context_alt Γ m :=
mapi (fun k def ⇒ vass def.(dname) (lift0 k (rho Γ def.(dtype)))) m.
Lemma fix_context_fold Γ m :
fix_context (map (map_def (rho (rho_ctx Γ))
(rho (rho_ctx Γ ,,, rho_ctx_over (rho_ctx Γ) (fix_context m)))) m) =
rho_ctx_over (rho_ctx Γ) (fix_context m).
Lemma fix_context_map_fix Γ mfix :
fix_context (map_fix rho (rho_ctx Γ) (rho_ctx_over (rho_ctx Γ) (fix_context mfix)) mfix) =
rho_ctx_over (rho_ctx Γ) (fix_context mfix).
Lemma rho_ctx_over_rev_mapi {Γ m} :
List.rev (mapi (λ (i : nat) (x : def term),
vass (dname x) (lift0 i (rho (rho_ctx Γ) (dtype x)))) m) =
rho_ctx_over (rho_ctx Γ) (fix_context m).
Lemma All2_local_env_pred_fix_ctx P (Γ Γ' : context) (mfix0 : mfixpoint term) (mfix1 : list (def term)) :
All2_local_env
(on_decl
(on_decl_over (λ (Γ0 Γ'0 : context) (t t0 : term), P Γ'0 (rho_ctx Γ0) t0 (rho (rho_ctx Γ0) t)) Γ Γ'))
(fix_context mfix0) (fix_context mfix1)
→ All2_local_env (on_decl (on_decl_over P Γ' (rho_ctx Γ))) (fix_context mfix1)
(fix_context (map_fix rho (rho_ctx Γ) (rho_ctx_over (rho_ctx Γ) (fix_context mfix0)) mfix0)).
Lemma rho_triangle_All_All2_ind_noeq:
∀ (Γ Γ' : context) (brs0 brs1 : list (nat × term)),
pred1_ctx Σ Γ Γ' →
All2 (on_Trel_eq (λ x y : term, (pred1 Σ Γ Γ' x y × pred1 Σ Γ' (rho_ctx Γ) y (rho (rho_ctx Γ) x))%type) snd
fst) brs0 brs1 →
All2 (on_Trel (pred1 Σ Γ' (rho_ctx Γ)) snd) brs1 (map (λ x : nat × term, (fst x, rho (rho_ctx Γ) (snd x))) brs0).
Lemma All2_app_r {A} (P : A → A → Type) l l' r r' : All2 P (l ++ [r]) (l' ++ [r']) →
(All2 P l l') × (P r r').
Lemma All2_map_left {A B} (P : A → A → Type) l l' (f : B → A) :
All2 (fun x y ⇒ P (f x) y) l l' → All2 P (map f l) l'.
Lemma All2_map_right {A B} (P : A → A → Type) l l' (f : B → A) :
All2 P l (map f l') → All2 (fun x y ⇒ P x (f y)) l l'.
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 All2_refl_All {A} (P : A → A → Type) l : All2 P l l → All (fun x ⇒ P x x) l.
Lemma mapi_cst_map {A B} (f : A → B) l : mapi (fun _ ⇒ f) l = map f l.
Lemma All_All2_telescopei_gen (Γ Γ' Δ Δ' : context) (m m' : mfixpoint term) :
#|Δ| = #|Δ'| →
All2
(λ (x y : def term), (pred1 Σ Γ'
(rho_ctx Γ)
(dtype x)
(rho (rho_ctx Γ) (dtype y))) × (dname x = dname y))%type m m' →
All2_local_env_over (pred1 Σ) Γ' (rho_ctx Γ) Δ (rho_ctx_over (rho_ctx Γ) Δ') →
All2_telescope_n (on_decl (pred1 Σ)) (λ n : nat, lift0 n)
(Γ' ,,, Δ) (rho_ctx (Γ ,,, Δ'))
#|Δ|
(map (λ def : def term, vass (dname def) (dtype def)) m)
(map (λ def : def term, vass (dname def) (rho (rho_ctx Γ) (dtype def))) m').
Lemma All_All2_telescopei (Γ Γ' : context) (m m' : mfixpoint term) :
All2 (λ (x y : def term), (pred1 Σ Γ' (rho_ctx Γ) (dtype x) (rho (rho_ctx Γ) (dtype y))) ×
(dname x = dname y))%type m m' →
All2_telescope_n (on_decl (pred1 Σ)) (λ n : nat, lift0 n)
Γ' (rho_ctx Γ)
0
(map (λ def : def term, vass (dname def) (dtype def)) m)
(map (λ def : def term, vass (dname def) (rho (rho_ctx Γ) (dtype def))) m').
Lemma pred1_rho_fix_context_2 (Γ Γ' : context) (m m' : mfixpoint term) :
pred1_ctx Σ Γ' (rho_ctx Γ) →
All2 (on_Trel_eq (pred1 Σ Γ' (rho_ctx Γ)) dtype dname) m
(map_fix rho (rho_ctx Γ)
(fold_fix_context rho (rho_ctx Γ) [] m') m') →
All2_local_env
(on_decl (on_decl_over (pred1 Σ) Γ' (rho_ctx Γ)))
(fix_context m)
(fix_context (map_fix rho (rho_ctx Γ) (fold_fix_context rho (rho_ctx Γ) [] m') m')).
Lemma fold_fix_context_id_rec Γ Δ m :
fold_fix_context (fun _ t ⇒ t) Γ Δ m =
List.rev (mapi_rec (λ (i : nat) (d : def term), vass (dname d) ((lift0 i) (dtype d))) m #|Δ|) ++ Δ.
Lemma fold_fix_context_id Γ m :
fold_fix_context (fun _ t ⇒ t) Γ [] m = fix_context m.
Lemma fold_ctx_over_id Γ Δ : fold_ctx_over (fun _ t ⇒ t) Γ Δ = Δ.
Lemma substitution_pred1 Γ Δ Γ' Δ' s s' N N' :
psubst Σ Γ Γ' s s' Δ Δ' →
pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') N N' →
pred1 Σ Γ Γ' (subst s 0 N) (subst s' 0 N').
Lemma All2_mix {A} {P Q : A → A → Type} {l l'} :
All2 P l l' → All2 Q l l' → All2 (fun x y ⇒ (P x y × Q x y))%type l l'.
Lemma All2_mix_inv {A} {P Q : A → A → Type} {l l'} :
All2 (fun x y ⇒ (P x y × Q x y))%type l l' →
(All2 P l l' × All2 Q l l').
Definition swap {A B : Type} (x : A × B) : B × A :=
(snd x, fst x).
Lemma All2_local_env_sym P Γ Γ' Δ Δ' :
All2_local_env (on_decl (on_decl_over (fun Γ Γ' t t' ⇒ P Γ' Γ t' t) Γ' Γ)) Δ' Δ →
All2_local_env (on_decl (on_decl_over P Γ Γ')) Δ Δ'.
Lemma All2_local_env_over_impl {P Q : context → context → term → term → Type}
{Γ Γ' par par'} :
All2_local_env (on_decl (on_decl_over P Γ Γ')) par par' →
(∀ par par' x y, P (Γ ,,, par) (Γ' ,,, par') x y → Q (Γ ,,, par) (Γ' ,,, par') x y) →
All2_local_env (on_decl (on_decl_over Q Γ Γ')) par par'.
Lemma All2_local_env_over_impl_f_g {P Q : context → context → term → term → Type}
f g {Γ Γ' par par'} :
All2_local_env (on_decl (on_decl_over P Γ (f Γ'))) par par' →
(∀ par par' x y, P (Γ ,,, par) (f Γ' ,,, par') x y →
Q (Γ ,,, par)
(f (Γ' ,,, par')) x (g (Γ' ,,, par') y)) →
All2_local_env (on_decl (on_decl_over (fun Γ Γ' t t' ⇒ Q Γ (f Γ') t (g Γ' t')) Γ Γ')) par par'.
Lemma weakening_pred1_lengths (Γ Δ Γ' Δ' : context)
(M N : term) m n :
m = #|Γ'| → n = #|Δ'| →
All2_local_env_over
(pred1 Σ) Γ Δ Γ' Δ'
→ pred1 Σ Γ Δ M N
→ pred1 Σ
(Γ ,,, Γ')
(Δ ,,, Δ')
((lift0 m) M)
((lift0 n) N).
Lemma wf_rho_fix_subst Γ Γ' mfix0 mfix1 :
#|mfix0| = #|mfix1| →
pred1_ctx Σ Γ' (rho_ctx Γ) →
All2_local_env
(on_decl
(on_decl_over
(λ (Γ Γ' : context) (t t0 : term), pred1 Σ Γ' (rho_ctx Γ) t0 (rho (rho_ctx Γ) t)) Γ
Γ')) (fix_context mfix0) (fix_context mfix1) →
All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
(λ x : def term, (dname x, rarg x))
(λ (Γ Γ' : context) (x y : term), (pred1 Σ Γ Γ' x y ×
pred1 Σ Γ' (rho_ctx Γ) y (rho (rho_ctx Γ) x))%type)
mfix0 mfix1 →
psubst Σ Γ' (rho_ctx Γ) (fix_subst mfix1) (map (rho (rho_ctx Γ)) (fix_subst mfix0))
(fix_context mfix1) (rho_ctx_over (rho_ctx Γ) (fix_context mfix0)).
Lemma wf_rho_cofix_subst Γ Γ' mfix0 mfix1 :
#|mfix0| = #|mfix1| →
pred1_ctx Σ Γ' (rho_ctx Γ) →
All2_local_env
(on_decl
(on_decl_over
(λ (Γ Γ' : context) (t t0 : term), pred1 Σ Γ' (rho_ctx Γ) t0 (rho (rho_ctx Γ) t)) Γ
Γ')) (fix_context mfix0) (fix_context mfix1) →
All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
(λ x : def term, (dname x, rarg x))
(λ (Γ Γ' : context) (x y : term), (pred1 Σ Γ Γ' x y ×
pred1 Σ Γ' (rho_ctx Γ) y (rho (rho_ctx Γ) x))%type)
mfix0 mfix1 →
psubst Σ Γ' (rho_ctx Γ) (cofix_subst mfix1) (map (rho (rho_ctx Γ)) (cofix_subst mfix0))
(fix_context mfix1) (rho_ctx_over (rho_ctx Γ) (fix_context mfix0)).
Lemma rho_cofix_subst Γ mfix :
cofix_subst (map_fix rho (rho_ctx Γ) (rho_ctx_over (rho_ctx Γ) (fix_context mfix)) mfix)
= (map (rho (rho_ctx Γ)) (cofix_subst mfix)).
Lemma rho_fix_subst Γ mfix :
fix_subst (map_fix rho (rho_ctx Γ) (rho_ctx_over (rho_ctx Γ) (fix_context mfix)) mfix)
= (map (rho (rho_ctx Γ)) (fix_subst mfix)).
Lemma ctxmap_cofix_subst:
∀ (Γ' : context) (mfix1 : mfixpoint term),
ctxmap (Γ' ,,, fix_context mfix1) Γ' (cofix_subst mfix1 ⋅n ids).
Lemma ctxmap_fix_subst:
∀ (Γ' : context) (mfix1 : mfixpoint term),
ctxmap (Γ' ,,, fix_context mfix1) Γ' (fix_subst mfix1 ⋅n ids).
Lemma nth_error_cofix_subst mfix n b :
nth_error (cofix_subst mfix) n = Some b →
b = tCoFix mfix (#|mfix| - S n).
Lemma nth_error_fix_subst mfix n b :
nth_error (fix_subst mfix) n = Some b →
b = tFix mfix (#|mfix| - S n).
Lemma pred_subst_rho_cofix (Γ Γ' : context) (mfix0 mfix1 : mfixpoint term) :
pred1_ctx Σ Γ Γ' → pred1_ctx Σ Γ' (rho_ctx Γ)
→ All2_local_env
(on_decl
(on_decl_over
(λ (Γ0 Γ'0 : context) (t t0 : term),
pred1 Σ Γ'0 (rho_ctx Γ0) t0
(rho (rho_ctx Γ0) t)) Γ Γ'))
(fix_context mfix0) (fix_context mfix1)
→ All2 (on_Trel eq (λ x : def term, (dname x, rarg x)))
mfix0 mfix1
→ All2
(on_Trel
(λ x y : term, pred1 Σ Γ Γ' x y
× pred1 Σ Γ'
(rho_ctx Γ) y
(rho (rho_ctx Γ) x)) dtype)
mfix0 mfix1
→ All2
(on_Trel
(λ x y : term, pred1 Σ
(Γ ,,, fix_context mfix0)
(Γ' ,,, fix_context mfix1) x
y
× pred1 Σ
(Γ' ,,, fix_context mfix1)
(rho_ctx
(Γ ,,, fix_context mfix0)) y
(rho
(rho_ctx
(Γ ,,, fix_context mfix0)) x))
dbody) mfix0 mfix1
→ pred1_subst (Γ' ,,, fix_context mfix1) Γ'
(rho_ctx Γ) (cofix_subst mfix1 ⋅n ids)
(cofix_subst
(map_fix rho (rho_ctx Γ)
(rho_ctx_over
(rho_ctx Γ)
(fix_context mfix0)) mfix0) ⋅n ids).
Lemma pred_subst_rho_fix (Γ Γ' : context) (mfix0 mfix1 : mfixpoint term) :
pred1_ctx Σ Γ Γ' → pred1_ctx Σ Γ' (rho_ctx Γ)
→ All2_local_env
(on_decl
(on_decl_over
(λ (Γ0 Γ'0 : context) (t t0 : term),
pred1 Σ Γ'0 (rho_ctx Γ0) t0
(rho (rho_ctx Γ0) t)) Γ Γ'))
(fix_context mfix0) (fix_context mfix1)
→ All2 (on_Trel eq (λ x : def term, (dname x, rarg x)))
mfix0 mfix1
→ All2
(on_Trel
(λ x y : term, pred1 Σ Γ Γ' x y
× pred1 Σ Γ'
(rho_ctx Γ) y
(rho (rho_ctx Γ) x)) dtype)
mfix0 mfix1
→ All2
(on_Trel
(λ x y : term, pred1 Σ
(Γ ,,, fix_context mfix0)
(Γ' ,,, fix_context mfix1) x
y
× pred1 Σ
(Γ' ,,, fix_context mfix1)
(rho_ctx
(Γ ,,, fix_context mfix0)) y
(rho
(rho_ctx
(Γ ,,, fix_context mfix0)) x))
dbody) mfix0 mfix1
→ pred1_subst (Γ' ,,, fix_context mfix1) Γ'
(rho_ctx Γ) (fix_subst mfix1 ⋅n ids)
(fix_subst
(map_fix rho (rho_ctx Γ)
(rho_ctx_over
(rho_ctx Γ)
(fix_context mfix0)) mfix0) ⋅n ids).
Lemma isConstruct_app_pred1 {Γ Δ a b} : pred1 Σ Γ Δ a b → isConstruct_app a → isConstruct_app b.
Lemma isFix_app_inv f args x :
~~ isApp f → isFix_app (tApp (mkApps f args) x) → isFix f.
Lemma pred1_mkApps_tLambda_inv (Γ Δ : context) na ty b args0 c :
pred1 Σ Γ Δ (mkApps (tLambda na ty b) args0) c →
({ ty' & { b' & { args1 &
(c = mkApps (tLambda na ty' b') args1) ×
(pred1 Σ Γ Δ ty ty') ×
(pred1 Σ (Γ ,, vass na ty) (Δ ,, vass na ty') b b') ×
(All2 (pred1 Σ Γ Δ) ) args0 args1 } } }%type) +
({ ty' & { b' & { hd & { tl &
(pred1 Σ Γ Δ ty ty') ×
(pred1 Σ (Γ ,, vass na ty) (Δ ,, vass na ty') b b') ×
(All2 (pred1 Σ Γ Δ) args0 (hd :: tl)) ×
(c = mkApps (b' {0:= hd}) tl) } } } })%type.
Lemma is_constructor_rho Γ n args :
is_constructor n args → is_constructor n (map (rho (rho_ctx Γ)) args).
Lemma mkApps_inj_args_length f f' l l' : #|l| = #|l'| → mkApps f l = mkApps f' l' → f = f' ∧ l = l'.
Lemma pred1_mkApps_Lambda_Fix_inv Γ Γ' f a u l a' l' :
isFix u → isLambda f → #|l| = #|l'| →
pred1 Σ Γ Γ' (mkApps f (a :: l)) (mkApps u (a' :: l')) →
∑ na ty b ty' b' a'',
(f = tLambda na ty b) ×
(tApp u a' = b' {0 := a''}) ×
pred1 Σ Γ Γ' ty ty' ×
pred1 Σ Γ Γ' a a'' ×
pred1 Σ (Γ ,, vass na ty) (Γ' ,, vass na ty') b b' ×
All2 (pred1 Σ Γ Γ') l l'.
Lemma triangle Γ Δ t u :
let Pctx :=
fun (Γ Δ : context) ⇒ pred1_ctx Σ Δ (rho_ctx Γ) in
pred1 Σ Γ Δ t u → pred1 Σ Δ (rho_ctx Γ) u (rho (rho_ctx Γ) t).
End TriangleFn.
Corollary confluence {cf : checker_flags} : ∀ Σ Γ Δ Δ' t u v, wf Σ →
pred1 Σ Γ Δ t u →
pred1 Σ Γ Δ' t v →
pred1 Σ Δ (rho_ctx Σ Γ) u (rho Σ (rho_ctx Σ Γ) t) ×
pred1 Σ Δ' (rho_ctx Σ Γ) v (rho Σ (rho_ctx Σ Γ) t).
End Confluence.
Print Assumptions confluence.