From c14ac2af2164ebf4cf10887a48e33144a79b8a59 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Tue, 4 Mar 2025 17:13:35 +0000 Subject: [PATCH 01/11] Started designing optimized language: defined preCon, preTy, preTm; defined wf predicates; defined Ty-formers and de Bruijn operators --- GeneralizedAlgebra/signature.lean | 146 ++++++++++++++++++------------ 1 file changed, 88 insertions(+), 58 deletions(-) diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index c88217b..1d881e1 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -1,76 +1,106 @@ import GeneralizedAlgebra.helper - open Nat mutual - inductive Con : Type where - | EMPTY : Con - | EXTEND : Con → Ty → Con - - inductive Subst : Type where - | EPSILON : Con → Subst - | ID : Con → Subst - | COMP : Subst → Subst → Subst - | PAIR : Subst → Tm → Subst - | PROJ1 : Subst → Subst - - inductive Ty : Type where - | SUBST_Ty : Subst → Ty → Ty - | UU : Ty - | EL : Tm → Ty - | PI : Tm → Ty → Ty - | EQ : Tm → Tm → Ty - - inductive Tm : Type where - | SUBST_Tm : Subst → Tm → Tm - | PROJ2 : Subst → Tm - | APP : Tm → Tm + inductive preTm : Type where + | preVAR : Nat → preTm + | preAPP : preTm → preTm → preTm + | preTRANSP : preTy → preTm → preTm → preTm + + inductive preTy : Type where + | preUU : preTy + | preEL : preTm → preTy + | prePI : preTm → preTy → preTy + | preEQ : preTm → preTm → preTm → preTy end +open preTm preTy -open Con Subst Ty Tm - +-- Written backwards! +def preCon : Type := List preTy -infixl:10 " ▷ " => EXTEND -notation t " [ " σ " ]t " => SUBST_Tm σ t +mutual + def preWkArrTy : preTy → Nat → preTy + | preUU, _ => preUU + | preEL X, a => preEL (preWkArrTm X a) + | prePI X Y, a => prePI (preWkArrTm X a) (preWkArrTy Y (succ a)) + | preEQ A t t', a => preEQ (preWkArrTm A a) (preWkArrTm t a) (preWkArrTm t' a) + def preWkArrTm : preTm → Nat → preTm + | preVAR n, a => if n ≥ a then preVAR (succ n) else preVAR n + | preAPP f t, a => preAPP (preWkArrTm f a) (preWkArrTm t a) + | preTRANSP A eq t, a => preTRANSP (preWkArrTy A a) (preWkArrTm eq a) (preWkArrTm t a) +end -def len : Con → Nat -| EMPTY => 0 -| Γ ▷ _ => succ (len Γ) +def preWkTy (A : preTy) : preTy := preWkArrTy A 0 +def preWkTm (t : preTm) : preTm := preWkArrTm t 0 -def deBruijn : Tm → Option Nat -| PROJ2 (ID _) => some 0 -| t [ PROJ1 (ID _) ]t => do let res ← deBruijn t; return (succ res) -| _ => none +mutual + def preSubstTy : preTy → preTm → preTy + | preUU, _ => preUU + | preEL X, z => preEL (preSubstTm X z) + | prePI X Y, z => prePI (preSubstTm X z) (preSubstTy Y z) + | preEQ A t t', z => preEQ (preSubstTm A z) (preSubstTm t z) (preSubstTm t' z) + def preSubstTm : preTm → preTm → preTm + | preVAR 0, z => z + | preVAR (succ n), _ => preVAR n + | preAPP f t, z => preAPP (preSubstTm f z) (preSubstTm t z) + | preTRANSP A eq t, z => preTRANSP (preSubstTy A z) (preSubstTm eq z) (preSubstTm t z) -- ? +end -def wk (Γ : Con) (A : Ty) : Subst := PROJ1 (@ID (Γ ▷ A)) -def V0 (Γ : Con) (T0 : Ty) : Tm := PROJ2 (@ID (Γ ▷ T0)) +mutual + inductive wfCon : preCon → Prop where + | wfNil : wfCon [] + | wfCons : {Γ : preCon} → {A : preTy} → wfTy Γ A → (_ : wfCon Γ) → wfCon (A::Γ) + + inductive wfTy : preCon → preTy → Prop + | wfWkTy : {Γ : preCon} → {A B : preTy} → wfTy Γ A → wfTy (B::Γ) (preWkTy A) + | wfUU : {Γ : preCon} → wfTy Γ preUU + | wfEL : {Γ : preCon} → {X : preTm} → wfTm Γ preUU X → wfTy Γ (preEL X) + | wfPI : {Γ : preCon} → {X : preTm} → {Y : preTy} → + wfTm Γ preUU X → wfTy (preEL X::Γ) Y → wfTy Γ (prePI X Y) + | wfEQ : {Γ : preCon} → {X t t' : preTm} → + wfTm Γ preUU X → wfTm Γ (preEL X) t → wfTm Γ (preEL X) t' → wfTy Γ (preEQ X t t') + | wfSubstTy : {Γ : preCon} → {A B : preTy} → {t : preTm} → + wfTy Γ B → wfTy (B::Γ) A → wfTm Γ B t → wfTy Γ (preSubstTy A t) + + inductive wfTm : preCon → preTy → preTm → Prop + | wfVAR0 : {Γ : preCon} → {A : preTy} → + wfTy Γ A → wfTm (A::Γ) (preWkTy A) (preVAR 0) + | wfWkTm : {Γ : preCon} → {A B : preTy} → {t : preTm} → + wfTm Γ A t → wfTy Γ B → wfTm (B::Γ) (preWkTy A) (preWkTm t) + | wfAPP : {Γ : preCon} → {X : preTm} → {Y : preTy} → {f t : preTm} → + wfTy Γ (prePI X Y) → wfTm Γ (prePI X Y) f → wfTm Γ (preEL X) t → wfTm Γ (preSubstTy Y t) (preAPP f t) + | wfTRANSP : {Γ : preCon} → {X eq t t' z: preTm} → {Y : preTy} → + {_ : wfTm Γ preUU X} → {_ : wfTy (preEL X::Γ) Y} → + {_ : wfTm Γ (preEL X) t} → {_ : wfTm Γ (preEL X) t'} → + wfTm Γ (preEQ X t t') eq → + wfTm Γ (preSubstTy Y t) z → + wfTm Γ (preSubstTy Y t') (preTRANSP Y eq z) + | wfSubstTm : {Γ : preCon} → {A B : preTy} → {t t': preTm} → + wfTm Γ B t → wfTm (B::Γ) A t' → wfTm Γ (preSubstTy A t) (preSubstTm t' t) +end --- namespace GAT +open wfCon wfTy wfTm -inductive Arg : Type where -| Impl : String → Ty → Arg -| Expl : String → Ty → Arg -| Anon : Ty → Arg -open Arg +def Con : Type := { Γ : preCon // wfCon Γ } +def Ty (Γ : Con) : Type := { A : preTy // wfTy Γ.1 A} +def Tm (Γ : Con) (A : Ty Γ) : Type := { t : preTm // wfTm Γ.1 A.1 t} -def getName : Arg → Option String -| Impl i _ => some i -| Expl i _ => some i -| Anon _ => none +def EMPTY : Con := ⟨[], wfNil⟩ +def EXTEND (Γ : Con) (A : Ty Γ) : Con := ⟨ A.1 :: Γ.1 , wfCons A.2 Γ.2 ⟩ -structure GAT where - (con : Con) - (topnames : List String) - (telescopes : List (List Arg × Ty)) +def UU {Γ : Con} : Ty Γ := ⟨ preUU , wfUU ⟩ +def EL {Γ : Con} (X : Tm Γ UU) : Ty Γ := ⟨ preEL X.1 , wfEL X.2 ⟩ +def PI {Γ : Con} (X : Tm Γ UU) (Y : Ty (EXTEND Γ (EL X))) : Ty Γ := + ⟨ prePI X.1 Y.1 , wfPI X.2 Y.2 ⟩ +def EQ {Γ : Con} (X : Tm Γ UU) (t t' : Tm Γ (EL X)) : Ty Γ := + ⟨ preEQ X.1 t.1 t'.1 , wfEQ X.2 t.2 t'.2 ⟩ --- #check Listappend -def GAT.subnames (𝔊 : GAT) : List String := - List.join $ - List.map (λ (L,s) => L ++ [s]) $ - List.zip - (List.map ((mappartial getName) ∘ Prod.fst) (GAT.telescopes 𝔊)) - (GAT.topnames 𝔊) +def wkTy {Γ : Con}{B : Ty Γ}(A : Ty Γ) : Ty (EXTEND Γ B) := + ⟨ preWkTy A.1 , wfWkTy A.2 ⟩ --- end GAT +def ZERO {Γ : Con}{A : Ty Γ} : Tm (EXTEND Γ A) (wkTy A) := + ⟨ preVAR 0, wfVAR0 A.2 ⟩ +def SUCC {Γ : Con}{B : Ty Γ}{A : Ty Γ} (t : Tm Γ A) : Tm (EXTEND Γ B) (wkTy A):= + ⟨ preWkTm t.1 , wfWkTm t.2 B.2 ⟩ From 5d98ee2093d19f727d13492611fc54a13ac25d14 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Sat, 8 Mar 2025 17:14:01 +0000 Subject: [PATCH 02/11] Attempted to get revised signature to work by making everything explicit --- GeneralizedAlgebra/signature.lean | 57 +++++++++++++++++++++++++++---- 1 file changed, 50 insertions(+), 7 deletions(-) diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 1d881e1..b4ac55d 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -70,7 +70,7 @@ mutual | wfWkTm : {Γ : preCon} → {A B : preTy} → {t : preTm} → wfTm Γ A t → wfTy Γ B → wfTm (B::Γ) (preWkTy A) (preWkTm t) | wfAPP : {Γ : preCon} → {X : preTm} → {Y : preTy} → {f t : preTm} → - wfTy Γ (prePI X Y) → wfTm Γ (prePI X Y) f → wfTm Γ (preEL X) t → wfTm Γ (preSubstTy Y t) (preAPP f t) + wfTm Γ (prePI X Y) f → wfTm Γ (preEL X) t → wfTm Γ (preSubstTy Y t) (preAPP f t) | wfTRANSP : {Γ : preCon} → {X eq t t' z: preTm} → {Y : preTy} → {_ : wfTm Γ preUU X} → {_ : wfTy (preEL X::Γ) Y} → {_ : wfTm Γ (preEL X) t} → {_ : wfTm Γ (preEL X) t'} → @@ -91,16 +91,59 @@ def EMPTY : Con := ⟨[], wfNil⟩ def EXTEND (Γ : Con) (A : Ty Γ) : Con := ⟨ A.1 :: Γ.1 , wfCons A.2 Γ.2 ⟩ def UU {Γ : Con} : Ty Γ := ⟨ preUU , wfUU ⟩ -def EL {Γ : Con} (X : Tm Γ UU) : Ty Γ := ⟨ preEL X.1 , wfEL X.2 ⟩ -def PI {Γ : Con} (X : Tm Γ UU) (Y : Ty (EXTEND Γ (EL X))) : Ty Γ := +def EL (Γ : Con) (X : Tm Γ UU) : Ty Γ := ⟨ preEL X.1 , wfEL X.2 ⟩ +def PI (Γ : Con) (X : Tm Γ UU) (Y : Ty (EXTEND Γ (EL Γ X))) : Ty Γ := ⟨ prePI X.1 Y.1 , wfPI X.2 Y.2 ⟩ -def EQ {Γ : Con} (X : Tm Γ UU) (t t' : Tm Γ (EL X)) : Ty Γ := +def EQ (Γ : Con) (X : Tm Γ UU) (t t' : Tm Γ (EL Γ X)) : Ty Γ := ⟨ preEQ X.1 t.1 t'.1 , wfEQ X.2 t.2 t'.2 ⟩ -def wkTy {Γ : Con}{B : Ty Γ}(A : Ty Γ) : Ty (EXTEND Γ B) := +def wkTy (Γ : Con)(B : Ty Γ)(A : Ty Γ) : Ty (EXTEND Γ B) := ⟨ preWkTy A.1 , wfWkTy A.2 ⟩ +def substTy (Γ : Con)(B : Ty Γ)(A : Ty (EXTEND Γ B))(t : Tm Γ B) : Ty Γ := + ⟨ preSubstTy A.1 t.1, wfSubstTy B.2 A.2 t.2 ⟩ +def APP (Γ : Con)(X : Tm Γ UU)(Y : Ty (EXTEND Γ (EL Γ X)))(f : Tm Γ (PI Γ X Y))(t : Tm Γ (EL Γ X)) : Tm Γ (substTy Γ (EL Γ X) Y t) := + ⟨ preAPP f.1 t.1, wfAPP f.2 t.2 ⟩ -def ZERO {Γ : Con}{A : Ty Γ} : Tm (EXTEND Γ A) (wkTy A) := +def ZERO (Γ : Con)(A : Ty Γ) : Tm (EXTEND Γ A) (wkTy Γ A A) := ⟨ preVAR 0, wfVAR0 A.2 ⟩ -def SUCC {Γ : Con}{B : Ty Γ}{A : Ty Γ} (t : Tm Γ A) : Tm (EXTEND Γ B) (wkTy A):= +def SUCC (Γ : Con)(B : Ty Γ)(A : Ty Γ) (t : Tm Γ A) : Tm (EXTEND Γ B) (wkTy Γ B A):= ⟨ preWkTm t.1 , wfWkTm t.2 B.2 ⟩ + +def len : Con → Nat := λ Γ => List.length Γ.1 + +-- #eval len $ EXTEND (EXTEND (EXTEND (EXTEND EMPTY UU) (PI ZERO (PI (SUCC ZERO) (EL $ SUCC $ SUCC $ ZERO)))) (EL $ SUCC $ ZERO)) (PI (SUCC $ SUCC $ ZERO) (EQ (SUCC $ SUCC $ SUCC $ ZERO) ZERO ZERO)) + + +infixl:10 " ▷ " => EXTEND +notation "⋄" => EMPTY + +-- def ONE := SUCC ZERO +def UUnil := @UU ⋄ +def P := ⋄ ▷ UUnil +def Q := P ▷ EL P (ZERO ⋄ UUnil) +def P' := P ▷ PI P (ZERO ⋄ UUnil) (PI Q (SUCC P _ _ (ZERO ⋄ UUnil)) UU) +def Q' := P' ▷ EL _ (SUCC _ _ _ (ZERO _ _)) +def Q'' := Q' ▷ EL _ (SUCC _ _ _ (SUCC _ _ _ (ZERO _ _))) +def P'' := P' ▷ PI _ (SUCC _ _ _ (ZERO _ _)) + (EL _ (APP Q' (SUCC P' _ _ (SUCC P _ _ (ZERO ⋄ _))) UU + (APP Q' (SUCC _ _ _ (SUCC _ _ _ (ZERO _ _))) _ + _ + (ZERO _ _)) + (ZERO _ _) + ) + ) + -- + +-- def x := @APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO) +-- def Q := P'' ▷ PI (SUCC ZERO) (@EL P''' (@APP P''' _ _ _ _)) +-- #reduce P''' + +-- #eval len $ +-- ⋄ ▷ UU ▷ PI ZERO UU + -- ▷ PI (SUCC ZERO) (EL (@APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO))) + --▷ (PI (SUCC ZERO) (EL (APP (SUCC ZERO) _ ))) + -- ▷ (PI ZERO (PI (SUCC ZERO) (EL $ SUCC $ SUCC $ ZERO))) + -- ▷ (PI (SUCC ZERO) (EQ (SUCC $ SUCC ZERO) (APP (SUCC $ ZERO) (APP _ _)) ZERO)) + -- ▷ (EL $ SUCC $ ZERO) + -- ▷ (PI (SUCC $ SUCC $ ZERO) (EQ (SUCC $ SUCC $ SUCC $ ZERO) ZERO (APP (APP (_) ZERO) (SUCC ZERO)))) +-- notation t " [ " σ " ]t " => SUBST_Tm σ t From ca13d1581fb294809c92264edca5d49a019cfe47 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Wed, 12 Mar 2025 00:07:09 +0000 Subject: [PATCH 03/11] Removed wf defns; started defining elim --- GeneralizedAlgebra/AlgPrinting.lean | 4 +- GeneralizedAlgebra/signature.lean | 230 ++++++++++++++-------------- 2 files changed, 115 insertions(+), 119 deletions(-) diff --git a/GeneralizedAlgebra/AlgPrinting.lean b/GeneralizedAlgebra/AlgPrinting.lean index ace8a8b..4f2aead 100644 --- a/GeneralizedAlgebra/AlgPrinting.lean +++ b/GeneralizedAlgebra/AlgPrinting.lean @@ -1,8 +1,8 @@ import GeneralizedAlgebra.signature open Nat -open Con Subst Ty Tm -open GAT +open Ty Tm +-- open GAT mutual diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index b4ac55d..0e9614d 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -3,142 +3,138 @@ import GeneralizedAlgebra.helper open Nat mutual - inductive preTm : Type where - | preVAR : Nat → preTm - | preAPP : preTm → preTm → preTm - | preTRANSP : preTy → preTm → preTm → preTm - - inductive preTy : Type where - | preUU : preTy - | preEL : preTm → preTy - | prePI : preTm → preTy → preTy - | preEQ : preTm → preTm → preTm → preTy + inductive Tm : Type where + | VAR : Nat → Tm + | APP : Tm → Tm → Tm + | TRANSP : Tm → Tm → Tm → Ty → Tm → Tm → Tm + + inductive Ty : Type where + | UU : Ty + | EL : Tm → Ty + | PI : Tm → Ty → Ty + | EQ : Tm → Tm → Tm → Ty end -open preTm preTy +open Tm Ty -- Written backwards! -def preCon : Type := List preTy +def Con : Type := List Ty +instance : GetElem Con Nat Ty fun (Γ : Con) (i : Nat) => i < Γ.length := List.instGetElemNatLtLength mutual - def preWkArrTy : preTy → Nat → preTy - | preUU, _ => preUU - | preEL X, a => preEL (preWkArrTm X a) - | prePI X Y, a => prePI (preWkArrTm X a) (preWkArrTy Y (succ a)) - | preEQ A t t', a => preEQ (preWkArrTm A a) (preWkArrTm t a) (preWkArrTm t' a) - def preWkArrTm : preTm → Nat → preTm - | preVAR n, a => if n ≥ a then preVAR (succ n) else preVAR n - | preAPP f t, a => preAPP (preWkArrTm f a) (preWkArrTm t a) - | preTRANSP A eq t, a => preTRANSP (preWkArrTy A a) (preWkArrTm eq a) (preWkArrTm t a) + def WkArrTy : Ty → Nat → Ty + | UU, _ => UU + | EL X, a => EL (WkArrTm X a) + | PI X Y, a => PI (WkArrTm X a) (WkArrTy Y (succ a)) + | EQ A t t', a => EQ (WkArrTm A a) (WkArrTm t a) (WkArrTm t' a) + def WkArrTm : Tm → Nat → Tm + | VAR n, a => if n ≥ a then VAR (succ n) else VAR n + | APP f t, a => APP (WkArrTm f a) (WkArrTm t a) + | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a) end -def preWkTy (A : preTy) : preTy := preWkArrTy A 0 -def preWkTm (t : preTm) : preTm := preWkArrTm t 0 +def WkTy : (Γ : Con) → (n : Nat) → n < Γ.length → Ty +| Γ,0,h => WkArrTy (Γ[0]'h) 0 +| _::Γ,succ n,h => WkArrTy (WkTy Γ n (lt_of_succ_lt_succ h)) 0 + +def WkTm (t : Tm) : Tm := WkArrTm t 0 + +inductive order where +| LESS : order +| EQUAL : order +| GREATER : Nat → order +open order +def GRsucc : order → order +| LESS => LESS +| EQUAL => EQUAL +| GREATER m => GREATER (succ m) + +def comparePred : Nat → Nat → order +| 0, 0 => EQUAL +| 0, succ _ => LESS +| succ m, 0 => GREATER m +| succ m, succ n => GRsucc $ comparePred m n mutual - def preSubstTy : preTy → preTm → preTy - | preUU, _ => preUU - | preEL X, z => preEL (preSubstTm X z) - | prePI X Y, z => prePI (preSubstTm X z) (preSubstTy Y z) - | preEQ A t t', z => preEQ (preSubstTm A z) (preSubstTm t z) (preSubstTm t' z) - def preSubstTm : preTm → preTm → preTm - | preVAR 0, z => z - | preVAR (succ n), _ => preVAR n - | preAPP f t, z => preAPP (preSubstTm f z) (preSubstTm t z) - | preTRANSP A eq t, z => preTRANSP (preSubstTy A z) (preSubstTm eq z) (preSubstTm t z) -- ? + def SubstArrTy : Ty → Tm → Nat → Ty + | UU, _,_ => UU + | EL X, z, a => EL (SubstArrTm X z a) + | PI X Y, z, a => PI (SubstArrTm X z a) (SubstArrTy Y z (succ a)) + | EQ A t t', z, a => EQ (SubstArrTm A z a) (SubstArrTm t z a) (SubstArrTm t' z a) + def SubstArrTm : Tm → Tm → Nat → Tm + | VAR m, z, a => match comparePred m a with + | LESS => VAR m + | EQUAL => z + | GREATER m' => VAR m' + | APP f t, z, a => APP (SubstArrTm f z a) (SubstArrTm t z a) + | TRANSP X s s' Y eq t, z, a => TRANSP (SubstArrTm X z a) (SubstArrTm s z a) (SubstArrTm s' z a) (SubstArrTy Y z (succ a)) (SubstArrTm eq z a) (SubstArrTm t z a) end +def SubstTy := λ T t => SubstArrTy T t 0 +def SubstTm := λ t t' => SubstArrTm t t' 0 + + +structure indData where + (Con_D : Con → Type) + (Ty_D : (Γ : Con) → Con_D Γ → Ty → Type) + (Tm_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → Ty_D Γ Γ_D A → Tm → Type) + (nil_D : Con_D []) + (cons_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Con_D (A::Γ)) + (UU_D : (Γ : Con) → (Γ_D : Con_D Γ) → Ty_D Γ Γ_D UU) + (EL_D : (Γ : Con) → (Γ_D : Con_D Γ) → + (X : Tm) → Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X → + Ty_D Γ Γ_D (EL X)) + (PI_D : (Γ : Con) → (Γ_D : Con_D Γ) → + (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → + (Y : Ty) → Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y → + Ty_D Γ Γ_D (PI X Y)) + (EQ_D : (Γ : Con) → (Γ_D : Con_D Γ) → + (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → + (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) → + (s' : Tm) → (s'_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s') → + Ty_D Γ Γ_D (EQ X s s')) + (VAR_D :(Γ : Con) → (Γ_D : Con_D Γ) → + (n : Nat) → (h : n < List.length Γ) → + (A_D : Ty_D Γ Γ_D (WkTy Γ n h)) → + Tm_D Γ Γ_D (WkTy Γ n h) A_D (VAR n)) + (APP_D :(Γ : Con) → (Γ_D : Con_D Γ) → + (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → + (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) → + (f : Tm) → (f_D : Tm_D Γ Γ_D (PI X Y) (PI_D Γ Γ_D X X_D Y Y_D) f) → + (t : Tm) → (t_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) t) → + (Yt_D : Ty_D Γ Γ_D (SubstTy Y t)) → + Tm_D Γ Γ_D (SubstTy Y t) Yt_D (APP f t)) + (TRANSP_D :(Γ : Con) → (Γ_D : Con_D Γ) → + (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → + (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) → + (s' : Tm) → (s'_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s') → + (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) → + (Ys_D : Ty_D Γ Γ_D (SubstTy Y s)) → (Ys'_D : Ty_D Γ Γ_D (SubstTy Y s')) → + (p : Tm) → (p_D : Tm_D Γ Γ_D (EQ X s s') (EQ_D Γ Γ_D X X_D s s_D s' s'_D) p) → + (k : Tm) → Tm_D Γ Γ_D (SubstTy Y s) Ys_D k → + Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k)) mutual - inductive wfCon : preCon → Prop where - | wfNil : wfCon [] - | wfCons : {Γ : preCon} → {A : preTy} → wfTy Γ A → (_ : wfCon Γ) → wfCon (A::Γ) - - inductive wfTy : preCon → preTy → Prop - | wfWkTy : {Γ : preCon} → {A B : preTy} → wfTy Γ A → wfTy (B::Γ) (preWkTy A) - | wfUU : {Γ : preCon} → wfTy Γ preUU - | wfEL : {Γ : preCon} → {X : preTm} → wfTm Γ preUU X → wfTy Γ (preEL X) - | wfPI : {Γ : preCon} → {X : preTm} → {Y : preTy} → - wfTm Γ preUU X → wfTy (preEL X::Γ) Y → wfTy Γ (prePI X Y) - | wfEQ : {Γ : preCon} → {X t t' : preTm} → - wfTm Γ preUU X → wfTm Γ (preEL X) t → wfTm Γ (preEL X) t' → wfTy Γ (preEQ X t t') - | wfSubstTy : {Γ : preCon} → {A B : preTy} → {t : preTm} → - wfTy Γ B → wfTy (B::Γ) A → wfTm Γ B t → wfTy Γ (preSubstTy A t) - - inductive wfTm : preCon → preTy → preTm → Prop - | wfVAR0 : {Γ : preCon} → {A : preTy} → - wfTy Γ A → wfTm (A::Γ) (preWkTy A) (preVAR 0) - | wfWkTm : {Γ : preCon} → {A B : preTy} → {t : preTm} → - wfTm Γ A t → wfTy Γ B → wfTm (B::Γ) (preWkTy A) (preWkTm t) - | wfAPP : {Γ : preCon} → {X : preTm} → {Y : preTy} → {f t : preTm} → - wfTm Γ (prePI X Y) f → wfTm Γ (preEL X) t → wfTm Γ (preSubstTy Y t) (preAPP f t) - | wfTRANSP : {Γ : preCon} → {X eq t t' z: preTm} → {Y : preTy} → - {_ : wfTm Γ preUU X} → {_ : wfTy (preEL X::Γ) Y} → - {_ : wfTm Γ (preEL X) t} → {_ : wfTm Γ (preEL X) t'} → - wfTm Γ (preEQ X t t') eq → - wfTm Γ (preSubstTy Y t) z → - wfTm Γ (preSubstTy Y t') (preTRANSP Y eq z) - | wfSubstTm : {Γ : preCon} → {A B : preTy} → {t t': preTm} → - wfTm Γ B t → wfTm (B::Γ) A t' → wfTm Γ (preSubstTy A t) (preSubstTm t' t) + def elim (P : indData) : (Γ : Con) → P.Con_D Γ + | [] => P.nil_D + | A::Γ => P.cons_D _ (elim _ _) _ (elimTy _ _ _ _) + + def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → P.Ty_D Γ Γ_D A + | UU => P.UU_D Γ Γ_D + | EL X => P.EL_D _ _ _ (elimTm _ _ _ _ _ _) + | PI X Y => P.PI_D _ _ _ (elimTm _ _ _ _ _ _) _ (elimTy _ _ _ _) + | EQ X s s' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _) _ (elimTm _ _ _ _ _ _) _ (elimTm _ _ _ _ _ _) + + def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) (A : Ty) (A_D : P.Ty_D Γ Γ_D A) : (t : Tm) → P.Tm_D Γ Γ_D A A_D t + | APP f t => P.APP_D Γ Γ_D _ _ _ _ _ _ _ (elimTm _ _ _ _ _ _) _ + | TRANSP X s s' Y eq k => _ --P.TRANSP_D Γ Γ_D _ _ _ _ _ _ _ _ (elimTy _ _ _ _) (elimTy _ _ _ _) _ _ _ _ + | VAR n => _ end -open wfCon wfTy wfTm - -def Con : Type := { Γ : preCon // wfCon Γ } -def Ty (Γ : Con) : Type := { A : preTy // wfTy Γ.1 A} -def Tm (Γ : Con) (A : Ty Γ) : Type := { t : preTm // wfTm Γ.1 A.1 t} - -def EMPTY : Con := ⟨[], wfNil⟩ -def EXTEND (Γ : Con) (A : Ty Γ) : Con := ⟨ A.1 :: Γ.1 , wfCons A.2 Γ.2 ⟩ - -def UU {Γ : Con} : Ty Γ := ⟨ preUU , wfUU ⟩ -def EL (Γ : Con) (X : Tm Γ UU) : Ty Γ := ⟨ preEL X.1 , wfEL X.2 ⟩ -def PI (Γ : Con) (X : Tm Γ UU) (Y : Ty (EXTEND Γ (EL Γ X))) : Ty Γ := - ⟨ prePI X.1 Y.1 , wfPI X.2 Y.2 ⟩ -def EQ (Γ : Con) (X : Tm Γ UU) (t t' : Tm Γ (EL Γ X)) : Ty Γ := - ⟨ preEQ X.1 t.1 t'.1 , wfEQ X.2 t.2 t'.2 ⟩ - -def wkTy (Γ : Con)(B : Ty Γ)(A : Ty Γ) : Ty (EXTEND Γ B) := - ⟨ preWkTy A.1 , wfWkTy A.2 ⟩ -def substTy (Γ : Con)(B : Ty Γ)(A : Ty (EXTEND Γ B))(t : Tm Γ B) : Ty Γ := - ⟨ preSubstTy A.1 t.1, wfSubstTy B.2 A.2 t.2 ⟩ -def APP (Γ : Con)(X : Tm Γ UU)(Y : Ty (EXTEND Γ (EL Γ X)))(f : Tm Γ (PI Γ X Y))(t : Tm Γ (EL Γ X)) : Tm Γ (substTy Γ (EL Γ X) Y t) := - ⟨ preAPP f.1 t.1, wfAPP f.2 t.2 ⟩ - -def ZERO (Γ : Con)(A : Ty Γ) : Tm (EXTEND Γ A) (wkTy Γ A A) := - ⟨ preVAR 0, wfVAR0 A.2 ⟩ -def SUCC (Γ : Con)(B : Ty Γ)(A : Ty Γ) (t : Tm Γ A) : Tm (EXTEND Γ B) (wkTy Γ B A):= - ⟨ preWkTm t.1 , wfWkTm t.2 B.2 ⟩ - -def len : Con → Nat := λ Γ => List.length Γ.1 - --- #eval len $ EXTEND (EXTEND (EXTEND (EXTEND EMPTY UU) (PI ZERO (PI (SUCC ZERO) (EL $ SUCC $ SUCC $ ZERO)))) (EL $ SUCC $ ZERO)) (PI (SUCC $ SUCC $ ZERO) (EQ (SUCC $ SUCC $ SUCC $ ZERO) ZERO ZERO)) - - -infixl:10 " ▷ " => EXTEND -notation "⋄" => EMPTY - --- def ONE := SUCC ZERO -def UUnil := @UU ⋄ -def P := ⋄ ▷ UUnil -def Q := P ▷ EL P (ZERO ⋄ UUnil) -def P' := P ▷ PI P (ZERO ⋄ UUnil) (PI Q (SUCC P _ _ (ZERO ⋄ UUnil)) UU) -def Q' := P' ▷ EL _ (SUCC _ _ _ (ZERO _ _)) -def Q'' := Q' ▷ EL _ (SUCC _ _ _ (SUCC _ _ _ (ZERO _ _))) -def P'' := P' ▷ PI _ (SUCC _ _ _ (ZERO _ _)) - (EL _ (APP Q' (SUCC P' _ _ (SUCC P _ _ (ZERO ⋄ _))) UU - (APP Q' (SUCC _ _ _ (SUCC _ _ _ (ZERO _ _))) _ - _ - (ZERO _ _)) - (ZERO _ _) - ) - ) - -- - -- def x := @APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO) -- def Q := P'' ▷ PI (SUCC ZERO) (@EL P''' (@APP P''' _ _ _ _)) -- #reduce P''' --- #eval len $ +-- #eval len -- ⋄ ▷ UU ▷ PI ZERO UU -- ▷ PI (SUCC ZERO) (EL (@APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO))) --▷ (PI (SUCC ZERO) (EL (APP (SUCC ZERO) _ ))) From 5bcce79f6d58814d86923f5d7f6feadc0a7fcf10 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Sun, 16 Mar 2025 01:56:58 +0000 Subject: [PATCH 04/11] Progress on eliminator --- GeneralizedAlgebra/signature.lean | 63 ++++++++++++++++++++++++------- 1 file changed, 49 insertions(+), 14 deletions(-) diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 0e9614d..3eff5bc 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -112,22 +112,57 @@ structure indData where (p : Tm) → (p_D : Tm_D Γ Γ_D (EQ X s s') (EQ_D Γ Γ_D X X_D s s_D s' s'_D) p) → (k : Tm) → Tm_D Γ Γ_D (SubstTy Y s) Ys_D k → Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k)) +mutual + inductive goodCon : Con → Type where + | goodNil : goodCon [] + | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ) + + inductive goodTy : Con → Ty → Type where + | goodUU : ∀ {Γ : Con}, goodTy Γ UU + | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X) + | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y) + | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t') + -- | goodSubst : ∀ {Γ : Con}{X : Tm}{Y : Ty}{t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (EL X) t → goodTy Γ (SubstTy Y t) + + inductive goodTm : Con → Ty → Tm → Type where + | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WkTy Γ n h) (VAR n) + | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP f t) + | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm}, + goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t) + +end +open goodTm goodTy goodCon + +def goodSubstArr : ∀ {Γ : Con}{X : Tm}{s : Tm}{Y : Ty}, (a : Nat) → goodTm Γ UU X → goodTm Γ (EL X) s → goodTy (EL X::Γ) Y → goodTy Γ (SubstArrTy Y s a) := _ + +def goodSubst : ∀ {Γ : Con}{X : Tm}{s : Tm}{Y : Ty}, goodTm Γ UU X → goodTm Γ (EL X) s → goodTy (EL X::Γ) Y → goodTy Γ (SubstTy Y s) := goodSubstArr 0 mutual - def elim (P : indData) : (Γ : Con) → P.Con_D Γ - | [] => P.nil_D - | A::Γ => P.cons_D _ (elim _ _) _ (elimTy _ _ _ _) - - def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → P.Ty_D Γ Γ_D A - | UU => P.UU_D Γ Γ_D - | EL X => P.EL_D _ _ _ (elimTm _ _ _ _ _ _) - | PI X Y => P.PI_D _ _ _ (elimTm _ _ _ _ _ _) _ (elimTy _ _ _ _) - | EQ X s s' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _) _ (elimTm _ _ _ _ _ _) _ (elimTm _ _ _ _ _ _) - - def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) (A : Ty) (A_D : P.Ty_D Γ Γ_D A) : (t : Tm) → P.Tm_D Γ Γ_D A A_D t - | APP f t => P.APP_D Γ Γ_D _ _ _ _ _ _ _ (elimTm _ _ _ _ _ _) _ - | TRANSP X s s' Y eq k => _ --P.TRANSP_D Γ Γ_D _ _ _ _ _ _ _ _ (elimTy _ _ _ _) (elimTy _ _ _ _) _ _ _ _ - | VAR n => _ + def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ + | [],_ => P.nil_D + | A::Γ,goodCons gA gΓ => P.cons_D _ (elim _ _ gΓ) _ (elimTy _ _ _ _ gΓ gA) + + -- def dispGetElem (P : indData) (Γ : Con) (n : Nat) (h : n < List.length Γ) : + -- Σ (Γ_D : P.Con_D Γ), P.Ty_D Γ Γ_D (WkTy Γ n h) := ⟨elim _ _,elimTy _ _ _ _ _⟩ + + -- def dispWkTy : (P : indData) → + -- (Γ : Con) → (Γ_D : P.Con_D Γ) → + -- (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → + -- (n : Nat) → (h : n < List.length Γ) → + -- P.Ty_D Γ Γ_D (WkTy Γ n h) → + -- P.Ty_D (A::Γ) (P.cons_D _ Γ_D _ A_D) (WkTy (A::Γ) (succ n) (succ_lt_succ h)) := _ + + + def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → goodCon Γ → goodTy Γ A → P.Ty_D Γ Γ_D A + | UU,_,goodUU => P.UU_D Γ Γ_D + | EL X,gΓ,goodEL gX => P.EL_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) + | PI X Y,gΓ,goodPI gX gY => P.PI_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) + | EQ X s s',gΓ,goodEQ gX gs gs' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') + + def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → (t : Tm) → goodCon Γ → goodTy Γ A → goodTm Γ A t → P.Tm_D Γ Γ_D A A_D t + | _,_,APP f t,gΓ,_, @goodAPP _ X Y _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _ + | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gX gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gX gs gY) gk) + | _,_,VAR n, gΓ,_, (goodVAR _ h) => P.VAR_D Γ Γ_D n _ _ end -- def x := @APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO) From baaafec2ec469e02d5d896114d2748df2b5cb6ea Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Sun, 16 Mar 2025 21:11:36 +0000 Subject: [PATCH 05/11] Almost got good predicate on signature working --- GeneralizedAlgebra/signature.lean | 94 +++++++++++++++++++++---------- 1 file changed, 63 insertions(+), 31 deletions(-) diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 3eff5bc..60715a2 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -5,7 +5,7 @@ open Nat mutual inductive Tm : Type where | VAR : Nat → Tm - | APP : Tm → Tm → Tm + | APP : Tm → Ty → Tm → Tm → Tm | TRANSP : Tm → Tm → Tm → Ty → Tm → Tm → Tm inductive Ty : Type where @@ -28,7 +28,7 @@ mutual | EQ A t t', a => EQ (WkArrTm A a) (WkArrTm t a) (WkArrTm t' a) def WkArrTm : Tm → Nat → Tm | VAR n, a => if n ≥ a then VAR (succ n) else VAR n - | APP f t, a => APP (WkArrTm f a) (WkArrTm t a) + | APP X Y f t, a => APP (WkArrTm X a) (WkArrTy Y (succ a)) (WkArrTm f a) (WkArrTm t a) | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a) end @@ -61,17 +61,73 @@ mutual | PI X Y, z, a => PI (SubstArrTm X z a) (SubstArrTy Y z (succ a)) | EQ A t t', z, a => EQ (SubstArrTm A z a) (SubstArrTm t z a) (SubstArrTm t' z a) def SubstArrTm : Tm → Tm → Nat → Tm - | VAR m, z, a => match comparePred m a with + | VAR m, z, a => + match comparePred m a with | LESS => VAR m | EQUAL => z | GREATER m' => VAR m' - | APP f t, z, a => APP (SubstArrTm f z a) (SubstArrTm t z a) + | APP X Y f t, z, a => APP (SubstArrTm X z a) (SubstArrTy Y z (succ a)) (SubstArrTm f z a) (SubstArrTm t z a) | TRANSP X s s' Y eq t, z, a => TRANSP (SubstArrTm X z a) (SubstArrTm s z a) (SubstArrTm s' z a) (SubstArrTy Y z (succ a)) (SubstArrTm eq z a) (SubstArrTm t z a) end +def varElim {motive : Tm → Type} (m : Nat) (z : Tm) (mL : motive (VAR m)) (mE : motive z) (mG : (m' : Nat) → motive (VAR m')) (a : Nat) : motive (SubstArrTm (VAR m) z a) := +by + cases (comparePred m a) + dsimp[SubstArrTm] + sorry + sorry + sorry + + + +def substAt : (Γ : Con) → (z : Tm) → (a : Nat) → (a < Γ.length) → Con +| _::Γ,_,0,_ => Γ +| A::Γ,z,succ a,h => SubstArrTy A z (a) :: substAt Γ z a (lt_of_succ_lt_succ h) + +def trunc : (Γ : Con) → (a : Nat) → (a < Γ.length) → Con +| _::Γ,succ a',h => trunc Γ a' (lt_of_succ_lt_succ h) +| _::Γ,0,_ => Γ + def SubstTy := λ T t => SubstArrTy T t 0 def SubstTm := λ t t' => SubstArrTm t t' 0 +mutual + inductive goodCon : Con → Type where + | goodNil : goodCon [] + | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ) + + inductive goodTy : Con → Ty → Type where + | goodUU : ∀ {Γ : Con}, goodTy Γ UU + | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X) + | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y) + | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t') + + inductive goodTm : Con → Ty → Tm → Type where + | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WkTy Γ n h) (VAR n) + | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP X Y f t) + | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm}, + goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t) +end + +open goodTm goodTy goodCon +mutual + def goodSubstArrTy {Γ : Con} : (A : Ty) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTy (substAt Γ z a h) (SubstArrTy A z a) + | UU, _,_,_,_,_ => goodUU + | EL X,z,a,h,goodEL gX,gz => goodEL (goodSubstArrTm X z a h goodUU gX gz) + | EQ X t t',z,a,h,goodEQ gX gt gt',gz => goodEQ (goodSubstArrTm X z a h goodUU gX gz) (goodSubstArrTm t z a h (goodEL gX) gt gz) (goodSubstArrTm t' z a h (goodEL gX) gt' gz) + | PI X Y, z,a,h,goodPI gX gY,gz => goodPI (goodSubstArrTm X z a h goodUU gX gz) (@goodSubstArrTy (EL X :: Γ) Y z (succ a) (succ_lt_succ h) gY gz) + + def goodSubstArrTm {Γ : Con}{A : Ty} : (t : Tm) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm Γ A t → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm (substAt Γ z a h) (SubstArrTy A z a) (SubstArrTm t z a) + | APP X Y f t, z, a, h, _ , goodAPP gX gY gf gt,gz => + goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y t 0 (zero_lt_succ Γ.length) gY gt) (goodAPP gX gY gf gt) gz + | TRANSP X s s' Y eq t, z, a, h, _, goodTRANSP gX gs gs' gY geq gt,gz => + goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y s' 0 (zero_lt_succ Γ.length) gY gs') (goodTRANSP gX gs gs' gY geq gt) gz + | VAR m, z, a, h, gw, gv,gz => varElim _ _ _ _ _ _ +end + +def goodSubst {Γ : Con}{X : Tm}{s : Tm}{Y : Ty} (gs : goodTm Γ (EL X) s) (gY : goodTy (EL X::Γ) Y) : goodTy Γ (SubstTy Y s) := + @goodSubstArrTy (EL X :: Γ) Y s 0 (zero_lt_succ Γ.length) gY gs + structure indData where (Con_D : Con → Type) @@ -102,7 +158,7 @@ structure indData where (f : Tm) → (f_D : Tm_D Γ Γ_D (PI X Y) (PI_D Γ Γ_D X X_D Y Y_D) f) → (t : Tm) → (t_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) t) → (Yt_D : Ty_D Γ Γ_D (SubstTy Y t)) → - Tm_D Γ Γ_D (SubstTy Y t) Yt_D (APP f t)) + Tm_D Γ Γ_D (SubstTy Y t) Yt_D (APP X Y f t)) (TRANSP_D :(Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) → @@ -112,30 +168,6 @@ structure indData where (p : Tm) → (p_D : Tm_D Γ Γ_D (EQ X s s') (EQ_D Γ Γ_D X X_D s s_D s' s'_D) p) → (k : Tm) → Tm_D Γ Γ_D (SubstTy Y s) Ys_D k → Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k)) -mutual - inductive goodCon : Con → Type where - | goodNil : goodCon [] - | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ) - - inductive goodTy : Con → Ty → Type where - | goodUU : ∀ {Γ : Con}, goodTy Γ UU - | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X) - | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y) - | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t') - -- | goodSubst : ∀ {Γ : Con}{X : Tm}{Y : Ty}{t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (EL X) t → goodTy Γ (SubstTy Y t) - - inductive goodTm : Con → Ty → Tm → Type where - | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WkTy Γ n h) (VAR n) - | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP f t) - | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm}, - goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t) - -end -open goodTm goodTy goodCon - -def goodSubstArr : ∀ {Γ : Con}{X : Tm}{s : Tm}{Y : Ty}, (a : Nat) → goodTm Γ UU X → goodTm Γ (EL X) s → goodTy (EL X::Γ) Y → goodTy Γ (SubstArrTy Y s a) := _ - -def goodSubst : ∀ {Γ : Con}{X : Tm}{s : Tm}{Y : Ty}, goodTm Γ UU X → goodTm Γ (EL X) s → goodTy (EL X::Γ) Y → goodTy Γ (SubstTy Y s) := goodSubstArr 0 mutual def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ @@ -160,8 +192,8 @@ mutual | EQ X s s',gΓ,goodEQ gX gs gs' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → (t : Tm) → goodCon Γ → goodTy Γ A → goodTm Γ A t → P.Tm_D Γ Γ_D A A_D t - | _,_,APP f t,gΓ,_, @goodAPP _ X Y _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _ - | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gX gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gX gs gY) gk) + | _,_,APP X Y f t,gΓ,_, @goodAPP _ _ _ _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _ + | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gs gY) gk) | _,_,VAR n, gΓ,_, (goodVAR _ h) => P.VAR_D Γ Γ_D n _ _ end From 94a3c14ad2f32b6a55127957e1cb970a8c1795cf Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Sun, 23 Mar 2025 18:15:51 +0000 Subject: [PATCH 06/11] Commented out in-progress good signature and signature elim --- GeneralizedAlgebra/signature.lean | 236 ++++++++++++++++++++---------- 1 file changed, 157 insertions(+), 79 deletions(-) diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 60715a2..4cf4100 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -32,10 +32,11 @@ mutual | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a) end -def WkTy : (Γ : Con) → (n : Nat) → n < Γ.length → Ty +def WknTy : (Γ : Con) → (n : Nat) → n < Γ.length → Ty | Γ,0,h => WkArrTy (Γ[0]'h) 0 -| _::Γ,succ n,h => WkArrTy (WkTy Γ n (lt_of_succ_lt_succ h)) 0 +| _::Γ,succ n,h => WkArrTy (WknTy Γ n (lt_of_succ_lt_succ h)) 0 +def WkTy (T : Ty) : Ty := WkArrTy T 0 def WkTm (t : Tm) : Tm := WkArrTm t 0 inductive order where @@ -62,21 +63,24 @@ mutual | EQ A t t', z, a => EQ (SubstArrTm A z a) (SubstArrTm t z a) (SubstArrTm t' z a) def SubstArrTm : Tm → Tm → Nat → Tm | VAR m, z, a => - match comparePred m a with - | LESS => VAR m - | EQUAL => z - | GREATER m' => VAR m' + if m < a then VAR m else + if m = a then z + else VAR (pred m) + -- match comparePred m a with + -- | LESS => VAR m + -- | EQUAL => z + -- | GREATER m' => VAR m' | APP X Y f t, z, a => APP (SubstArrTm X z a) (SubstArrTy Y z (succ a)) (SubstArrTm f z a) (SubstArrTm t z a) | TRANSP X s s' Y eq t, z, a => TRANSP (SubstArrTm X z a) (SubstArrTm s z a) (SubstArrTm s' z a) (SubstArrTy Y z (succ a)) (SubstArrTm eq z a) (SubstArrTm t z a) end -def varElim {motive : Tm → Type} (m : Nat) (z : Tm) (mL : motive (VAR m)) (mE : motive z) (mG : (m' : Nat) → motive (VAR m')) (a : Nat) : motive (SubstArrTm (VAR m) z a) := -by - cases (comparePred m a) - dsimp[SubstArrTm] - sorry - sorry - sorry +-- def varElim {motive : Tm → Type} (m : Nat) (z : Tm) (mL : motive (VAR m)) (mE : motive z) (mG : (m' : Nat) → motive (VAR m')) (a : Nat) : motive (SubstArrTm (VAR m) z a) := +-- by +-- cases (comparePred m a) +-- dsimp[SubstArrTm] +-- sorry +-- sorry +-- sorry @@ -91,43 +95,107 @@ def trunc : (Γ : Con) → (a : Nat) → (a < Γ.length) → Con def SubstTy := λ T t => SubstArrTy T t 0 def SubstTm := λ t t' => SubstArrTm t t' 0 -mutual - inductive goodCon : Con → Type where - | goodNil : goodCon [] - | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ) - - inductive goodTy : Con → Ty → Type where - | goodUU : ∀ {Γ : Con}, goodTy Γ UU - | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X) - | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y) - | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t') - - inductive goodTm : Con → Ty → Tm → Type where - | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WkTy Γ n h) (VAR n) - | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP X Y f t) - | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm}, - goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t) -end - -open goodTm goodTy goodCon -mutual - def goodSubstArrTy {Γ : Con} : (A : Ty) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTy (substAt Γ z a h) (SubstArrTy A z a) - | UU, _,_,_,_,_ => goodUU - | EL X,z,a,h,goodEL gX,gz => goodEL (goodSubstArrTm X z a h goodUU gX gz) - | EQ X t t',z,a,h,goodEQ gX gt gt',gz => goodEQ (goodSubstArrTm X z a h goodUU gX gz) (goodSubstArrTm t z a h (goodEL gX) gt gz) (goodSubstArrTm t' z a h (goodEL gX) gt' gz) - | PI X Y, z,a,h,goodPI gX gY,gz => goodPI (goodSubstArrTm X z a h goodUU gX gz) (@goodSubstArrTy (EL X :: Γ) Y z (succ a) (succ_lt_succ h) gY gz) - - def goodSubstArrTm {Γ : Con}{A : Ty} : (t : Tm) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm Γ A t → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm (substAt Γ z a h) (SubstArrTy A z a) (SubstArrTm t z a) - | APP X Y f t, z, a, h, _ , goodAPP gX gY gf gt,gz => - goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y t 0 (zero_lt_succ Γ.length) gY gt) (goodAPP gX gY gf gt) gz - | TRANSP X s s' Y eq t, z, a, h, _, goodTRANSP gX gs gs' gY geq gt,gz => - goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y s' 0 (zero_lt_succ Γ.length) gY gs') (goodTRANSP gX gs gs' gY geq gt) gz - | VAR m, z, a, h, gw, gv,gz => varElim _ _ _ _ _ _ -end - -def goodSubst {Γ : Con}{X : Tm}{s : Tm}{Y : Ty} (gs : goodTm Γ (EL X) s) (gY : goodTy (EL X::Γ) Y) : goodTy Γ (SubstTy Y s) := - @goodSubstArrTy (EL X :: Γ) Y s 0 (zero_lt_succ Γ.length) gY gs - +-- mutual +-- inductive goodCon : Con → Type where +-- | goodNil : goodCon [] +-- | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ) + +-- inductive goodTy : Con → Ty → Type where +-- | goodUU : ∀ {Γ : Con}, goodTy Γ UU +-- | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X) +-- | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y) +-- | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t') + +-- inductive goodTm : Con → Ty → Tm → Type where +-- -- | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WknTy Γ n h) (VAR n) +-- | goodVAR0 : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodTm (A::Γ) (WkTy A) (VAR 0) +-- | goodSUCC : ∀ {Γ : Con}{A : Ty}{B : Ty}{m : Nat}, goodTy Γ A → goodTm Γ A (VAR m) → goodTm (B::Γ) (WkTy A) (VAR (succ m)) +-- | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP X Y f t) +-- | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm}, +-- goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t) +-- end + + +-- open goodTm goodTy goodCon + +-- theorem UU_stable : UU = WkTy UU := Eq.refl _ + +-- def good_Set : goodCon [UU] := by +-- apply goodCons +-- exact goodUU +-- exact goodNil + +-- def good_pointed : goodCon [EL (VAR 0),UU] := by +-- apply goodCons +-- apply goodEL +-- apply goodVAR0 +-- apply goodUU +-- exact good_Set + +-- def good_nat : goodCon [PI (VAR 1) (EL (VAR 2)),EL (VAR 0),UU] := by +-- apply goodCons +-- apply goodPI +-- rw [UU_stable] +-- apply goodSUCC +-- apply goodUU +-- rw [←UU_stable] +-- apply goodVAR0 +-- apply goodUU +-- apply goodEL +-- rw [UU_stable] +-- apply goodSUCC +-- apply goodUU +-- rw [UU_stable] +-- apply goodSUCC +-- apply goodUU +-- rw [←UU_stable] +-- rw [←UU_stable] +-- apply goodVAR0 +-- apply goodUU +-- exact good_pointed + + + + + +-- mutual +-- -- def SubstArrTy : Ty → Tm → Nat → Ty +-- -- def SubstArrTm : Tm → Tm → Nat → Tm +-- -- def WkArrTy : Ty → Nat → Ty +-- -- | UU, _ => UU +-- -- | EL X, a => EL (WkArrTm X a) +-- -- | PI X Y, a => PI (WkArrTm X a) (WkArrTy Y (succ a)) +-- -- | EQ A t t', a => EQ (WkArrTm A a) (WkArrTm t a) (WkArrTm t' a) +-- -- def WkArrTm : Tm → Nat → Tm +-- -- | VAR n, a => if n ≥ a then VAR (succ n) else VAR n +-- -- | APP X Y f t, a => APP (WkArrTm X a) (WkArrTy Y (succ a)) (WkArrTm f a) (WkArrTm t a) +-- -- | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a) +-- -- def goodWkArrTy {Γ : Con} : (A : Ty) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → + +-- -- def goodUntrunc {Γ : Con} (A : Ty) (z : Tm) : (a : Nat) → (h : a < Γ.length) → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm Γ (WknTy ) + +-- def goodSubstArrTy {Γ : Con} : (A : Ty) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTy (substAt Γ z a h) (SubstArrTy A z a) +-- | UU, _,_,_,_,_ => goodUU +-- | EL X,z,a,h,goodEL gX,gz => goodEL (goodSubstArrTm X z a h goodUU gX gz) +-- | EQ X t t',z,a,h,goodEQ gX gt gt',gz => goodEQ (goodSubstArrTm X z a h goodUU gX gz) (goodSubstArrTm t z a h (goodEL gX) gt gz) (goodSubstArrTm t' z a h (goodEL gX) gt' gz) +-- | PI X Y, z,a,h,goodPI gX gY,gz => goodPI (goodSubstArrTm X z a h goodUU gX gz) (@goodSubstArrTy (EL X :: Γ) Y z (succ a) (succ_lt_succ h) gY gz) + +-- def goodSubstArrTm {Γ : Con}{A : Ty} : (t : Tm) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm Γ A t → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm (substAt Γ z a h) (SubstArrTy A z a) (SubstArrTm t z a) +-- | APP X Y f t, z, a, h, _ , goodAPP gX gY gf gt,gz => +-- goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y t 0 (zero_lt_succ Γ.length) gY gt) (goodAPP gX gY gf gt) gz +-- | TRANSP X s s' Y eq t, z, a, h, _, goodTRANSP gX gs gs' gY geq gt,gz => +-- goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y s' 0 (zero_lt_succ Γ.length) gY gs') (goodTRANSP gX gs gs' gY geq gt) gz +-- | VAR m, z, a, h, gw, gv,gz => +-- if m < a then _ else +-- if m = a then _ else +-- _ +-- end + +-- def goodSubst {Γ : Con}{X : Tm}{s : Tm}{Y : Ty} (gs : goodTm Γ (EL X) s) (gY : goodTy (EL X::Γ) Y) : goodTy Γ (SubstTy Y s) := +-- @goodSubstArrTy (EL X :: Γ) Y s 0 (zero_lt_succ Γ.length) gY gs + +-- def extractGoodVar {Γ : Con}{A : Ty}{n : Nat} : goodTm Γ A (VAR n) → +-- ∃ (h : n < Γ.length), A = WknTy Γ n h := sorry structure indData where (Con_D : Con → Type) @@ -150,8 +218,8 @@ structure indData where Ty_D Γ Γ_D (EQ X s s')) (VAR_D :(Γ : Con) → (Γ_D : Con_D Γ) → (n : Nat) → (h : n < List.length Γ) → - (A_D : Ty_D Γ Γ_D (WkTy Γ n h)) → - Tm_D Γ Γ_D (WkTy Γ n h) A_D (VAR n)) + (A_D : Ty_D Γ Γ_D (WknTy Γ n h)) → + Tm_D Γ Γ_D (WknTy Γ n h) A_D (VAR n)) (APP_D :(Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) → @@ -169,33 +237,43 @@ structure indData where (k : Tm) → Tm_D Γ Γ_D (SubstTy Y s) Ys_D k → Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k)) -mutual - def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ - | [],_ => P.nil_D - | A::Γ,goodCons gA gΓ => P.cons_D _ (elim _ _ gΓ) _ (elimTy _ _ _ _ gΓ gA) - - -- def dispGetElem (P : indData) (Γ : Con) (n : Nat) (h : n < List.length Γ) : - -- Σ (Γ_D : P.Con_D Γ), P.Ty_D Γ Γ_D (WkTy Γ n h) := ⟨elim _ _,elimTy _ _ _ _ _⟩ - - -- def dispWkTy : (P : indData) → - -- (Γ : Con) → (Γ_D : P.Con_D Γ) → - -- (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → - -- (n : Nat) → (h : n < List.length Γ) → - -- P.Ty_D Γ Γ_D (WkTy Γ n h) → - -- P.Ty_D (A::Γ) (P.cons_D _ Γ_D _ A_D) (WkTy (A::Γ) (succ n) (succ_lt_succ h)) := _ - - - def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → goodCon Γ → goodTy Γ A → P.Ty_D Γ Γ_D A - | UU,_,goodUU => P.UU_D Γ Γ_D - | EL X,gΓ,goodEL gX => P.EL_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) - | PI X Y,gΓ,goodPI gX gY => P.PI_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) - | EQ X s s',gΓ,goodEQ gX gs gs' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') - - def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → (t : Tm) → goodCon Γ → goodTy Γ A → goodTm Γ A t → P.Tm_D Γ Γ_D A A_D t - | _,_,APP X Y f t,gΓ,_, @goodAPP _ _ _ _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _ - | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gs gY) gk) - | _,_,VAR n, gΓ,_, (goodVAR _ h) => P.VAR_D Γ Γ_D n _ _ -end + +-- mutual +-- def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ +-- | [],_ => P.nil_D +-- | A::Γ,goodCons gA gΓ => P.cons_D _ (elim _ _ gΓ) _ (elimTy _ _ _ _ gΓ gA) + +-- -- def dispGetElem (P : indData) (Γ : Con) (n : Nat) (h : n < List.length Γ) : +-- -- Σ (Γ_D : P.Con_D Γ), P.Ty_D Γ Γ_D (WknTy Γ n h) := ⟨elim _ _,elimTy _ _ _ _ _⟩ + +-- -- def dispWknTy : (P : indData) → +-- -- (Γ : Con) → (Γ_D : P.Con_D Γ) → +-- -- (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → +-- -- (n : Nat) → (h : n < List.length Γ) → +-- -- P.Ty_D Γ Γ_D (WknTy Γ n h) → +-- -- P.Ty_D (A::Γ) (P.cons_D _ Γ_D _ A_D) (WknTy (A::Γ) (succ n) (succ_lt_succ h)) := _ +-- def elimWknTy {P : indData} : (Γ : Con) → (Γ_D : P.Con_D Γ) → (n : Nat) → (h : n < Γ.length) → P.Ty_D Γ Γ_D (WknTy Γ n h) +-- | A::Γ , _ , 0 , _ => _ + +-- def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → goodCon Γ → goodTy Γ A → P.Ty_D Γ Γ_D A +-- | UU,_,goodUU => P.UU_D Γ Γ_D +-- | EL X,gΓ,goodEL gX => P.EL_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) +-- | PI X Y,gΓ,goodPI gX gY => P.PI_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) +-- | EQ X s s',gΓ,goodEQ gX gs gs' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') + +-- def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → (t : Tm) → goodCon Γ → goodTy Γ A → goodTm Γ A t → P.Tm_D Γ Γ_D A A_D t +-- | _,_,APP X Y f t,gΓ,_, @goodAPP _ _ _ _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _ +-- | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gs gY) gk) +-- | A,_,VAR n, gΓ,gA, gv => by +-- let hh := @extractGoodVar _ _ _ gv +-- let h := hh.1 +-- let p : A = WknTy Γ n h := hh.2 +-- rw [p] + +-- -- rw p + +-- -- P.VAR_D Γ Γ_D n h (elimWknTy Γ Γ_D n h) +-- end -- def x := @APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO) -- def Q := P'' ▷ PI (SUCC ZERO) (@EL P''' (@APP P''' _ _ _ _)) From 0f14ec2bc1fc5985878a5c03da3c5d6e034e34a1 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Tue, 1 Apr 2025 11:29:11 +0100 Subject: [PATCH 07/11] Further work on getting general elimination to work --- GeneralizedAlgebra/nouGAT.lean | 98 ++++++++++---------- GeneralizedAlgebra/signature.lean | 64 +++++++++++-- GeneralizedAlgebra/signatures/bipointed.lean | 20 +++- GeneralizedAlgebra/signatures/pointed.lean | 29 +++++- GeneralizedAlgebra/signatures/set.lean | 10 +- 5 files changed, 161 insertions(+), 60 deletions(-) diff --git a/GeneralizedAlgebra/nouGAT.lean b/GeneralizedAlgebra/nouGAT.lean index 9298fdc..bf76edd 100644 --- a/GeneralizedAlgebra/nouGAT.lean +++ b/GeneralizedAlgebra/nouGAT.lean @@ -2,7 +2,7 @@ import GeneralizedAlgebra.signature import Lean open Lean Elab Meta -open Con Subst Ty Tm +open Ty Tm declare_syntax_cat gat_ty syntax "U" : gat_ty @@ -80,15 +80,17 @@ structure varTel (VV : varStruct) where def varLookup (VV : varStruct) (key : String) : MetaM Expr := VV.f key +#check mkNatLit + def varExtend (VV : varStruct) (key : String) (ctx : Expr) (newType : Expr) (newCtx : Expr) (newTelescope : List metaArg) (resT : Expr): varStruct := ⟨ λ s => if s=key - then mkAppM ``V0 #[ ctx , newType ] + then mkAppM ``VAR #[ mkNatLit 0 ] else do let old ← varLookup VV s - let ID ← mkAppM ``ID #[newCtx] - let p ← mkAppM ``PROJ1 #[ID] - mkAppM ``SUBST_Tm #[ p , old], + -- let ID ← mkAppM ``ID #[newCtx] + -- let p ← mkAppM ``PROJ1 #[ID] + mkAppM ``WkTm #[ old ], VV.topnames ++ [key], VV.telescopes ++ [(newTelescope,resT)], λ s => if s=key then return newTelescope else VV.getArgs s @@ -103,17 +105,17 @@ def varTelLookup {VV : varStruct} (TT : varTel VV) (key : String) : MetaM (Expr let args ← (VV.getArgs key) <|> return [] return (T,args) -def varTelExtend {VV : varStruct} (TT : varTel VV) (newArg : metaArg) (ctx : Expr) (newCtx : Expr) : varTel VV := -⟨ λ s => - if argMatch s newArg - then mkAppM ``V0 #[ ctx , extractMetaTy newArg ] - else do - let (old,_) ← varTelLookup TT s - let ID ← mkAppM ``ID #[newCtx] - let p ← mkAppM ``PROJ1 #[ID] - mkAppM ``SUBST_Tm #[ p , old], - TT.args ++ [newArg], -⟩ +-- def varTelExtend {VV : varStruct} (TT : varTel VV) (newArg : metaArg) (ctx : Expr) (newCtx : Expr) : varTel VV := +-- ⟨ λ s => +-- if argMatch s newArg +-- then mkAppM ``V0 #[ ctx , extractMetaTy newArg ] +-- else do +-- let (old,_) ← varTelLookup TT s +-- let ID ← mkAppM ``ID #[newCtx] +-- let p ← mkAppM ``PROJ1 #[ID] +-- mkAppM ``SUBST_Tm #[ p , old], +-- TT.args ++ [newArg], +-- ⟩ partial def splitArgList (message : String) : List metaArg → MetaM (metaArg × List metaArg) | [] => throwError message @@ -129,23 +131,23 @@ partial def failIfExplicitArgs (message : String) : List metaArg → MetaM Unit partial def elabGATTm {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Syntax → MetaM (Expr × List metaArg) | `(gat_tm| ( $g:gat_tm ) ) => elabGATTm ctx TT g -| `(gat_tm| $g1:gat_tm $g2:gat_tm ) => do - let (t1,args1) ← elabGATTm ctx TT g1 - let (A,args1') ← splitArgList "Too many args #0" args1 - -- TODO: Check the type of A against the type of t2 - let Appt1 ← mkAppM ``APP #[t1] - let (t2,args2)← elabGATTm ctx TT g2 - failIfExplicitArgs "Insufficient Args #0" args2 - -- let actualT2 ← reduce t2 - -- let expectedT2 ← reduce (extractMetaTy A) - -- let tyMatch ← isDefEq actualT2 expectedT2 - -- if (not tyMatch) then - -- throwError "X" - -- else do - let ID ← mkAppM ``ID #[ctx] - let substt2 ← mkAppM ``PAIR #[ID,t2] - let resT ← mkAppM ``SUBST_Tm #[substt2,Appt1] - return (resT,args1') +-- | `(gat_tm| $g1:gat_tm $g2:gat_tm ) => do +-- let (t1,args1) ← elabGATTm ctx TT g1 +-- let (A,args1') ← splitArgList "Too many args #0" args1 +-- -- TODO: Check the type of A against the type of t2 +-- let Appt1 ← mkAppM ``APP #[t1] +-- let (t2,args2)← elabGATTm ctx TT g2 +-- failIfExplicitArgs "Insufficient Args #0" args2 +-- -- let actualT2 ← reduce t2 +-- -- let expectedT2 ← reduce (extractMetaTy A) +-- -- let tyMatch ← isDefEq actualT2 expectedT2 +-- -- if (not tyMatch) then +-- -- throwError "X" +-- -- else do +-- let ID ← mkAppM ``ID #[ctx] +-- let substt2 ← mkAppM ``PAIR #[ID,t2] +-- let resT ← mkAppM ``SUBST_Tm #[substt2,Appt1] +-- return (resT,args1') | `(gat_tm| $i:ident ) => do varTelLookup TT i.getId.toString -- let args ← vars.getArgs i.getI @@ -174,22 +176,22 @@ partial def elabGATArg {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Synt partial def elabGATTy {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Syntax → MetaM (varTel vars × Expr × Expr) -| `(gat_ty| ( $g:gat_ty ) ) => elabGATTy ctx TT g +-- | `(gat_ty| ( $g:gat_ty ) ) => elabGATTy ctx TT g | `(gat_ty| U ) => return (TT, .const ``UU [], .const ``UU []) | `(gat_ty| $x:gat_tm ) => do let t ← elabClosedGATTm ctx TT x let T ← mkAppM ``EL #[t] return (TT, T, T) -| `(gat_ty| $T:gat_arg ⇒ $T':gat_ty) => do - let argT ← elabGATArg ctx TT T - let domain := extractMetaTy argT - let elDomain ← mkAppM ``EL #[domain] - let elT ← argEl argT - let newCtx ← mkAppM ``EXTEND #[ctx,elDomain] - let newTT := varTelExtend TT elT ctx newCtx - let (newnewTT,codomain,resT) ← elabGATTy newCtx newTT T' - let result ← mkAppM ``PI #[domain,codomain] - return (newnewTT,result,resT) +-- | `(gat_ty| $T:gat_arg ⇒ $T':gat_ty) => do +-- let argT ← elabGATArg ctx TT T +-- let domain := extractMetaTy argT +-- let elDomain ← mkAppM ``EL #[domain] +-- let elT ← argEl argT +-- let newCtx ← mkAppM ``EXTEND #[ctx,elDomain] +-- let newTT := varTelExtend TT elT ctx newCtx +-- let (newnewTT,codomain,resT) ← elabGATTy newCtx newTT T' +-- let result ← mkAppM ``PI #[domain,codomain] +-- return (newnewTT,result,resT) | `(gat_ty| $t1:gat_tm ≡ $t2:gat_tm) => do let tt1 ← elabClosedGATTm ctx TT t1 let tt2 ← elabClosedGATTm ctx TT t2 @@ -213,9 +215,9 @@ partial def elabGATCon_core (ctx : Expr) (vars : varStruct) : Syntax → MetaM ( return (newCtx, newVars) | `(con_inner| $d:gat_decl ) => do let (i,TT,T,resT) ← elabGATdecl ctx vars d - let newCtx ← mkAppM ``EXTEND #[ctx, T] + let newCtx ← mkAppM ``EXTEND #[ctx,T] let newVars := varExtend vars i ctx T newCtx TT.args resT - let res ← mkAppM ``EXTEND #[ctx, T] + let res ← mkAppM ``EXTEND #[ctx,T] return (res, newVars) -- | `(gat_con| include $g:ident as ( $is:ident_list ); $rest:gat_con ) => do -- let (newCon,newVars) ← elab_ident_list ctx (.const g.getId []) vars is @@ -256,12 +258,12 @@ partial def elabGATCon : Syntax → MetaM Expr | `(con_outer| ⦃ ⦄ ) => do let emptyStrList ← mkListStrLit [] let emptyLArgList ← mkListListArgLit [] - mkAppM ``GAT.mk #[.const ``EMPTY [],emptyStrList,emptyLArgList] + mkAppM ``GATdata.mk #[.const ``EMPTY [],emptyStrList,emptyLArgList] | `(con_outer| ⦃ $s:con_inner ⦄ ) => do let (resCon,VV) ← elabGATCon_core (.const ``EMPTY []) varEmpty s let topList ← mkListStrLit VV.topnames let telescopes ← mkListListArgLit VV.telescopes - mkAppM ``GAT.mk #[resCon,topList,telescopes] + mkAppM ``GATdata.mk #[resCon,topList,telescopes] | _ => throwError "ConFail" diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 4cf4100..cd616fa 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -19,6 +19,8 @@ open Tm Ty -- Written backwards! def Con : Type := List Ty instance : GetElem Con Nat Ty fun (Γ : Con) (i : Nat) => i < Γ.length := List.instGetElemNatLtLength +def EXTEND (Γ : Con) (A : Ty) := A :: Γ +def EMPTY : Con := [] mutual def WkArrTy : Ty → Nat → Ty @@ -36,8 +38,17 @@ def WknTy : (Γ : Con) → (n : Nat) → n < Γ.length → Ty | Γ,0,h => WkArrTy (Γ[0]'h) 0 | _::Γ,succ n,h => WkArrTy (WknTy Γ n (lt_of_succ_lt_succ h)) 0 -def WkTy (T : Ty) : Ty := WkArrTy T 0 -def WkTm (t : Tm) : Tm := WkArrTm t 0 +mutual + def WkTy : Ty → Ty + | UU => UU + | EL X => EL (WkTm X) + | EQ A t t' => EQ (WkTm A) (WkTm t) (WkTm t') + | T => WkArrTy T 0 + def WkTm : Tm → Tm + | VAR n => VAR (succ n) + | TRANSP X s s' Y eq t => TRANSP (WkTm X) (WkTm s) (WkTm s') (WkTy Y) (WkTm eq) (WkTm t) + | t => WkArrTm t 0 +end inductive order where | LESS : order @@ -118,7 +129,7 @@ def SubstTm := λ t t' => SubstArrTm t t' 0 -- open goodTm goodTy goodCon --- theorem UU_stable : UU = WkTy UU := Eq.refl _ +theorem UU_stable : UU = WkTy UU := Eq.refl _ -- def good_Set : goodCon [UU] := by -- apply goodCons @@ -203,6 +214,7 @@ structure indData where (Tm_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → Ty_D Γ Γ_D A → Tm → Type) (nil_D : Con_D []) (cons_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Con_D (A::Γ)) + (WkTy_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A)) (UU_D : (Γ : Con) → (Γ_D : Con_D Γ) → Ty_D Γ Γ_D UU) (EL_D : (Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X → @@ -216,10 +228,18 @@ structure indData where (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) → (s' : Tm) → (s'_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s') → Ty_D Γ Γ_D (EQ X s s')) - (VAR_D :(Γ : Con) → (Γ_D : Con_D Γ) → - (n : Nat) → (h : n < List.length Γ) → - (A_D : Ty_D Γ Γ_D (WknTy Γ n h)) → - Tm_D Γ Γ_D (WknTy Γ n h) A_D (VAR n)) + -- (VAR_D :(Γ : Con) → (Γ_D : Con_D Γ) → + -- (n : Nat) → (h : n < List.length Γ) → + -- (A_D : Ty_D Γ Γ_D (WknTy Γ n h)) → + -- Tm_D Γ Γ_D (WknTy Γ n h) A_D (VAR n)) + (VAR0_D : (Γ : Con) → (Γ_D : Con_D Γ) → + (A : Ty) → (A_D : Ty_D Γ Γ_D A) → (A'_D : Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A)) → + Tm_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A) A'_D (VAR 0) + ) + (VARSUCC_D : (Γ : Con) → (Γ_D : Con_D Γ) → + (A : Ty) → (A_D : Ty_D Γ Γ_D A) → (t : Tm) → + (B : Ty) → (B_D : Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) B) → + Tm_D Γ Γ_D A A_D t → Tm_D (A::Γ) (cons_D Γ Γ_D A A_D) B B_D (WkTm t)) (APP_D :(Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) → @@ -238,6 +258,36 @@ structure indData where Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k)) +-- def VAR0_D {P : indData} + +inductive Arg : Type where +| Impl : String → Ty → Arg +| Expl : String → Ty → Arg +| Anon : Ty → Arg +open Arg + +def getName : Arg → Option String +| Impl i _ => some i +| Expl i _ => some i +| Anon _ => none + + +structure GATdata where + (con : Con) + (topnames : List String) + (telescopes : List (List Arg × Ty)) + +structure GAT extends GATdata where + (elim : (P : indData) → P.Con_D con) + +-- #check Listappend +def GAT.subnames (𝔊 : GAT) : List String := + List.join $ + List.map (λ (L,s) => L ++ [s]) $ + List.zip + (List.map ((mappartial getName) ∘ Prod.fst) (𝔊.telescopes)) + (𝔊.topnames) + -- mutual -- def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ -- | [],_ => P.nil_D diff --git a/GeneralizedAlgebra/signatures/bipointed.lean b/GeneralizedAlgebra/signatures/bipointed.lean index ca6378b..3b7c87d 100644 --- a/GeneralizedAlgebra/signatures/bipointed.lean +++ b/GeneralizedAlgebra/signatures/bipointed.lean @@ -1,3 +1,19 @@ -import GeneralizedAlgebra.nouGAT +import GeneralizedAlgebra.signatures.pointed -def 𝔅 : GAT := ⦃ X : U, x : X, x' : X ⦄ +def 𝔅 : GAT := ⟨ + ⦃ X : U, x : X, x' : X ⦄, + + by + intro P + apply P.cons_D + apply P.EL_D + rw [WkTm] + have helper := P.VARSUCC_D [Ty.EL (Tm.VAR 0), Ty.UU] --[Ty.UU] (P.cons_D _ P.nil_D _ (P.UU_D _ _)) (Ty.EL (Tm.VAR 0)) (P.EL_D _ _ _ (P.VAR0_D _ _ _ _ _)) (Tm.VAR 0) Ty.UU (P.UU_D _ _) -- (Ty.EL (Tm.VAR 1)) + -- rw [WkTm] at helper + apply helper + have helper' := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) + rw [WkTy] at helper' + apply helper' + + + ⟩ diff --git a/GeneralizedAlgebra/signatures/pointed.lean b/GeneralizedAlgebra/signatures/pointed.lean index 3110289..e7c129c 100644 --- a/GeneralizedAlgebra/signatures/pointed.lean +++ b/GeneralizedAlgebra/signatures/pointed.lean @@ -1,4 +1,29 @@ import GeneralizedAlgebra.nouGAT -def 𝔓 : GAT := ⦃ X : U, x : X -⦄ + +def pointedLemma (P : indData) : + P.Tm_D + [Ty.UU] + (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) + (Ty.EL (Tm.VAR 0)) + (P.EL_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) (Tm.VAR 0) (P.VAR0_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D) (P.UU_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D))))) + (Tm.VAR 0) + := by + + have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) (P.UU_D _ _) + -- rw [WkTy] at helper + sorry + + + +def 𝔓 : GAT := ⟨ + ⦃ X : U, x : X ⦄, + + by + intro P + apply P.cons_D + apply P.EL_D + have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) + rw [WkTy] at helper + apply helper + ⟩ diff --git a/GeneralizedAlgebra/signatures/set.lean b/GeneralizedAlgebra/signatures/set.lean index 9783762..dd9055c 100644 --- a/GeneralizedAlgebra/signatures/set.lean +++ b/GeneralizedAlgebra/signatures/set.lean @@ -1,3 +1,11 @@ import GeneralizedAlgebra.nouGAT -def 𝔖𝔢𝔱 : GAT := ⦃ X : U ⦄ +def 𝔖𝔢𝔱 : GAT := ⟨ + ⦃ X : U ⦄, + + by + intro P + apply P.cons_D + apply P.UU_D + apply P.nil_D + ⟩ From ebc49aa0bef56bb43dd85ef34ee4e8f40dff97c3 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Mon, 16 Jun 2025 19:00:35 +0000 Subject: [PATCH 08/11] Fixed VARSUCC_D in indData, got bipointed and nat eliminable, made some progress towards AlgPrinting --- GeneralizedAlgebra.lean | 186 ++++++++-------- GeneralizedAlgebra/AlgPrinting.lean | 216 +++---------------- GeneralizedAlgebra/nouGAT.lean | 40 ++-- GeneralizedAlgebra/signature.lean | 20 +- GeneralizedAlgebra/signatures/bipointed.lean | 17 +- GeneralizedAlgebra/signatures/nat.lean | 9 +- GeneralizedAlgebra/signatures/pointed.lean | 41 ++-- 7 files changed, 185 insertions(+), 344 deletions(-) diff --git a/GeneralizedAlgebra.lean b/GeneralizedAlgebra.lean index 369c3a0..699283f 100644 --- a/GeneralizedAlgebra.lean +++ b/GeneralizedAlgebra.lean @@ -1,106 +1,108 @@ import GeneralizedAlgebra.AlgPrinting -import GeneralizedAlgebra.ConPrinting +-- import GeneralizedAlgebra.ConPrinting import GeneralizedAlgebra.signatures.set import GeneralizedAlgebra.signatures.pointed import GeneralizedAlgebra.signatures.bipointed import GeneralizedAlgebra.signatures.nat -import GeneralizedAlgebra.signatures.evenodd -import GeneralizedAlgebra.signatures.quiver -import GeneralizedAlgebra.signatures.refl_quiver -import GeneralizedAlgebra.signatures.monoid -import GeneralizedAlgebra.signatures.group -import GeneralizedAlgebra.signatures.preorder -import GeneralizedAlgebra.signatures.setoid -import GeneralizedAlgebra.signatures.category -import GeneralizedAlgebra.signatures.groupoid -import GeneralizedAlgebra.signatures.CwF -import GeneralizedAlgebra.signatures.PCwF +-- import GeneralizedAlgebra.signatures.evenodd +-- import GeneralizedAlgebra.signatures.quiver +-- import GeneralizedAlgebra.signatures.refl_quiver +-- import GeneralizedAlgebra.signatures.monoid +-- import GeneralizedAlgebra.signatures.group +-- import GeneralizedAlgebra.signatures.preorder +-- import GeneralizedAlgebra.signatures.setoid +-- import GeneralizedAlgebra.signatures.category +-- import GeneralizedAlgebra.signatures.groupoid +-- import GeneralizedAlgebra.signatures.CwF +-- import GeneralizedAlgebra.signatures.PCwF /- ## Basic structures -/ --- Sets -#eval 𝔖𝔢𝔱 -#eval Alg 𝔖𝔢𝔱 -#eval DAlg 𝔖𝔢𝔱 none ["P"] -#eval DAlg 𝔖𝔢𝔱 (some "𝔖𝔢𝔱") ["P"] - --- Pointed sets -#eval 𝔓 -#eval Alg 𝔓 -#eval DAlg 𝔓 none ["P"] -#eval DAlg 𝔓 (some "𝔓") ["P","p₀"] ["X","x₀"] - --- Bipointed sets -#eval 𝔅 -#eval Alg 𝔅 -#eval DAlg 𝔅 none ["P"] -#eval DAlg 𝔅 (some "𝔅") ["P","p₀","p₁"] - --- Natural numbers -#eval 𝔑 -#eval Alg 𝔑 -#eval DAlg 𝔑 none ["P","n"] ["N","z","s"] -#eval DAlg 𝔑 (some "𝔑") ["P","base_case","n","ind_step"] - --- Even/Odd Natural Numbers -#eval 𝔈𝔒 -#eval Alg 𝔈𝔒 -#eval DAlg 𝔈𝔒 none ["Pe","Po","n","m"] -#eval DAlg 𝔈𝔒 (some "𝔑") ["Pe", "Po", "bc","n","ih","m","ih'"] - --- Monoids -#eval 𝔐𝔬𝔫 --- #eval Alg 𝔐𝔬𝔫 none -#eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫") - --- Groups -#eval 𝔊𝔯𝔭 --- #eval Alg 𝔊𝔯𝔭 none -#eval Alg 𝔊𝔯𝔭 (some "𝔊𝔯𝔭") - -/- -## Quiver-like structures --/ --- Quivers -#eval 𝔔𝔲𝔦𝔳 -#eval Alg 𝔔𝔲𝔦𝔳 --- -- Reflexive quivers -#eval 𝔯𝔔𝔲𝔦𝔳 -#eval Alg 𝔯𝔔𝔲𝔦𝔳 +#eval 𝔓.elim AlgStr +-- Sets +-- #eval 𝔖𝔢𝔱 +-- #eval Alg 𝔖𝔢𝔱 +-- #eval DAlg 𝔖𝔢𝔱 none ["P"] +-- #eval DAlg 𝔖𝔢𝔱 (some "𝔖𝔢𝔱") ["P"] + +-- -- Pointed sets +-- #eval 𝔓 +-- #eval Alg 𝔓 +-- #eval DAlg 𝔓 none ["P"] +-- #eval DAlg 𝔓 (some "𝔓") ["P","p₀"] ["X","x₀"] + +-- -- Bipointed sets +-- #eval 𝔅 +-- #eval Alg 𝔅 +-- #eval DAlg 𝔅 none ["P"] +-- #eval DAlg 𝔅 (some "𝔅") ["P","p₀","p₁"] + +-- -- Natural numbers +-- #eval 𝔑 +-- #eval Alg 𝔑 +-- #eval DAlg 𝔑 none ["P","n"] ["N","z","s"] +-- #eval DAlg 𝔑 (some "𝔑") ["P","base_case","n","ind_step"] + +-- -- Even/Odd Natural Numbers +-- #eval 𝔈𝔒 +-- #eval Alg 𝔈𝔒 +-- #eval DAlg 𝔈𝔒 none ["Pe","Po","n","m"] +-- #eval DAlg 𝔈𝔒 (some "𝔑") ["Pe", "Po", "bc","n","ih","m","ih'"] -- -- Monoids -#eval 𝔐𝔬𝔫 -#eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫") - --- -- Preorders -#eval 𝔓𝔯𝔢𝔒𝔯𝔡 -#eval Alg 𝔓𝔯𝔢𝔒𝔯𝔡 (some "𝔓𝔯𝔢𝔒𝔯𝔡") - --- -- Setoids -#eval 𝔖𝔢𝔱𝔬𝔦𝔡 -#eval Alg 𝔖𝔢𝔱𝔬𝔦𝔡 (some "𝔖𝔢𝔱𝔬𝔦𝔡") - --- -- Categories -#eval ℭ𝔞𝔱 -#eval Alg ℭ𝔞𝔱 (some "ℭ𝔞𝔱") - --- -- Groupoids -#eval 𝔊𝔯𝔭𝔡 -#eval Alg 𝔊𝔯𝔭𝔡 (some "𝔊𝔯𝔭𝔡") - - -/- -## Models of Type Theory --/ --- Categories with Families -#eval ℭ𝔴𝔉 -#eval Alg ℭ𝔴𝔉 (some "ℭ𝔴𝔉") -#eval Alg ℭ𝔴𝔉 none CwF_inlinenames - --- -- Polarized Categories with Families -#eval 𝔓ℭ𝔴𝔉 -#eval Alg 𝔓ℭ𝔴𝔉 (some "𝔓ℭ𝔴𝔉") +-- #eval 𝔐𝔬𝔫 +-- -- #eval Alg 𝔐𝔬𝔫 none +-- #eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫") + +-- -- Groups +-- #eval 𝔊𝔯𝔭 +-- -- #eval Alg 𝔊𝔯𝔭 none +-- #eval Alg 𝔊𝔯𝔭 (some "𝔊𝔯𝔭") + +-- /- +-- ## Quiver-like structures +-- -/ +-- -- Quivers +-- #eval 𝔔𝔲𝔦𝔳 +-- #eval Alg 𝔔𝔲𝔦𝔳 + +-- -- -- Reflexive quivers +-- #eval 𝔯𝔔𝔲𝔦𝔳 +-- #eval Alg 𝔯𝔔𝔲𝔦𝔳 + +-- -- -- Monoids +-- #eval 𝔐𝔬𝔫 +-- #eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫") + +-- -- -- Preorders +-- #eval 𝔓𝔯𝔢𝔒𝔯𝔡 +-- #eval Alg 𝔓𝔯𝔢𝔒𝔯𝔡 (some "𝔓𝔯𝔢𝔒𝔯𝔡") + +-- -- -- Setoids +-- #eval 𝔖𝔢𝔱𝔬𝔦𝔡 +-- #eval Alg 𝔖𝔢𝔱𝔬𝔦𝔡 (some "𝔖𝔢𝔱𝔬𝔦𝔡") + +-- -- -- Categories +-- #eval ℭ𝔞𝔱 +-- #eval Alg ℭ𝔞𝔱 (some "ℭ𝔞𝔱") + +-- -- -- Groupoids +-- #eval 𝔊𝔯𝔭𝔡 +-- #eval Alg 𝔊𝔯𝔭𝔡 (some "𝔊𝔯𝔭𝔡") + + +-- /- +-- ## Models of Type Theory +-- -/ +-- -- Categories with Families +-- #eval ℭ𝔴𝔉 +-- #eval Alg ℭ𝔴𝔉 (some "ℭ𝔴𝔉") +-- #eval Alg ℭ𝔴𝔉 none CwF_inlinenames + +-- -- -- Polarized Categories with Families +-- #eval 𝔓ℭ𝔴𝔉 +-- #eval Alg 𝔓ℭ𝔴𝔉 (some "𝔓ℭ𝔴𝔉") diff --git a/GeneralizedAlgebra/AlgPrinting.lean b/GeneralizedAlgebra/AlgPrinting.lean index 4f2aead..5ce5a4f 100644 --- a/GeneralizedAlgebra/AlgPrinting.lean +++ b/GeneralizedAlgebra/AlgPrinting.lean @@ -2,191 +2,33 @@ import GeneralizedAlgebra.signature open Nat open Ty Tm --- open GAT - -mutual -inductive Argument : Type where -| NonDep : List Token → Argument -| Dep : List Token → Argument -inductive Token : Type where -| printArg : Nat → Token -| printVarName : Nat → Token -| printStr : String → Token -| printConstrSplit : Token -| printArrow : Token -| BREAK : Token -end -open Argument Token - -def newVar ( ty : List Token) : StateT (List Argument) Option Nat := do - let vars ← get - let new := NonDep ty - set $ vars++[new] - pure $ List.length vars - -def countDepends : List Argument → Nat -| [] => 0 -| (Dep _)::rest => 1 + countDepends rest -| (NonDep _)::rest => countDepends rest - -def getDepends : List Argument → Nat → Option (Bool × Nat × List Token) -| [] , _ => none -| (Dep ts)::_, 0 => return (true,0,ts) -| (NonDep ts)::_, 0 => return (false,0,ts) -| (Dep _)::rest, succ n => do - let (bit,res,ts) ← getDepends rest n - return (bit,succ res,ts) -| (NonDep _)::rest, succ n => getDepends rest n - -def foldTokens_core (constrSplit : String) (varNames : List String) : Nat → List Argument → List Token → Option String -| succ FUEL, args, printArrow::rest => do - let restStr ← foldTokens_core constrSplit varNames FUEL args rest - return (" → " ++ restStr) -| succ FUEL, args, printConstrSplit::rest => do - let restStr ← foldTokens_core constrSplit varNames FUEL args rest - return (constrSplit ++ restStr) -| succ FUEL, args, (printStr s)::rest => do - let restStr ← foldTokens_core constrSplit varNames FUEL args rest - return (s ++ restStr) -| succ FUEL, args, (printArg n)::rest => do - let (doPrint, index, ts) ← getDepends args n - let printRest ← foldTokens_core constrSplit varNames FUEL args rest - let argType ← foldTokens_core constrSplit varNames FUEL args ts - let varName ← nth index varNames - if doPrint - then return ("(" ++ varName ++ " : " ++ argType ++ ")" ++ printRest) - else return (argType ++ printRest) -| succ FUEL, args, (printVarName n)::rest => do - let (_, index, _) ← getDepends args n - let printRest ← foldTokens_core constrSplit varNames FUEL args rest - let varName ← nth index varNames - return (varName ++ printRest) -| _,_,[] => some "" -| _,_, _ => none - -def foldTokens (constrSplit : String := " × ") (varNames : List String) (args : List Argument):= - foldTokens_core constrSplit varNames 1000 args - -def genVarNames_core (REPR : Nat → String) (varLetter : String) : Nat → List String → Nat → List String -| 0, varNames,_ => varNames -| succ n, varNames,index => genVarNames_core REPR varLetter n (varNames ++ [varLetter ++ REPR index]) (succ index) - -def genVarNames (n : Nat) (starterNames : List String) (varLetter := "X_"): List String := - genVarNames_core (if n < 10 then twoRepr else threeRepr) varLetter (n - List.length starterNames) (List.take n starterNames) 0 - -def pingNth_core : List Argument → Nat → Option (List Argument) -| [],_ => none -| (NonDep ts)::rest,0 => some ((Dep ts)::rest) -| x::rest,succ n => do - let res ← pingNth_core rest n - return (x::res) -| L,_ => some L - -def pingNth (n :Nat) : StateT (List Argument) Option Unit := do - let current ← get - let new ← StateT.lift $ pingNth_core current n - set new - -mutual - def Alg_Con : Con → StateT (List Argument) Option (List Nat × List Token) - | EMPTY => pure $ ([],[printStr "⊤"]) - | EMPTY ▷ UU => do - let theVar ← newVar [printStr "Set"] - pure ([theVar],[printArg theVar]) - | Γ ▷ A => do - let (tel,res) ← Alg_Con Γ - let As ← Alg_Ty A tel - let theVar ← newVar As - pure (tel++[theVar],res ++ [printConstrSplit, printStr "(", printArg theVar, printStr ")"]) - def Alg_Ty : Ty → List Nat → StateT (List Argument) Option (List Token) - | UU,_ => pure [printStr "Set"] - | EL X, tel => Alg_Tm X tel - | PI X Y, tel => do - let Xs ← Alg_Tm X tel - let Xvar ← newVar Xs - let Ys ← Alg_Ty Y (tel++[Xvar]) - pure $ [printArg Xvar, printArrow] ++ Ys - | EQ t t',tel => do - let ts ← Alg_Tm t tel - let t's ← Alg_Tm t' tel - pure $ ts ++ [printStr " = "] ++ t's - - | _,_ => StateT.lift none - def Alg_Tm (t : Tm) (tel : List Nat) : StateT (List Argument) Option (List Token) := - match t,deBruijn t with - | _,some n => do - let glob_n ← StateT.lift (nthBackwards n tel) - pingNth glob_n - pure $ [printVarName glob_n] - | (APP f) [ PAIR (ID _) t ]t,_ => do - let fs ← Alg_Tm f tel - let ts ← Alg_Tm t tel - pure $ fs ++ [printStr " ("] ++ ts ++ [printStr ")"] - | _,_ => none -end - -def Alg (𝔊 : GAT) (recordName : Option String := none) (comp_names : List String := []) : Option String := do - let ((tel,res),vars) ← StateT.run (Alg_Con (GAT.con 𝔊)) ([]) - let vars' ← if recordName.isSome then List.foldlM pingNth_core vars tel else some vars - let compSep := if recordName.isSome then " \n " else " × " - let comp_names := if comp_names.isEmpty then GAT.subnames 𝔊 else comp_names - let varNames := genVarNames (List.length vars') comp_names - let algStr ← foldTokens compSep varNames vars' res - match recordName with - | (some name) => return "record " ++ name ++ "-Alg where\n " ++ algStr - | none => return algStr - -mutual - def DAlg_Con : List String → Con → StateT (List Argument) Option (List Nat × List Token) - | _,EMPTY => pure $ ([],[printStr "⊤"]) - | carrier::_,EMPTY ▷ UU => do - let theVar ← newVar [printStr carrier,printArrow,printStr "Set"] - pure ([theVar],[printArg theVar]) - | alg_comp::Alg_comp,Γ ▷ A => do - let (tel,res) ← DAlg_Con Alg_comp Γ - let As ← DAlg_Ty tel ([printStr alg_comp]::(List.map (λ x => [printStr x]) Alg_comp)) A - let theVar ← newVar As - pure (tel++[theVar],res ++ [printConstrSplit, printStr "(", printArg theVar, printStr ")"]) - | _,_ => none - def DAlg_Ty : List Nat → List (List Token) → Ty → StateT (List Argument) Option (List Token) - | _,carrier::_,UU => pure $ carrier ++ [printArrow,printStr "Set"] - | tel,alg_elt::_,EL X => DAlg_Tm tel alg_elt X - | tel,alg_fn::alg_rest,PI X Y => do - let Atype ← (deBruijn X >>= λ n => nth n alg_rest) <|> some [printStr "?"] - let alpha ← newVar Atype - pingNth alpha - let Xs ← DAlg_Tm tel [printVarName alpha] X - let Xvar ← newVar Xs - let Ys ← DAlg_Ty (tel++[Xvar]) (([printStr "("]++alg_fn++[printStr " ",printVarName alpha,printStr ")"])::alg_rest) Y - pure $ [printArg alpha, printStr " → ",printArg Xvar, printStr " → "] ++ Ys - -- | EQ t t',tel => do - -- let ts ← DAlg_Tm t tel - -- let t's ← DAlg_Tm t' tel - -- pure $ ts ++ [printStr " = "] ++ t's - - | _,_,_ => StateT.lift none - def DAlg_Tm (tel : List Nat) (alg_elt : List Token) (t : Tm) : StateT (List Argument) Option (List Token) := - match t,deBruijn t with - | _,some n => do - let glob_n ← StateT.lift (nthBackwards n tel) - pingNth glob_n - pure $ [printVarName glob_n,printStr " "]++alg_elt - -- | (APP f) [ PAIR (ID _) t ]t,_ => do - -- let fs ← DAlg_Tm f tel - -- let ts ← DAlg_Tm t tel - -- pure $ fs ++ [printStr " "] ++ ts - | _,_ => none -end - -def DAlg (𝔊 : GAT) (recordName : Option String := none) (comp_names : List String := []) (Alg_comp_names : List String := []) : Option String := do - let Alg_comp_names := if Alg_comp_names.isEmpty then 𝔊.topnames else Alg_comp_names - let Alg_comp := genVarNames (len 𝔊.con) Alg_comp_names "Y_" - let ((tel,res),vars) ← StateT.run (DAlg_Con (List.reverse Alg_comp) 𝔊.con) ([]) - let vars' ← if recordName.isSome then List.foldlM pingNth_core vars tel else some vars - let compSep := if recordName.isSome then "\n " else " × " - let varNames := genVarNames (List.length vars') comp_names - let algStr ← foldTokens compSep varNames vars' res - match recordName with - | (some name) => return "record " ++ name ++ "-DAlg " ++ collapse Alg_comp ++ " where\n " ++ algStr - | none => return algStr +instance AlgStr : indData where + Con_D := λ _ => String + Ty_D := λ _ _ _ => String + Tm_D := λ _ _ _ _ _ => String + nil_D := "⋄" + cons_D := λ 𝔊 𝔊s A As => 𝔊s ++ " × " ++ As + UU_D := λ _ _ => "Set" + EL_D := λ _ 𝔊s _ Xs => 𝔊s ++ "-" ++ Xs + PI_D := λ _ _ _ _ _ _ => "w" + EQ_D := λ _ _ _ _ _ _ _ _ => "v" + VAR0_D := λ _ 𝔊s _ As A's => "(" ++ As ++ "|" ++ A's ++ ")" + VARSUCC_D := λ _ _ _ _ _ _ _ _ _ => "t" + APP_D := λ _ _ _ _ _ _ _ _ _ _ _ => "s" + TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r" + +instance Alg : indData where + Con_D := λ _ => Type 1 + Ty_D := λ _ Γ _ => Γ → Type 1 + Tm_D := λ _ Γ _ A _ => (γ : Γ) → A γ + nil_D := PUnit + cons_D := λ 𝔊 Γ _ A => Sigma (λ γ => A γ) + UU_D := λ _ _ _ => Type + EL_D := λ _ 𝔊s _ Xs γ => Xs γ + -- PI_D := λ _ _ _ _ _ _ => "w" + -- EQ_D := λ _ _ _ _ _ _ _ _ => "v" + -- VAR0_D := λ _ 𝔊s _ As A's => "(" ++ As ++ "|" ++ A's ++ ")" + -- VARSUCC_D := λ _ _ _ _ _ _ _ _ _ => "t" + -- APP_D := λ _ _ _ _ _ _ _ _ _ _ _ => "s" + -- TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r" diff --git a/GeneralizedAlgebra/nouGAT.lean b/GeneralizedAlgebra/nouGAT.lean index bf76edd..11c6a78 100644 --- a/GeneralizedAlgebra/nouGAT.lean +++ b/GeneralizedAlgebra/nouGAT.lean @@ -105,17 +105,15 @@ def varTelLookup {VV : varStruct} (TT : varTel VV) (key : String) : MetaM (Expr let args ← (VV.getArgs key) <|> return [] return (T,args) --- def varTelExtend {VV : varStruct} (TT : varTel VV) (newArg : metaArg) (ctx : Expr) (newCtx : Expr) : varTel VV := --- ⟨ λ s => --- if argMatch s newArg --- then mkAppM ``V0 #[ ctx , extractMetaTy newArg ] --- else do --- let (old,_) ← varTelLookup TT s --- let ID ← mkAppM ``ID #[newCtx] --- let p ← mkAppM ``PROJ1 #[ID] --- mkAppM ``SUBST_Tm #[ p , old], --- TT.args ++ [newArg], --- ⟩ +def varTelExtend {VV : varStruct} (TT : varTel VV) (newArg : metaArg) (ctx : Expr) (newCtx : Expr) : varTel VV := +⟨ λ s => + if argMatch s newArg + then mkAppM ``VAR #[ mkNatLit 0 ] + else do + let (old,_) ← varTelLookup TT s + mkAppM ``WkTm #[ old ], + TT.args ++ [newArg], +⟩ partial def splitArgList (message : String) : List metaArg → MetaM (metaArg × List metaArg) | [] => throwError message @@ -182,16 +180,16 @@ partial def elabGATTy {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Synta let t ← elabClosedGATTm ctx TT x let T ← mkAppM ``EL #[t] return (TT, T, T) --- | `(gat_ty| $T:gat_arg ⇒ $T':gat_ty) => do --- let argT ← elabGATArg ctx TT T --- let domain := extractMetaTy argT --- let elDomain ← mkAppM ``EL #[domain] --- let elT ← argEl argT --- let newCtx ← mkAppM ``EXTEND #[ctx,elDomain] --- let newTT := varTelExtend TT elT ctx newCtx --- let (newnewTT,codomain,resT) ← elabGATTy newCtx newTT T' --- let result ← mkAppM ``PI #[domain,codomain] --- return (newnewTT,result,resT) +| `(gat_ty| $T:gat_arg ⇒ $T':gat_ty) => do + let argT ← elabGATArg ctx TT T + let domain := extractMetaTy argT + let elDomain ← mkAppM ``EL #[domain] + let elT ← argEl argT + let newCtx ← mkAppM ``EXTEND #[ctx,elDomain] + let newTT := varTelExtend TT elT ctx newCtx + let (newnewTT,codomain,resT) ← elabGATTy newCtx newTT T' + let result ← mkAppM ``PI #[domain,codomain] + return (newnewTT,result,resT) | `(gat_ty| $t1:gat_tm ≡ $t2:gat_tm) => do let tt1 ← elabClosedGATTm ctx TT t1 let tt2 ← elabClosedGATTm ctx TT t2 diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index cd616fa..420cee8 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -207,14 +207,18 @@ theorem UU_stable : UU = WkTy UU := Eq.refl _ -- def extractGoodVar {Γ : Con}{A : Ty}{n : Nat} : goodTm Γ A (VAR n) → -- ∃ (h : n < Γ.length), A = WknTy Γ n h := sorry +universe u v w structure indData where - (Con_D : Con → Type) - (Ty_D : (Γ : Con) → Con_D Γ → Ty → Type) - (Tm_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → Ty_D Γ Γ_D A → Tm → Type) + (Con_D : Con → Type u) + (Ty_D : (Γ : Con) → Con_D Γ → Ty → Type v) + (Tm_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → Ty_D Γ Γ_D A → Tm → Type w) (nil_D : Con_D []) (cons_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Con_D (A::Γ)) - (WkTy_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A)) + -- (WkTy_D : (Γ : Con) → (Γ_D : Con_D Γ) → + -- (A : Ty) → (A_D : Ty_D Γ Γ_D A) → + -- (A' : Ty) → (A'_D : Ty_D Γ Γ_D A') → + -- Ty_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A)) (UU_D : (Γ : Con) → (Γ_D : Con_D Γ) → Ty_D Γ Γ_D UU) (EL_D : (Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X → @@ -237,9 +241,11 @@ structure indData where Tm_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A) A'_D (VAR 0) ) (VARSUCC_D : (Γ : Con) → (Γ_D : Con_D Γ) → - (A : Ty) → (A_D : Ty_D Γ Γ_D A) → (t : Tm) → - (B : Ty) → (B_D : Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) B) → - Tm_D Γ Γ_D A A_D t → Tm_D (A::Γ) (cons_D Γ Γ_D A A_D) B B_D (WkTm t)) + (A : Ty) → (A_D : Ty_D Γ Γ_D A) → + (t : Tm) → Tm_D Γ Γ_D A A_D t → + (A' : Ty) → (A'_D : Ty_D Γ Γ_D A') → + (WkA_D : Ty_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A)) → + Tm_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A) WkA_D (WkTm t)) (APP_D :(Γ : Con) → (Γ_D : Con_D Γ) → (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) → (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) → diff --git a/GeneralizedAlgebra/signatures/bipointed.lean b/GeneralizedAlgebra/signatures/bipointed.lean index 3b7c87d..6806132 100644 --- a/GeneralizedAlgebra/signatures/bipointed.lean +++ b/GeneralizedAlgebra/signatures/bipointed.lean @@ -1,19 +1,8 @@ import GeneralizedAlgebra.signatures.pointed +#check indData.VARSUCC_D def 𝔅 : GAT := ⟨ ⦃ X : U, x : X, x' : X ⦄, - - by - intro P - apply P.cons_D - apply P.EL_D - rw [WkTm] - have helper := P.VARSUCC_D [Ty.EL (Tm.VAR 0), Ty.UU] --[Ty.UU] (P.cons_D _ P.nil_D _ (P.UU_D _ _)) (Ty.EL (Tm.VAR 0)) (P.EL_D _ _ _ (P.VAR0_D _ _ _ _ _)) (Tm.VAR 0) Ty.UU (P.UU_D _ _) -- (Ty.EL (Tm.VAR 1)) - -- rw [WkTm] at helper - apply helper - have helper' := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) - rw [WkTy] at helper' - apply helper' - - + λ P => P.cons_D _ (𝔓.elim P) _ (P.EL_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) (Tm.VAR 0) (P.VAR0_D _ _ _ _ _) _ _ _)) ⟩ +-- diff --git a/GeneralizedAlgebra/signatures/nat.lean b/GeneralizedAlgebra/signatures/nat.lean index b265e4e..63f8b8a 100644 --- a/GeneralizedAlgebra/signatures/nat.lean +++ b/GeneralizedAlgebra/signatures/nat.lean @@ -1,7 +1,10 @@ -import GeneralizedAlgebra.nouGAT +import GeneralizedAlgebra.signatures.pointed -def 𝔑 : GAT := ⦃ +def 𝔑 : GAT := ⟨ +⦃ Nat : U, zero : Nat, succ : Nat ⇒ Nat -⦄ +⦄, +λ P => P.cons_D _ (𝔓.elim P) _ (P.PI_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) (Tm.VAR 0) (P.VAR0_D _ _ _ _ _) _ _ _) _ (P.EL_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VAR0_D _ _ _ _ _) _ _ _) _ _ _))) +⟩ diff --git a/GeneralizedAlgebra/signatures/pointed.lean b/GeneralizedAlgebra/signatures/pointed.lean index e7c129c..1cfee01 100644 --- a/GeneralizedAlgebra/signatures/pointed.lean +++ b/GeneralizedAlgebra/signatures/pointed.lean @@ -1,29 +1,30 @@ -import GeneralizedAlgebra.nouGAT +import GeneralizedAlgebra.signatures.set -def pointedLemma (P : indData) : - P.Tm_D - [Ty.UU] - (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) - (Ty.EL (Tm.VAR 0)) - (P.EL_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) (Tm.VAR 0) (P.VAR0_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D) (P.UU_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D))))) - (Tm.VAR 0) - := by +-- def pointedLemma (P : indData) : +-- P.Tm_D +-- [Ty.UU] +-- (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) +-- (Ty.EL (Tm.VAR 0)) +-- (P.EL_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) (Tm.VAR 0) (P.VAR0_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D) (P.UU_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D))))) +-- (Tm.VAR 0) +-- := by - have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) (P.UU_D _ _) - -- rw [WkTy] at helper - sorry +-- have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) (P.UU_D _ _) +-- -- rw [WkTy] at helper +-- sorry def 𝔓 : GAT := ⟨ ⦃ X : U, x : X ⦄, - - by - intro P - apply P.cons_D - apply P.EL_D - have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) - rw [WkTy] at helper - apply helper + λ P => P.cons_D _ (𝔖𝔢𝔱.elim P) _ (P.EL_D _ _ _ (P.VAR0_D _ _ _ _ _)) + -- by + -- intro P + -- apply P.cons_D + -- apply P.EL_D + -- have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) + -- rw [WkTy] at helper + -- apply helper ⟩ +-- #reduce 𝔓.elim From a3cc3ec3977111292da3fcebe13b99fac257882a Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Mon, 23 Jun 2025 19:18:26 +0000 Subject: [PATCH 09/11] Implemented elim for quiver --- GeneralizedAlgebra/signatures/quiver.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/GeneralizedAlgebra/signatures/quiver.lean b/GeneralizedAlgebra/signatures/quiver.lean index 36b862d..cbfa2b9 100644 --- a/GeneralizedAlgebra/signatures/quiver.lean +++ b/GeneralizedAlgebra/signatures/quiver.lean @@ -1,6 +1,8 @@ -import GeneralizedAlgebra.nouGAT +import GeneralizedAlgebra.signatures.set -def 𝔔𝔲𝔦𝔳 : GAT := ⦃ +def 𝔔𝔲𝔦𝔳 : GAT := ⟨ ⦃ V : U, E : V ⇒ V ⇒ U -⦄ +⦄, +λ P => P.cons_D _ (𝔖𝔢𝔱.elim P) _ (P.PI_D _ _ _ (P.VAR0_D _ _ _ _ _) _ (P.PI_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VAR0_D _ _ _ _ _) _ _ _) _ (P.UU_D _ _))) +⟩ From 81e7c11358721ffbe200f9c30a9a3e3d75a74b54 Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Mon, 23 Jun 2025 19:19:23 +0000 Subject: [PATCH 10/11] Added ConPrinting --- GeneralizedAlgebra/AlgPrinting.lean | 20 ++++--- GeneralizedAlgebra/ConPrinting.lean | 82 +++++++++++++++++++---------- 2 files changed, 65 insertions(+), 37 deletions(-) diff --git a/GeneralizedAlgebra/AlgPrinting.lean b/GeneralizedAlgebra/AlgPrinting.lean index 5ce5a4f..1c7824f 100644 --- a/GeneralizedAlgebra/AlgPrinting.lean +++ b/GeneralizedAlgebra/AlgPrinting.lean @@ -3,6 +3,10 @@ import GeneralizedAlgebra.signature open Nat open Ty Tm + + + + instance AlgStr : indData where Con_D := λ _ => String Ty_D := λ _ _ _ => String @@ -18,14 +22,14 @@ instance AlgStr : indData where APP_D := λ _ _ _ _ _ _ _ _ _ _ _ => "s" TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r" -instance Alg : indData where - Con_D := λ _ => Type 1 - Ty_D := λ _ Γ _ => Γ → Type 1 - Tm_D := λ _ Γ _ A _ => (γ : Γ) → A γ - nil_D := PUnit - cons_D := λ 𝔊 Γ _ A => Sigma (λ γ => A γ) - UU_D := λ _ _ _ => Type - EL_D := λ _ 𝔊s _ Xs γ => Xs γ +-- instance Alg : indData where +-- Con_D := λ _ => Type 1 +-- Ty_D := λ _ Γ _ => Γ → Type 1 +-- Tm_D := λ _ Γ _ A _ => (γ : Γ) → A γ +-- nil_D := PUnit +-- cons_D := λ 𝔊 Γ _ A => Sigma (λ γ => A γ) +-- UU_D := λ _ _ _ => Type +-- EL_D := λ _ 𝔊s _ Xs γ => Xs γ -- PI_D := λ _ _ _ _ _ _ => "w" -- EQ_D := λ _ _ _ _ _ _ _ _ => "v" -- VAR0_D := λ _ 𝔊s _ As A's => "(" ++ As ++ "|" ++ A's ++ ")" diff --git a/GeneralizedAlgebra/ConPrinting.lean b/GeneralizedAlgebra/ConPrinting.lean index 04d8fb9..6ba08f8 100644 --- a/GeneralizedAlgebra/ConPrinting.lean +++ b/GeneralizedAlgebra/ConPrinting.lean @@ -1,36 +1,60 @@ import GeneralizedAlgebra.signature open Nat -open Con Subst Ty Tm +open Ty Tm -mutual - def Con_toString : Con → String - | EMPTY => "⋄" - | Γ ▷ A => (Con_toString Γ) ++ " ▷ " ++ (Ty_toString A) - def Ty_toString : Ty → String - | UU => "U" - | EL X => "El " ++ paren (Tm_toString X) - | PI X UU => "Π " ++ paren (Tm_toString X) ++ " U" - | PI X Y => "Π " ++ paren (Tm_toString X) ++ " " ++ paren (Ty_toString Y) - | EQ t t' => "Eq " ++ paren (Tm_toString t) ++ " " ++ paren (Tm_toString t') - | SUBST_Ty σ T => (Ty_toString T) ++ " [ " ++ (Subst_toString σ) ++ " ]T" +-- mutual +-- def Con_toString : Con → String +-- | EMPTY => "⋄" +-- | Γ ▷ A => (Con_toString Γ) ++ " ▷ " ++ (Ty_toString A) +-- def Ty_toString : Ty → String +-- | UU => "U" +-- | EL X => "El " ++ paren (Tm_toString X) +-- | PI X UU => "Π " ++ paren (Tm_toString X) ++ " U" +-- | PI X Y => "Π " ++ paren (Tm_toString X) ++ " " ++ paren (Ty_toString Y) +-- | EQ t t' => "Eq " ++ paren (Tm_toString t) ++ " " ++ paren (Tm_toString t') +-- | SUBST_Ty σ T => (Ty_toString T) ++ " [ " ++ (Subst_toString σ) ++ " ]T" - def Tm_toString (theTerm : Tm) : String := - match deBruijn theTerm with - | some n => Nat.repr n - | _ => match theTerm with - | (APP f) [ PAIR (ID _) t ]t => (Tm_toString f) ++ " @ " ++ paren (Tm_toString t) - | PROJ2 σ => "π₂ " ++ (Subst_toString σ) - | APP f => "App " ++ paren (Tm_toString f) - | t [ σ ]t => paren (Tm_toString t) ++ " [ " ++ (Subst_toString σ) ++ " ]t " - def Subst_toString : Subst → String - | PROJ1 (ID _) => "wk" - | PROJ1 σ => "π₁ " ++ (Subst_toString σ) - | PAIR σ t => (Subst_toString σ) ++ " , " ++ paren (Tm_toString t) - | EPSILON _ => "ε" - | COMP σ τ => (Subst_toString σ) ++ " ∘ " ++ (Subst_toString τ) - | (ID _) => "id" -end +-- def Tm_toString (theTerm : Tm) : String := +-- match deBruijn theTerm with +-- | some n => Nat.repr n +-- | _ => match theTerm with +-- | (APP f) [ PAIR (ID _) t ]t => (Tm_toString f) ++ " @ " ++ paren (Tm_toString t) +-- | PROJ2 σ => "π₂ " ++ (Subst_toString σ) +-- | APP f => "App " ++ paren (Tm_toString f) +-- | t [ σ ]t => paren (Tm_toString t) ++ " [ " ++ (Subst_toString σ) ++ " ]t " +-- def Subst_toString : Subst → String +-- | PROJ1 (ID _) => "wk" +-- | PROJ1 σ => "π₁ " ++ (Subst_toString σ) +-- | PAIR σ t => (Subst_toString σ) ++ " , " ++ paren (Tm_toString t) +-- | EPSILON _ => "ε" +-- | COMP σ τ => (Subst_toString σ) ++ " ∘ " ++ (Subst_toString τ) +-- | (ID _) => "id" +-- end + +def mkParen (s:String) : String := + if s.isNat then s else + if s="U" then s else "("++s++")" + +def wkStr (s : String) : String := +match s.toNat? with +| (some n) => Nat.repr (succ n) +| _ => s ++ "[wk]" + +instance ConStr_method : indData where + Con_D := λ _ => String + Ty_D := λ _ _ _ => String + Tm_D := λ _ _ _ _ _ => String + nil_D := "⋄" + cons_D := λ _ 𝔊s _ As => 𝔊s ++ " ▷ " ++ As + UU_D := λ _ _ => "U" + EL_D := λ _ _ _ Xs => "El " ++ (mkParen Xs) + PI_D := λ _ _ _ Xs _ Ys => "Π " ++ (mkParen Xs) ++ " " ++ (mkParen Ys) + EQ_D := λ _ _ _ Xs _ ss _ ts => "Eq " ++ Xs ++ " " ++ ss ++ " " ++ ts + VAR0_D := λ _ _ _ _ _ => "0" + VARSUCC_D := λ _ _ _ _ _ ts _ _ _ => wkStr ts + APP_D := λ _ _ _ _ _ _ _ fs _ xs _ => fs ++ " @ " ++ xs + TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r" instance GATRepr : Repr GAT := -⟨ λ 𝔊 _ => Con_toString 𝔊.con⟩ +⟨ λ 𝔊 _ => 𝔊.elim ConStr_method ⟩ From 102174c314f7f5af32cd9d28792373f3c3d3d18f Mon Sep 17 00:00:00 2001 From: Jacob Neumann Date: Mon, 23 Jun 2025 19:19:53 +0000 Subject: [PATCH 11/11] Work towards refl_quiver; encountered issue with application nouGAT parsing --- GeneralizedAlgebra.lean | 6 ++--- GeneralizedAlgebra/nouGAT.lean | 17 ++++++------- GeneralizedAlgebra/signature.lean | 24 +++++++++++++++++++ .../signatures/refl_quiver.lean | 18 ++++++++++---- 4 files changed, 50 insertions(+), 15 deletions(-) diff --git a/GeneralizedAlgebra.lean b/GeneralizedAlgebra.lean index 699283f..a1c9d55 100644 --- a/GeneralizedAlgebra.lean +++ b/GeneralizedAlgebra.lean @@ -1,5 +1,5 @@ import GeneralizedAlgebra.AlgPrinting --- import GeneralizedAlgebra.ConPrinting +import GeneralizedAlgebra.ConPrinting import GeneralizedAlgebra.signatures.set import GeneralizedAlgebra.signatures.pointed @@ -21,8 +21,8 @@ import GeneralizedAlgebra.signatures.nat /- ## Basic structures -/ - -#eval 𝔓.elim AlgStr +#eval 𝔑 +#eval 𝔑.elim AlgStr -- Sets -- #eval 𝔖𝔢𝔱 -- #eval Alg 𝔖𝔢𝔱 diff --git a/GeneralizedAlgebra/nouGAT.lean b/GeneralizedAlgebra/nouGAT.lean index 11c6a78..9afafc1 100644 --- a/GeneralizedAlgebra/nouGAT.lean +++ b/GeneralizedAlgebra/nouGAT.lean @@ -129,13 +129,14 @@ partial def failIfExplicitArgs (message : String) : List metaArg → MetaM Unit partial def elabGATTm {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Syntax → MetaM (Expr × List metaArg) | `(gat_tm| ( $g:gat_tm ) ) => elabGATTm ctx TT g --- | `(gat_tm| $g1:gat_tm $g2:gat_tm ) => do --- let (t1,args1) ← elabGATTm ctx TT g1 --- let (A,args1') ← splitArgList "Too many args #0" args1 +| `(gat_tm| $g1:gat_tm $g2:gat_tm ) => do + let (t1,args1) ← elabGATTm ctx TT g1 + let (A,args1') ← splitArgList "Too many args #0" args1 + let domain := extractMetaTy A -- -- TODO: Check the type of A against the type of t2 --- let Appt1 ← mkAppM ``APP #[t1] --- let (t2,args2)← elabGATTm ctx TT g2 --- failIfExplicitArgs "Insufficient Args #0" args2 + -- let Appt1 ← mkAppM ``APP #[t1] + let (t2,args2)← elabGATTm ctx TT g2 + failIfExplicitArgs "Insufficient Args #0" args2 -- -- let actualT2 ← reduce t2 -- -- let expectedT2 ← reduce (extractMetaTy A) -- -- let tyMatch ← isDefEq actualT2 expectedT2 @@ -144,8 +145,8 @@ partial def elabGATTm {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Synta -- -- else do -- let ID ← mkAppM ``ID #[ctx] -- let substt2 ← mkAppM ``PAIR #[ID,t2] --- let resT ← mkAppM ``SUBST_Tm #[substt2,Appt1] --- return (resT,args1') + let resT ← mkAppM ``APP #[t1,domain,t1,t2] + return (resT,args1') | `(gat_tm| $i:ident ) => do varTelLookup TT i.getId.toString -- let args ← vars.getArgs i.getI diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean index 420cee8..2b7e2cd 100644 --- a/GeneralizedAlgebra/signature.lean +++ b/GeneralizedAlgebra/signature.lean @@ -277,6 +277,30 @@ def getName : Arg → Option String | Expl i _ => some i | Anon _ => none +mutual +def Tmrepr : Tm → String +| APP X Y f t => "APP (" ++ (Tmrepr X) ++ ") (" ++ (Tyrepr Y) ++ ") (" ++ (Tmrepr f) ++ ") (" ++ (Tmrepr t) ++ ")" +| VAR n => Nat.repr n +| TRANSP X s s' Y eq t => "transp " ++ (Tmrepr eq) ++ " " ++ (Tmrepr t) + +def Tyrepr : Ty → String +| UU => "U" +| EQ X s t => "Eq " ++ (Tmrepr X) ++ " " ++ (Tmrepr s) ++ " " ++ (Tmrepr t) +| EL X => "El (" ++ (Tmrepr X) ++ ")" +| PI X Y => "Π (" ++ (Tmrepr X) ++ ") (" ++ (Tyrepr Y) ++ ")" +end + +def Argrepr : Arg → String +| Impl i T => "iArg(" ++ i ++ "," ++ Tyrepr T ++ ")" +| Expl i T => "eArg(" ++ i ++ "," ++ Tyrepr T ++ ")" +| Anon T => "aArg(" ++ Tyrepr T ++ ")" + +instance : Repr Tm where + reprPrec := λ t _ => Tmrepr t +instance : Repr Ty where + reprPrec := λ t _ => Tyrepr t +instance : Repr Arg where + reprPrec := λ A _ => Argrepr A structure GATdata where (con : Con) diff --git a/GeneralizedAlgebra/signatures/refl_quiver.lean b/GeneralizedAlgebra/signatures/refl_quiver.lean index 4d97944..6a29faa 100644 --- a/GeneralizedAlgebra/signatures/refl_quiver.lean +++ b/GeneralizedAlgebra/signatures/refl_quiver.lean @@ -1,7 +1,17 @@ -import GeneralizedAlgebra.nouGAT +import GeneralizedAlgebra.signatures.quiver -def 𝔯𝔔𝔲𝔦𝔳 : GAT := ⦃ +-- def 𝔯𝔔𝔲𝔦𝔳 : GAT := ⟨ ⦃ +-- V : U, +-- E : V ⇒ V ⇒ U, +-- r : (v : V) ⇒ E v v +-- ⦄, +-- λ P => _ +-- ⟩ + +def foo := ⦃ V : U, - E : V ⇒ V ⇒ U, - r : (v : V) ⇒ E v v + E : V ⇒ U, + r : (v : V) ⇒ E v ⦄ + +#eval foo.telescopes