Skip to content

chore: remove some level annotations #123

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

chore: remove some level annotations #123

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions GroupoidModel/Syntax/Autosubst.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,14 +41,14 @@ def rename (ξ : Nat → Nat) : Expr → Expr
| .pi l l' A B => .pi l l' (A.rename ξ) (B.rename (upr ξ))
| .sigma l l' A B => .sigma l l' (A.rename ξ) (B.rename (upr ξ))
| .lam l l' A t => .lam l l' (A.rename ξ) (t.rename (upr ξ))
| .app l l' B fn arg => .app l l' (B.rename (upr ξ)) (fn.rename ξ) (arg.rename ξ)
| .app l B fn arg => .app l (B.rename (upr ξ)) (fn.rename ξ) (arg.rename ξ)
| .pair l l' B t u => .pair l l' (B.rename (upr ξ)) (t.rename ξ) (u.rename ξ)
| .fst l l' A B p => .fst l l' (A.rename ξ) (B.rename (upr ξ)) (p.rename ξ)
| .snd l l' A B p => .snd l l' (A.rename ξ) (B.rename (upr ξ)) (p.rename ξ)
| .Id l A t u => .Id l (A.rename ξ) (t.rename ξ) (u.rename ξ)
| .refl l t => .refl l (t.rename ξ)
| .idRec l l' t C r u h =>
.idRec l l' (t.rename ξ) (C.rename (upr <| upr ξ)) (r.rename ξ) (u.rename ξ) (h.rename ξ)
| .Id A t u => .Id (A.rename ξ) (t.rename ξ) (u.rename ξ)
| .refl t => .refl (t.rename ξ)
| .idRec l t C r u h =>
.idRec l (t.rename ξ) (C.rename (upr <| upr ξ)) (r.rename ξ) (u.rename ξ) (h.rename ξ)
| .univ l => .univ l
| .el a => .el (a.rename ξ)
| .code A => .code (A.rename ξ)
Expand Down Expand Up @@ -79,14 +79,14 @@ def subst (σ : Nat → Expr) : Expr → Expr
| .pi l l' A B => .pi l l' (A.subst σ) (B.subst (up σ))
| .sigma l l' A B => .sigma l l' (A.subst σ) (B.subst (up σ))
| .lam l l' A t => .lam l l' (A.subst σ) (t.subst (up σ))
| .app l l' B fn arg => .app l l' (B.subst (up σ)) (fn.subst σ) (arg.subst σ)
| .app l B fn arg => .app l (B.subst (up σ)) (fn.subst σ) (arg.subst σ)
| .pair l l' B t u => .pair l l' (B.subst (up σ)) (t.subst σ) (u.subst σ)
| .fst l l' A B p => .fst l l' (A.subst σ) (B.subst (up σ)) (p.subst σ)
| .snd l l' A B p => .snd l l' (A.subst σ) (B.subst (up σ)) (p.subst σ)
| .Id l A t u => .Id l (A.subst σ) (t.subst σ) (u.subst σ)
| .refl l t => .refl l (t.subst σ)
| .idRec l l' t C r u h =>
.idRec l l' (t.subst σ) (C.subst <| up <| up σ) (r.subst σ) (u.subst σ) (h.subst σ)
| .Id A t u => .Id (A.subst σ) (t.subst σ) (u.subst σ)
| .refl t => .refl (t.subst σ)
| .idRec l t C r u h =>
.idRec l (t.subst σ) (C.subst <| up <| up σ) (r.subst σ) (u.subst σ) (h.subst σ)
| .univ l => .univ l
| .el a => .el (a.subst σ)
| .code A => .code (A.subst σ)
Expand Down
8 changes: 4 additions & 4 deletions GroupoidModel/Syntax/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ inductive Expr where
/-- Lambda with the specified argument type. -/
| lam (l l' : Nat) (A b : Expr)
/-- Application at the specified output type family `B`. -/
| app (l l' : Nat) (B fn arg : Expr)
| app (l : Nat) (B fn arg : Expr)
/-- Dependent sum. -/
| sigma (l l' : Nat) (A B : Expr)
/-- Pair formation. -/
Expand All @@ -20,11 +20,11 @@ inductive Expr where
| snd (l l' : Nat) (A B p : Expr)
/-- Identity type. -/
-- TODO: capitalize all the types
| Id (l : Nat) (A t u : Expr)
| Id (A t u : Expr)
/-- A reflexive identity. -/
| refl (l : Nat) (t : Expr)
| refl (t : Expr)
/-- Eliminates an identity. -/
| idRec (l l' : Nat) (t C r u h : Expr)
| idRec (l : Nat) (t C r u h : Expr)
/-- A type universe. -/
| univ (l : Nat)
/-- Type from a code. -/
Expand Down
12 changes: 6 additions & 6 deletions GroupoidModel/Syntax/GCongr.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,21 +55,21 @@ theorem EqTp.cong_Id_tp {Γ A A' t u l} :
Γ ⊢[l] A ≡ A' →
Γ ⊢[l] t : A →
Γ ⊢[l] u : A →
Γ ⊢[l] .Id l A t u ≡ .Id l A' t u :=
Γ ⊢[l] .Id A t u ≡ .Id A' t u :=
fun A t u => .cong_Id A (.refl_tm t) (.refl_tm u)

@[gcongr]
theorem EqTp.cong_Id_left {Γ A t t' u l} :
Γ ⊢[l] t ≡ t' : A →
Γ ⊢[l] u : A →
Γ ⊢[l] .Id l A t u ≡ .Id l A t' u :=
Γ ⊢[l] .Id A t u ≡ .Id A t' u :=
fun h h' => .cong_Id (.refl_tp h.wf_tp) h (.refl_tm h')

@[gcongr]
theorem EqTp.cong_Id_right {Γ A t u u' l} :
Γ ⊢[l] t : A →
Γ ⊢[l] u ≡ u' : A →
Γ ⊢[l] .Id l A t u ≡ .Id l A t u' :=
Γ ⊢[l] .Id A t u ≡ .Id A t u' :=
fun h h' => .cong_Id (.refl_tp h.wf_tp) (.refl_tm h) h'

attribute [gcongr] EqTp.cong_Id
Expand Down Expand Up @@ -98,23 +98,23 @@ theorem EqTm.cong_app_cod {Γ A B B' f a l l'} :
(A, l) :: Γ ⊢[l'] B ≡ B' →
Γ ⊢[max l l'] f : .pi l l' A B →
Γ ⊢[l] a : A →
Γ ⊢[l'] .app l l' B f a ≡ .app l l' B' f a : B.subst a.toSb :=
Γ ⊢[l'] .app l B f a ≡ .app l B' f a : B.subst a.toSb :=
fun hBB' hf ha =>
EqTm.cong_app hBB' (EqTm.refl_tm hf) (EqTm.refl_tm ha)

@[gcongr]
theorem EqTm.cong_app_fn {Γ A B f f' a l l'} :
Γ ⊢[max l l'] f ≡ f' : .pi l l' A B →
Γ ⊢[l] a : A →
Γ ⊢[l'] .app l l' B f a ≡ .app l l' B f' a : B.subst a.toSb :=
Γ ⊢[l'] .app l B f a ≡ .app l B f' a : B.subst a.toSb :=
fun hff' ha =>
EqTm.cong_app (EqTp.refl_tp hff'.wf_tp.inv_pi.2) hff' (EqTm.refl_tm ha)

@[gcongr]
theorem EqTm.cong_app_arg {Γ A B f a a' l l'} :
Γ ⊢[max l l'] f : .pi l l' A B →
Γ ⊢[l] a ≡ a' : A →
Γ ⊢[l'] .app l l' B f a ≡ .app l l' B f a' : B.subst a.toSb :=
Γ ⊢[l'] .app l B f a ≡ .app l B f a' : B.subst a.toSb :=
fun hf haa' =>
EqTm.cong_app (EqTp.refl_tp hf.wf_tp.inv_pi.2) (EqTm.refl_tm hf) haa'

Expand Down
6 changes: 3 additions & 3 deletions GroupoidModel/Syntax/Injectivity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,6 @@ axiom EqTp.inv_sigma {Γ A B A' B' l₀ l₁ l₂ l₁' l₂'} :
(Γ ⊢[l₁] A ≡ A') ∧ ((A, l₁) :: Γ ⊢[l₂] B ≡ B')

/-- Injectivity of Id types. -/
axiom EqTp.inv_Id {Γ A A' t u t' u' l₀ l l'} :
Γ ⊢[l₀] .Id l A t u ≡ .Id l' A' t' u' →
l₀ = l ∧ l₀ = l' ∧ (Γ ⊢[l₀] A ≡ A') ∧ (Γ ⊢[l₀] t ≡ t' : A) ∧ (Γ ⊢[l₀] u ≡ u' : A)
axiom EqTp.inv_Id {Γ A A' t u t' u' l} :
Γ ⊢[l] .Id A t u ≡ .Id A' t' u' →
(Γ ⊢[l] A ≡ A') ∧ (Γ ⊢[l] t ≡ t' : A) ∧ (Γ ⊢[l] u ≡ u' : A)
41 changes: 19 additions & 22 deletions GroupoidModel/Syntax/Interpretation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,7 @@ def ofType (Γ : s.CObj) (l : Nat) :
let A ← ofType Γ i A
let B ← ofType (Γ.snoc ilen A) j B
return lij ▸ s.mkSigma ilen jlen A B
| .Id _ A a0 a1, llen => do
| .Id A a0 a1, llen => do
let A ← ofType Γ l A
let a0 ← ofTerm Γ l a0
let a1 ← ofTerm Γ l a1
Expand All @@ -318,15 +318,14 @@ def ofTerm (Γ : s.CObj) (l : Nat) :
let A ← ofType Γ i A
let e ← ofTerm (Γ.snoc ilen A) j e
return lij ▸ s.mkLam ilen jlen A e
| .app i j B f a, _ => do
Part.assert (l = j) fun lj => do
| .app i B f a, llen => do
Part.assert (i < s.length + 1) fun ilen => do
have jlen : j < s.length + 1 := by omega
let f ← ofTerm Γ (max i j) f
have jlen : l < s.length + 1 := by omega
let f ← ofTerm Γ (max i l) f
let a ← ofTerm Γ i a
let B ← ofType (Γ.snoc ilen (a ≫ s[i].tp)) j B
Part.assert (f ≫ s[max i j].tp = s.mkPi ilen jlen (a ≫ s[i].tp) B) fun h =>
return lj ▸ s.mkApp ilen jlen _ B f h a rfl
let B ← ofType (Γ.snoc ilen (a ≫ s[i].tp)) l B
Part.assert (f ≫ s[max i l].tp = s.mkPi ilen llen (a ≫ s[i].tp) B) fun h =>
return s.mkApp ilen llen _ B f h a rfl
| .pair i j B t u, _ => do
Part.assert (l = max i j) fun lij => do
have ilen : i < s.length + 1 := by omega
Expand Down Expand Up @@ -394,8 +393,8 @@ theorem mem_ofType_sigma {Γ l i j A B} {llen : l < s.length + 1} {x} :
dsimp only [ofType]; simp_part; exact exists_congr fun _ => by subst l; simp_part

@[simp]
theorem mem_ofType_Id {Γ l i A a b} {llen : l < s.length + 1} {x} :
x ∈ s.ofType Γ l (.Id i A a b) llen ↔
theorem mem_ofType_Id {Γ l A a b} {llen : l < s.length + 1} {x} :
x ∈ s.ofType Γ l (.Id A a b) llen ↔
∃ (A' : y(Γ.fst) ⟶ s[l].Ty), A' ∈ s.ofType Γ l A ∧
∃ (a' : y(Γ.fst) ⟶ s[l].Tm), a' ∈ s.ofTerm Γ l a ∧
∃ (b' : y(Γ.fst) ⟶ s[l].Tm), b' ∈ s.ofTerm Γ l b ∧
Expand Down Expand Up @@ -443,17 +442,16 @@ theorem mem_ofTerm_lam {Γ l i j A e} {llen : l < s.length + 1} {x} :
dsimp only [ofTerm]; simp_part; exact exists_congr fun _ => by subst l; simp_part

@[simp]
theorem mem_ofTerm_app {Γ l i j B f a} {llen : l < s.length + 1} {x} :
x ∈ s.ofTerm Γ l (.app i j B f a) llen ↔
∃ lj : l = j,
theorem mem_ofTerm_app {Γ l i B f a} {llen : l < s.length + 1} {x} :
x ∈ s.ofTerm Γ l (.app i B f a) llen ↔
∃ ilen : i < s.length + 1,
have jlen : j < s.length + 1 := by omega
∃ f' : y(Γ.1) ⟶ s[max i j].Tm, f' ∈ ofTerm Γ (max i j) f ∧
have llen : l < s.length + 1 := by omega
∃ f' : y(Γ.1) ⟶ s[max i l].Tm, f' ∈ ofTerm Γ (max i l) f ∧
∃ a' : y(Γ.1) ⟶ s[i].Tm, a' ∈ ofTerm Γ i a ∧
∃ B' : y((Γ.snoc ilen (a' ≫ s[i].tp)).1) ⟶ s[j].Ty,
B' ∈ ofType (Γ.snoc ilen (a' ≫ s[i].tp)) j B ∧
∃ h, x = lj ▸ s.mkApp ilen jlen _ B' f' h a' rfl := by
dsimp only [ofTerm]; simp_part; exact exists_congr fun _ => by subst l; simp_part
∃ B' : y((Γ.snoc ilen (a' ≫ s[i].tp)).1) ⟶ s[l].Ty,
B' ∈ ofType (Γ.snoc ilen (a' ≫ s[i].tp)) l B ∧
∃ h, x = s.mkApp ilen llen _ B' f' h a' rfl := by
dsimp only [ofTerm]; simp_part

@[simp]
theorem mem_ofTerm_pair {Γ l i j B t u} {llen : l < s.length + 1} {x} :
Expand Down Expand Up @@ -667,9 +665,8 @@ theorem mem_ofType_ofTerm_subst' {full}
refine ⟨_, (ihA llen.1 σ).1 hA, _, ?_, rfl⟩
rw [← CSb.up_toSb]; exact (ihB llen.2 (σ.up llen.1 A)).2 hB
case app ihB ihf iha =>
obtain ⟨rfl, llen', H⟩ := mem_ofTerm_app.1 H; simp at H llen
obtain ⟨f, hf, a, ha, B, hB, eq, rfl⟩ := H; clear H
simp only [Expr.subst, comp_mkApp, mem_ofTerm_app, exists_true_left]
obtain ⟨llen', f, hf, a, ha, B, hB, eq, rfl⟩ := mem_ofTerm_app.1 H
simp only [Expr.subst, comp_mkApp, mem_ofTerm_app]
refine ⟨‹_›, _, (ihf (by simp [*]) σ).2 hf, _, (iha llen' σ).2 ha, _, ?_, ?_, rfl⟩
· rw [← CSb.up'_toSb]; exact (ihB llen (σ.up' llen' _ (Category.assoc ..).symm)).1 hB
· simp [*, comp_mkPi]
Expand Down
88 changes: 43 additions & 45 deletions GroupoidModel/Syntax/Inversion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -292,11 +292,11 @@ theorem WfTp.inv_sigma {Γ A B l₀ l l'} : Γ ⊢[l₀] .sigma l l' A B →
fun h => this h rfl
mutual_induction WfCtx <;> grind

theorem WfTp.inv_Id {Γ A t u l₀ l} : Γ ⊢[l₀] .Id l A t u →
l₀ = l ∧ (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) := by
theorem WfTp.inv_Id {Γ A t u l} : Γ ⊢[l] .Id A t u →
(Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) := by
suffices
∀ {Γ l₀ T}, Γ ⊢[l₀] T → ∀ {l t u}, T = .Id l A t u →
l₀ = l ∧ (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) from
∀ {Γ l T}, Γ ⊢[l] T → ∀ {t u}, T = .Id A t u →
(Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) from
fun h => this h rfl
mutual_induction WfCtx <;> grind

Expand All @@ -323,7 +323,7 @@ theorem WfTp.sigma {Γ A B l l'} :
theorem WfTp.Id {Γ A t u l} :
Γ ⊢[l] t : A →
Γ ⊢[l] u : A →
Γ ⊢[l] .Id l A t u :=
Γ ⊢[l] .Id A t u :=
fun t u => WfTp.Id' t.wf_tp t u

theorem EqTp.cong_pi {Γ A A' B B' l l'} :
Expand All @@ -346,7 +346,7 @@ theorem WfTm.lam {Γ A B t l l'} :
theorem WfTm.app {Γ A B f a l l'} :
Γ ⊢[max l l'] f : .pi l l' A B →
Γ ⊢[l] a : A →
Γ ⊢[l'] .app l l' B f a : B.subst a.toSb :=
Γ ⊢[l'] .app l B f a : B.subst a.toSb :=
fun hf ha =>
have ⟨_, hB⟩ := hf.wf_tp.inv_pi
WfTm.app' hB.wf_binder hB hf ha
Expand Down Expand Up @@ -374,16 +374,16 @@ theorem WfTm.snd {Γ A B p l l'} :

theorem WfTm.refl {Γ A t l} :
Γ ⊢[l] t : A →
Γ ⊢[l] .refl l t : .Id l A t t :=
Γ ⊢[l] .refl t : .Id A t t :=
fun t => .refl' t.wf_tp t

theorem WfTm.idRec {Γ A M t r u h l l'} :
(.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
Γ ⊢[l] h : .Id l A t u →
Γ ⊢[l'] .idRec l l' t M r u h : M.subst (.snoc u.toSb h) :=
(.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
Γ ⊢[l] h : .Id A t u →
Γ ⊢[l'] .idRec l t M r u h : M.subst (.snoc u.toSb h) :=
fun M r h =>
have ⟨_, t, u⟩ := h.wf_tp.inv_Id
have ⟨t, u⟩ := h.wf_tp.inv_Id
.idRec' t.wf_tp t M r u h

theorem EqTm.cong_lam {Γ A A' B t t' l l'} :
Expand All @@ -396,7 +396,7 @@ theorem EqTm.cong_app {Γ A B B' f f' a a' l l'} :
(A, l) :: Γ ⊢[l'] B ≡ B' →
Γ ⊢[max l l'] f ≡ f' : .pi l l' A B →
Γ ⊢[l] a ≡ a' : A →
Γ ⊢[l'] .app l l' B f a ≡ .app l l' B' f' a' : B.subst a.toSb :=
Γ ⊢[l'] .app l B f a ≡ .app l B' f' a' : B.subst a.toSb :=
fun hBB' hff' haa' => EqTm.cong_app' haa'.wf_tp hBB' hff' haa'

theorem EqTm.cong_pair {Γ A B B' t t' u u' l l'} :
Expand All @@ -422,17 +422,17 @@ theorem EqTm.cong_snd {Γ A A' B B' p p' l l'} :

theorem EqTm.cong_idRec {Γ A M M' t t' r r' u u' h h' l l'} :
Γ ⊢[l] t ≡ t' : A →
(.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl l t) →
(.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl t) →
Γ ⊢[l] u ≡ u' : A →
Γ ⊢[l] h ≡ h' : .Id l A t u →
Γ ⊢[l'] .idRec l l' t M r u h ≡ .idRec l l' t' M' r' u' h' : M.subst (.snoc u.toSb h) :=
Γ ⊢[l] h ≡ h' : .Id A t u →
Γ ⊢[l'] .idRec l t M r u h ≡ .idRec l t' M' r' u' h' : M.subst (.snoc u.toSb h) :=
fun teq Meq req ueq heq => .cong_idRec' teq.wf_tp teq.wf_left teq Meq req ueq heq

theorem EqTm.app_lam {Γ A B t u l l'} :
(A, l) :: Γ ⊢[l'] t : B →
Γ ⊢[l] u : A →
Γ ⊢[l'] .app l l' B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb :=
Γ ⊢[l'] .app l B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb :=
fun ht hu => EqTm.app_lam' hu.wf_tp ht.wf_tp ht hu

theorem EqTm.fst_pair {Γ A B t u l l'} :
Expand All @@ -451,20 +451,20 @@ theorem EqTm.snd_pair {Γ A B t u l l'} :

theorem EqTm.cong_refl {Γ A t t' l} :
Γ ⊢[l] t ≡ t' : A →
Γ ⊢[l] .refl l t ≡ .refl l t' : .Id l A t t :=
Γ ⊢[l] .refl t ≡ .refl t' : .Id A t t :=
fun t => .cong_refl' t.wf_tp t

theorem EqTm.idRec_refl {Γ A M t r l l'} :
Γ ⊢[l] t : A →
(.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
Γ ⊢[l'] .idRec l l' t M r t (.refl l t) ≡ r : M.subst (.snoc t.toSb <| .refl l t) :=
(.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
Γ ⊢[l'] .idRec l t M r t (.refl t) ≡ r : M.subst (.snoc t.toSb <| .refl t) :=
fun t M r => .idRec_refl' t.wf_tp t M r

theorem EqTm.lam_app {Γ A B f l l'} :
Γ ⊢[max l l'] f : .pi l l' A B →
Γ ⊢[max l l'] f ≡
.lam l l' A (.app l l' (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
.lam l l' A (.app l (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
.pi l l' A B :=
fun hf =>
have ⟨_, hB⟩ := hf.wf_tp.inv_pi
Expand All @@ -489,7 +489,7 @@ theorem EqTm.trans_tm {Γ A t t' t'' l} :
fun htt' ht't'' => EqTm.trans_tm' htt'.wf_tp htt' ht't''

theorem WfTp.Id_bvar {Γ A t l} : Γ ⊢[l] t : A →
(A, l) :: Γ ⊢[l] .Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
(A, l) :: Γ ⊢[l] .Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
fun t => WfTp.Id (t.subst (WfSb.wk t.wf_tp)) (.bvar (t.wf_ctx.snoc t.wf_tp) (.zero ..))

/-! ## Term former inversion -/
Expand All @@ -513,13 +513,11 @@ theorem WfTm.inv_lam {Γ A C b l₀ l l'} : Γ ⊢[l₀] .lam l l' A b : C →
mutual_induction WfCtx <;>
try grind [WfTp.pi, WfTm.wf_tp, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]

theorem WfTm.inv_app {Γ B C f a l₀ l l'} : Γ ⊢[l₀] .app l l' B f a : C →
l₀ = l' ∧ ∃ A,
(Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
theorem WfTm.inv_app {Γ B C f a l l'} : Γ ⊢[l'] .app l B f a : C →
∃ A, (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
suffices
∀ {Γ l₀ C t}, Γ ⊢[l₀] t : C → ∀ {B f a l l'}, t = .app l l' B f a →
l₀ = l' ∧ ∃ A,
(Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
∀ {Γ l' C t}, Γ ⊢[l'] t : C → ∀ {B f a l}, t = .app l B f a →
∃ A, (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
fun h => this h rfl
mutual_induction WfCtx <;>
grind [InvProof.tp_inst, WfTp.wf_ctx, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]
Expand Down Expand Up @@ -557,36 +555,36 @@ theorem WfTm.inv_snd {Γ A B C p l₀ l l'} : Γ ⊢[l₀] .snd l l' A B p : C
mutual_induction WfCtx <;>
grind [InvProof.tp_inst, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp, WfTm.fst, WfTp.wf_ctx]

theorem WfTm.inv_refl {Γ C t l₀ l} : Γ ⊢[l₀] .refl l t : C →
l₀ = l ∧ ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id l A t t) := by
theorem WfTm.inv_refl {Γ C t l} : Γ ⊢[l] .refl t : C →
∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id A t t) := by
suffices
∀ {Γ l₀ C t'}, Γ ⊢[l₀] t' : C → ∀ {l t}, t' = .refl l t →
l₀ = l ∧ ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id l A t t) from
∀ {Γ l C t'}, Γ ⊢[l] t' : C → ∀ {t}, t' = .refl t →
∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id A t t) from
fun h => this h rfl
mutual_induction WfCtx <;> grind [WfTp.Id, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]

theorem WfTm.inv_idRec {Γ M C t r u h l₀ l l'} : Γ ⊢[l₀] .idRec l l' t M r u h : C →
l₀ = l' ∧ ∃ A,
theorem WfTm.inv_idRec {Γ M C t r u h l l'} : Γ ⊢[l'] .idRec l t M r u h : C →
∃ A,
(Γ ⊢[l] t : A) ∧
((.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
(Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t)) ∧
((.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
(Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t)) ∧
(Γ ⊢[l] u : A) ∧
(Γ ⊢[l] h : .Id l A t u) ∧
(Γ ⊢[l] h : .Id A t u) ∧
(Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) := by
suffices ∀ {Γ l₀ C t'}, Γ ⊢[l₀] t' : C → ∀ {t M r u h l l'}, t' = .idRec l l' t M r u h →
l₀ = l' ∧ ∃ A,
suffices ∀ {Γ l' C t'}, Γ ⊢[l'] t' : C → ∀ {t M r u h l}, t' = .idRec l t M r u h →
∃ A,
(Γ ⊢[l] t : A) ∧
((.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
(Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t)) ∧
((.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
(Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t)) ∧
(Γ ⊢[l] u : A) ∧
(Γ ⊢[l] h : .Id l A t u) ∧
(Γ ⊢[l] h : .Id A t u) ∧
(Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) from
fun h => this h rfl
mutual_induction WfCtx
all_goals intros; try exact True.intro
all_goals rename_i eq; cases eq
case refl t M r u h _ _ _ _ _ _ =>
refine ⟨rfl, _, t, M, r, u, h, ?_⟩
refine ⟨_, t, M, r, u, h, ?_⟩
apply EqTp.refl_tp <| M.subst (WfSb.snoc (WfSb.toSb u) _ _)
. grind [WfTp.Id_bvar, WfTp.wf_ctx]
. autosubst; assumption
Expand Down
Loading