Library Lambda.Russell.GenerationCoerce
Require Import Lambda.Terms.
Require Import Lambda.Reduction.
Require Import Lambda.Conv.
Require Import Lambda.Conv_Dec.
Require Import Lambda.LiftSubst.
Require Import Lambda.Env.
Require Import Lambda.Russell.Types.
Require Import Lambda.Russell.Thinning.
Require Import Lambda.Russell.Substitution.
Require Import Lambda.Russell.Coercion.
Require Import Lambda.Russell.GenerationNotKind.
Implicit Types i k m n p : nat.
Implicit Type s : sort.
Implicit Types A B M N T t u v : term.
Implicit Types e f g : env.
Fixpoint type_range (t : term) : term :=
match t with
| Prod U V ⇒ type_range V
| _ ⇒ t
end.
Lemma subst_to_sort : ∀ t t' s, subst t t' = Srt s → t ≠ Srt s →
t' = Srt s.
Fixpoint is_low t : Prop :=
match t with
| Prod T U ⇒ is_low U
| Srt s ⇒ is_prop s
| _ ⇒ False
end.
Lemma red_sort_eq : ∀ s t, red (Srt s) t → t = Srt s.
Lemma kind_is_prod_aux : ∀ G t T, G |-- t : T →
T = Srt kind → is_low t.
Lemma type_kind_range : ∀ G t, G |-- t : Srt kind → is_low t.
Lemma sort_conv_eq : ∀ G T s, G |-- T : Srt kind → conv T (Srt s) → T = Srt s.
Lemma coerce_sort_l_in_kind : ∀ G A s s', G |-- Srt s >> A : s' → s' = kind.
Lemma coerce_sort_r_in_kind : ∀ G A s s', G |-- A >> Srt s : s' → s' = kind.
Lemma coerce_not_kind_l : ∀ G T s, ¬ G |-- Srt kind >> T : s.
Lemma coerce_not_kind_r : ∀ G T s, ¬ G |-- T >> Srt kind : s.
Lemma coerce_propset_l_aux : ∀ G Ts A s', G |-- Ts >> A : s' →
∀ s, Ts = Srt s → s' = kind → A = Srt s.
Lemma coerce_propset_r_aux : ∀ G Ts A s', G |-- A >> Ts : s' →
∀ s, Ts = Srt s → s' = kind → A = Srt s.
Lemma coerce_propset_l : ∀ G s A s', G |-- Srt s >> A : s' →
A = Srt s.
Lemma coerce_propset_r : ∀ G s A s', G |-- A >> Srt s : s' →
A = Srt s.
Fixpoint no_sort t : Prop :=
match t with
| Prod T U ⇒ no_sort U
| Srt s ⇒ False
| _ ⇒ True
end.
Fixpoint is_low_full t : Prop :=
match t with
| Prod T U ⇒ is_low_full U
| Srt s ⇒ is_prop s
| _ ⇒ False
end.
Lemma sort_of_kinded_aux : ∀ G t T, G |-- t : T →
∀ s, T = Srt s →
(s = kind → is_low_full t) ∧ (is_prop s → no_sort t).
Lemma sorts_of_sorted : ∀ G t s, G |-- t : Srt s →
(s = kind → is_low_full t) ∧ (is_prop s → no_sort t).
Lemma sort_of_kinded : ∀ G t, G |-- t : Srt kind →
is_low_full t.
Lemma sort_of_propset : ∀ G t s, G |-- t : Srt s →
is_prop s → no_sort t.