From b91c793944c20338742fc067b83989d01f391430 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Sun, 10 Dec 2023 12:02:12 +0700 Subject: [PATCH] some macro tricks & bugfix for #success/#failure --- GroundZero/Exercises/Chap5.lean | 2 +- GroundZero/HITs/Merely.lean | 49 +++++++++++++++--------------- GroundZero/HITs/Trunc.lean | 22 +++++++------- GroundZero/Meta/Notation.lean | 10 +++--- GroundZero/Meta/Trust.lean | 8 ++--- GroundZero/Theorems/Functions.lean | 15 ++++----- GroundZero/Types/CellComplex.lean | 12 ++++---- 7 files changed, 58 insertions(+), 60 deletions(-) diff --git a/GroundZero/Exercises/Chap5.lean b/GroundZero/Exercises/Chap5.lean index ff6afcb..8cd0f8a 100644 --- a/GroundZero/Exercises/Chap5.lean +++ b/GroundZero/Exercises/Chap5.lean @@ -45,7 +45,7 @@ namespace «5.3» hott definition ez₂ : E := e hott definition es₂ : ℕ → E → E := λ n _, e - #failure @es₁ E ≡ @es₂ E e : ℕ → E + #failure @es₁ E ≡ @es₂ E e : ℕ → E → E hott definition f : ℕ → E := λ _, e diff --git a/GroundZero/HITs/Merely.lean b/GroundZero/HITs/Merely.lean index 193cfc1..38cf7a3 100644 --- a/GroundZero/HITs/Merely.lean +++ b/GroundZero/HITs/Merely.lean @@ -21,62 +21,64 @@ universe u v w * https://arxiv.org/pdf/1512.02274 -/ -def Merely (A : Type u) := +hott definition Merely (A : Type u) := Colimit (Generalized.rep A) (Generalized.dep A) notation "∥" A "∥" => Merely A namespace Merely - def elem {A : Type u} (x : A) : ∥A∥ := + hott definition elem {A : Type u} (x : A) : ∥A∥ := Colimit.inclusion 0 x + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/absolute.20value + macro:max atomic("|" noWs) x:term noWs "|" : term => `(Merely.elem $x) + section variable {A : Type u} {B : ∥A∥ → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, prop (B x)) - hott def resp : Π (n : ℕ) (x : Generalized.rep A n), B (Colimit.incl x) + hott definition resp : Π (n : ℕ) (x : Generalized.rep A n), B (Colimit.incl x) | Nat.zero, x => elemπ x | Nat.succ n, w => @Generalized.ind _ (λ x, B (Colimit.inclusion (n + 1) x)) (λ x, transport B (Colimit.glue x)⁻¹ (resp n x)) (λ a b, uniqπ _ _ _) w - hott def ind : Π x, B x := - begin intro x; fapply Colimit.ind; apply resp elemπ uniqπ; intros; apply uniqπ end + hott definition ind : Π x, B x := + Colimit.ind (resp elemπ uniqπ) (λ _ _, uniqπ _ _ _) end attribute [eliminator] ind - hott def rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) : ∥A∥ → B := + hott definition rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) : ∥A∥ → B := ind f (λ _, H) - hott def weakUniq {A : Type u} (x y : A) : @Types.Id ∥A∥ (elem x) (elem y) := + hott lemma weakUniq {A : Type u} (x y : A) : @Id ∥A∥ |x| |y| := begin transitivity; { symmetry; apply Colimit.glue }; symmetry; transitivity; { symmetry; apply Colimit.glue }; apply ap; apply Generalized.glue end - hott def incl {A : Type u} {n : ℕ} := + hott definition incl {A : Type u} {n : ℕ} := @Colimit.incl (Generalized.rep A) (Generalized.dep A) n - hott def glue {A : Type u} {n : ℕ} {x : Generalized.rep A n} : + hott definition glue {A : Type u} {n : ℕ} {x : Generalized.rep A n} : incl (Generalized.dep A n x) = incl x := Colimit.glue x - hott def exactNth {A : Type u} (a : A) : Π n, Generalized.rep A n + hott definition exactNth {A : Type u} (a : A) : Π n, Generalized.rep A n | Nat.zero => a | Nat.succ n => Generalized.dep A n (exactNth a n) - hott def nthGlue {A : Type u} (a : A) : Π n, incl (exactNth a n) = @incl A 0 a + hott definition nthGlue {A : Type u} (a : A) : Π n, incl (exactNth a n) = @incl A 0 a | Nat.zero => idp _ | Nat.succ n => Colimit.glue (exactNth a n) ⬝ nthGlue a n - hott lemma inclUniq {A : Type u} {n : ℕ} (a b : Generalized.rep A n) : incl a = incl b := + hott lemma inclUniq {A : Type u} {n : ℕ} (a b : Generalized.rep A n) := calc incl a = incl (Generalized.dep A n a) : glue⁻¹ ... = incl (Generalized.dep A n b) : ap incl (Generalized.glue a b) ... = incl b : glue - hott lemma inclZeroEqIncl {A : Type u} {n : ℕ} (x : A) - (y : Generalized.rep A n) : @incl A 0 x = incl y := + hott lemma inclZeroEqIncl {A : Type u} {n : ℕ} (x : A) (y : Generalized.rep A n) := calc @incl A 0 x = incl (exactNth x n) : (nthGlue x n)⁻¹ ... = incl y : inclUniq (exactNth x n) y @@ -88,7 +90,7 @@ namespace Merely hott lemma congClose {A : Type u} {n : ℕ} {a b : Generalized.rep A n} (p : a = b) : glue⁻¹ ⬝ ap incl (ap (Generalized.dep A n) p) ⬝ glue = ap incl p := begin - induction p; transitivity; { symmetry; apply Id.assoc }; + induction p; transitivity; symmetry; apply Id.assoc; apply Equiv.rewriteComp; symmetry; apply Id.rid end @@ -125,27 +127,26 @@ namespace Merely hott corollary hprop {A : Type u} : is-(−1)-type ∥A∥ := minusOneEqvProp.left uniq - hott def lift {A : Type u} {B : Type v} (f : A → B) : ∥A∥ → ∥B∥ := + hott definition lift {A : Type u} {B : Type v} (f : A → B) : ∥A∥ → ∥B∥ := rec uniq (elem ∘ f) - hott def rec₂ {A : Type u} {B : Type v} {γ : Type w} (H : prop γ) + hott definition rec₂ {A : Type u} {B : Type v} {γ : Type w} (H : prop γ) (φ : A → B → γ) : ∥A∥ → ∥B∥ → γ := @rec A (∥B∥ → γ) (implProp H) (rec H ∘ φ) - hott def lift₂ {A : Type u} {B : Type v} {γ : Type w} + hott definition lift₂ {A : Type u} {B : Type v} {γ : Type w} (φ : A → B → γ) : ∥A∥ → ∥B∥ → ∥γ∥ := - rec₂ uniq (λ a b, elem (φ a b)) + rec₂ uniq (λ a b, |φ a b|) - hott def equivIffTrunc {A B : Type u} - (f : A → B) (g : B → A) : ∥A∥ ≃ ∥B∥ := + hott theorem equivIffTrunc {A B : Type u} (f : A → B) (g : B → A) : ∥A∥ ≃ ∥B∥ := ⟨lift f, (⟨lift g, λ _, uniq _ _⟩, ⟨lift g, λ _, uniq _ _⟩)⟩ - def diag {A : Type u} (a : A) : A × A := ⟨a, a⟩ + hott definition diag {A : Type u} (a : A) : A × A := ⟨a, a⟩ - hott def productIdentity {A : Type u} : ∥A∥ ≃ ∥A × A∥ := + hott corollary productIdentity {A : Type u} : ∥A∥ ≃ ∥A × A∥ := equivIffTrunc diag Prod.fst - hott def uninhabitedImpliesTruncUninhabited {A : Type u} : ¬A → ¬∥A∥ := + hott corollary uninhabitedImpliesTruncUninhabited {A : Type u} : ¬A → ¬∥A∥ := rec Structures.emptyIsProp end Merely diff --git a/GroundZero/HITs/Trunc.lean b/GroundZero/HITs/Trunc.lean index 4824e50..712ac57 100644 --- a/GroundZero/HITs/Trunc.lean +++ b/GroundZero/HITs/Trunc.lean @@ -33,8 +33,7 @@ namespace Trunc | −1 => Merely.hprop | succ (succ n) => λ _ _, propIsNType (λ _ _, trustCoherence) n - @[eliminator] def ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x)) - (uniqπ : Π x, is-n-type (B x)) : Π x, B x := + @[eliminator] def ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, is-n-type (B x)) : Π x, B x := match n with | −2 => λ x, (uniqπ x).1 | −1 => Merely.ind elemπ (λ _, minusOneEqvProp.forward (uniqπ _)) @@ -50,10 +49,11 @@ namespace Trunc macro:max "∥" A:term "∥" n:subscript : term => do `(Trunc $(← Meta.Notation.parseSubscript n) $A) - macro "|" x:term "|" n:subscript : term => do - `(@Trunc.elem _ $(← Meta.Notation.parseSubscript n) $x) + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/absolute.20value + macro:max atomic("|" noWs) x:term noWs "|" n:subscript : term => + do `(@Trunc.elem _ $(← Meta.Notation.parseSubscript n) $x) - hott lemma indβrule {B : ∥A∥ₙ → Type v} (elemπ : Π x, B (elem x)) + hott lemma indβrule {B : ∥A∥ₙ → Type v} (elemπ : Π x, B |x|ₙ) (uniqπ : Π x, is-n-type (B x)) (x : A) : ind elemπ uniqπ (elem x) = elemπ x := begin match n with | −2 => _ | −1 => _ | succ (succ n) => _; @@ -63,13 +63,13 @@ namespace Trunc section variable {B : Type v} (elemπ : A → B) (uniqπ : is-n-type B) - hott def rec : ∥A∥ₙ → B := @ind A n (λ _, B) elemπ (λ _, uniqπ) + hott definition rec : ∥A∥ₙ → B := @ind A n (λ _, B) elemπ (λ _, uniqπ) hott corollary recβrule (x : A) : rec elemπ uniqπ (elem x) = elemπ x := by apply indβrule end - hott def elemClose {B : Type v} (G : is-n-type B) + hott definition elemClose {B : Type v} (G : is-n-type B) (f g : ∥A∥ₙ → B) (H : f ∘ elem = g ∘ elem) : f = g := begin apply Theorems.funext; fapply ind <;> intro x; @@ -77,7 +77,7 @@ namespace Trunc { apply hlevel.cumulative; assumption } end - hott def nthTrunc (H : is-n-type A) : A ≃ ∥A∥ₙ := + hott definition nthTrunc (H : is-n-type A) : A ≃ ∥A∥ₙ := begin existsi elem; apply Prod.mk <;> existsi rec id H; { intro; apply recβrule; }; @@ -85,13 +85,13 @@ namespace Trunc apply Theorems.funext; intro; apply ap elem; apply recβrule; } end - hott def setEquiv {A : Type u} (H : hset A) : A ≃ ∥A∥₀ := + hott definition setEquiv {A : Type u} (H : hset A) : A ≃ ∥A∥₀ := begin apply nthTrunc; apply zeroEqvSet.left; assumption end - hott def ap {A : Type u} {B : Type v} {n : ℕ₋₂} (f : A → B) : ∥A∥ₙ → ∥B∥ₙ := + hott definition ap {A : Type u} {B : Type v} {n : ℕ₋₂} (f : A → B) : ∥A∥ₙ → ∥B∥ₙ := rec (elem ∘ f) (uniq n) - hott def ap₂ {A : Type u} {B : Type v} {C : Type w} + hott definition ap₂ {A : Type u} {B : Type v} {C : Type w} {n : ℕ₋₂} (f : A → B → C) : ∥A∥ₙ → ∥B∥ₙ → ∥C∥ₙ := rec (ap ∘ f) (piRespectsNType n (λ _, uniq n)) diff --git a/GroundZero/Meta/Notation.lean b/GroundZero/Meta/Notation.lean index 674b8c4..34ebc73 100644 --- a/GroundZero/Meta/Notation.lean +++ b/GroundZero/Meta/Notation.lean @@ -66,7 +66,7 @@ section } end -macro "begin " ts:sepBy1(tactic, ";", "; ", allowTrailingSep) i:"end" : term => +macro "begin " ts:sepBy(tactic, ";", "; ", allowTrailingSep) i:"end" : term => `(by { $[($ts:tactic)]* }%$i) declare_syntax_cat superscriptNumeral @@ -323,8 +323,8 @@ namespace Defeq elab "#success " σ₁:term tag:" ≡ " σ₂:term τ:(typeSpec)? : command => Elab.Command.runTermElabM fun _ => do { let T ← elabTypeSpec τ; - let τ₁ ← Elab.Term.elabTerm σ₁ T; - let τ₂ ← Elab.Term.elabTerm σ₂ T; + let τ₁ ← Elab.Term.elabTermEnsuringType σ₁ T; + let τ₂ ← Elab.Term.elabTermEnsuringType σ₂ T; Elab.Term.synthesizeSyntheticMVarsNoPostponing; let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁); @@ -336,8 +336,8 @@ namespace Defeq elab "#failure " σ₁:term tag:" ≡ " σ₂:term τ:(typeSpec)? : command => Elab.Command.runTermElabM fun _ => do { let T ← elabTypeSpec τ; - let τ₁ ← Elab.Term.elabTerm σ₁ T; - let τ₂ ← Elab.Term.elabTerm σ₂ T; + let τ₁ ← Elab.Term.elabTermEnsuringType σ₁ T; + let τ₂ ← Elab.Term.elabTermEnsuringType σ₂ T; Elab.Term.synthesizeSyntheticMVarsNoPostponing; let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁); diff --git a/GroundZero/Meta/Trust.lean b/GroundZero/Meta/Trust.lean index 77905f0..957fa76 100644 --- a/GroundZero/Meta/Trust.lean +++ b/GroundZero/Meta/Trust.lean @@ -22,7 +22,7 @@ def Quot.withUseOf {X : Type u} {R : X → X → Sort 0} {A : Type v} {B : Type section variable (X : Type u) (R : X → X → Sort 0) (A : Type u) (B : Type w) (a₁ a₂ : A) (b : B) - #failure @Quot.withUseOf X R A B a₁ b ≡ @Quot.withUseOf X R A B a₂ b + #failure @Quot.withUseOf X R A B a₁ b ≡ @Quot.withUseOf X R A B a₂ b : Quot R → B end /-- @@ -43,11 +43,11 @@ namespace EtaFailure variable (X : Type u) (A : Type u) (B : Type w) (a₁ a₂ : A) (b : B) - #success @withUseOf X A B a₁ b ≡ @withUseOf X A B a₂ b + #success @withUseOf X A B a₁ b ≡ @withUseOf X A B a₂ b : Opaque X → B variable (x : Opaque X) - #success @withUseOf X A B a₁ b x ≡ b - #success @withUseOf X A B a₂ b x ≡ b + #success @withUseOf X A B a₁ b x ≡ b : B + #success @withUseOf X A B a₂ b x ≡ b : B end EtaFailure namespace Opaque diff --git a/GroundZero/Theorems/Functions.lean b/GroundZero/Theorems/Functions.lean index e19b49e..e5dfee7 100644 --- a/GroundZero/Theorems/Functions.lean +++ b/GroundZero/Theorems/Functions.lean @@ -26,16 +26,14 @@ hott def Ran {A : Type u} {B : Type v} (f : A → B) := total (fibInh f) hott def cut {A : Type u} {B : Type v} (f : A → B) : A → Ran f := -λ x, ⟨f x, Merely.elem ⟨x, idp (f x)⟩⟩ +λ x, ⟨f x, |⟨x, idp (f x)⟩|⟩ hott def cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) := begin intro ⟨x, (H : ∥_∥)⟩; induction H; - case elemπ G => { - apply Merely.elem; existsi G.1; - fapply Sigma.prod; exact G.2; - apply Merely.uniq - }; + case elemπ G => + { apply Merely.elem; existsi G.1; fapply Sigma.prod; + exact G.2; apply Merely.uniq }; apply Merely.uniq end @@ -52,9 +50,8 @@ begin { intro; reflexivity } end -hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) : - Ran (Function.const A b) := -⟨b, Merely.elem ⟨a, idp b⟩⟩ +hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) : Ran (Function.const A b) := +⟨b, |⟨a, idp b⟩|⟩ hott def ranConstEqv {A : Type u} (a : A) {B : Type v} (H : hset B) (b : B) : Ran (Function.const A b) ≃ 𝟏 := diff --git a/GroundZero/Types/CellComplex.lean b/GroundZero/Types/CellComplex.lean index 8bced3e..e56b23b 100644 --- a/GroundZero/Types/CellComplex.lean +++ b/GroundZero/Types/CellComplex.lean @@ -1,21 +1,21 @@ import GroundZero.HITs.Sphere open GroundZero.HITs -universe u v +universe u v w namespace GroundZero namespace Types --- https://github.com/leanprover/lean2/blob/master/hott/homotopy/cellcomplex.hlean --- https://arxiv.org/abs/1802.02191 +/- https://github.com/leanprover/lean2/blob/master/hott/homotopy/cellcomplex.hlean + Cellular Cohomology in Homotopy Type Theory, https://arxiv.org/abs/1802.02191 +-/ hott definition Model := Σ (X : Type u), X → Type v hott definition FdCC : ℕ → Model -| Nat.zero => ⟨Set u, Sigma.fst⟩ -| Nat.succ n => ⟨Σ (X : (FdCC n).1) (A : Set u), A.1 × Sⁿ → (FdCC n).2 X, - λ w, Pushout (@Prod.fst w.2.1.1 Sⁿ) w.2.2⟩ +| Nat.zero => ⟨Set u, Sigma.pr₁⟩ +| Nat.succ n => ⟨Σ (X : (FdCC n).1) (A : Set u), A.1 × Sⁿ → (FdCC n).2 X, λ w, Pushout Prod.pr₁ w.2.2⟩ -- finite-dimensional cell complex hott definition fdcc (n : ℕ) := (FdCC n).1