diff options
| -rw-r--r-- | Algebra/Derivations.lean | 10 | ||||
| -rw-r--r-- | Graded/GradedMonad.lean | 20 | ||||
| -rw-r--r-- | Nominal/Equivariance.lean | 9 | ||||
| -rw-r--r-- | Nominal/Helpers/CountableString.lean | 6 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 12 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 10 | ||||
| -rw-r--r-- | Nominal/LambdaCalculus/Terms.lean | 22 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 6 | ||||
| -rw-r--r-- | Nominal/Support.lean | 2 | ||||
| -rw-r--r-- | flake.lock | 6 | ||||
| -rw-r--r-- | lake-manifest.json | 26 | ||||
| -rw-r--r-- | lakefile.toml | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
13 files changed, 70 insertions, 65 deletions
diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean index 717ffe1..b6e5cb5 100644 --- a/Algebra/Derivations.lean +++ b/Algebra/Derivations.lean @@ -118,11 +118,11 @@ lemma Derivable.of_eq Derivable T eq := by intro hderiv have heq : (eq.val.vars ⊢ t ≣ u) = eq := by - apply Subtype.eq; ext + apply Subtype.ext; ext · rfl · rfl - · rw [heq_eq_eq]; exact ht - · rw [heq_eq_eq]; exact hu + · exact heq_of_eq ht + · exact heq_of_eq hu rw [← heq]; exact hderiv lemma Derivable.equivariant_substitution @@ -180,7 +180,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : · rw [rename_eq] apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _ apply Derivable.trans _ (by apply equivariant_substitution; exact h_1) - rw [← MulAction.mul_smul, ← MulAction.mul_smul] + rw [← SemigroupAction.mul_smul, ← SemigroupAction.mul_smul] apply Derivable.ax · exact h · exact h_1 @@ -195,7 +195,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : exact h_1 x · intro x show Derivable T (X_1 ⊢ π • ts x ≣ ⸨π a, π b⸩ • π • us x) - rw [← MulAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, MulAction.mul_smul] + rw [← SemigroupAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, SemigroupAction.mul_smul] exact a_ih x instance DerivableEq.instEquivariant : Rel.Equivariant 𝔸 (DerivableEq T X n) := by diff --git a/Graded/GradedMonad.lean b/Graded/GradedMonad.lean index d0af5f4..39d543c 100644 --- a/Graded/GradedMonad.lean +++ b/Graded/GradedMonad.lean @@ -54,17 +54,23 @@ def ofMonad (M : Monad C) : GradedMonad C where toFunctor _ := M.toFunctor η := M.η μ _ _ := M.μ - assoc X _ _ _ := by simp [M.assoc X] - left_unit X _ := by simp [M.left_unit] - right_unit X _ := by simp [M.right_unit] + assoc X _ _ _ := by simp only [Functor.comp_obj, eqToHom_refl, Category.comp_id]; exact M.assoc X + left_unit X _ := by simp only [eqToHom_refl, Category.comp_id]; exact M.left_unit X + right_unit X _ := by exact M.right_unit X def toMonad (M : GradedMonad C) : Monad C := { M 0 with η := M.η μ := M.μ 0 0 - assoc X := by simp [M.assoc X 0 0 0] - left_unit X := by simp [M.left_unit X 0] - right_unit X := by simp [M.right_unit X 0] } + assoc X := by + have h := M.assoc X 0 0 0 + simp only [Functor.comp_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h + exact h + left_unit X := by + have h := M.left_unit X 0 + simp only [Functor.id_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h + exact h + right_unit X := M.right_unit X 0 } lemma toMonad_ofMonad {M : Monad C} : (ofMonad M).toMonad = M := rfl @@ -83,6 +89,8 @@ def ofComp (F : C ⥤ C) : GradedMonad C where η := NatTrans.id (𝟭 C) μ n k := NatTrans.id (compFunctor F k ⋙ compFunctor F n) ≫ eqToHom (compFunctor_comp _ n k) assoc X n k m := by simp [eqToHom_map] + left_unit X n := by simp [compFunctor] + right_unit X n := by simp [compFunctor] end GradedMonad diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 2682a55..e9bd850 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -25,7 +25,7 @@ class inductive Function.Equivariant (f : X → Y) : Prop lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] : ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by - cases (inferInstanceAs (Equivariant 𝔸 f)); assumption + cases (inferInstance : Equivariant 𝔸 f); assumption /-- A set is equivariant if it is closed under permutations. -/ class inductive Set.Equivariant (S : Set X) : Prop @@ -34,7 +34,7 @@ class inductive Set.Equivariant (S : Set X) : Prop /-- For equivariant sets, we even have "if and only if". -/ lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] : ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by - cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h + cases (inferInstance : Equivariant 𝔸 S); rename_i h intro x π; constructor · intro hx; exact h x π hx · intro hx @@ -49,7 +49,7 @@ class inductive Rel.Equivariant (R : Rel X Y) : Prop /-- For equivariant relations, we even have "if and only if". -/ lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] : ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by - cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h + cases (inferInstance : Equivariant 𝔸 R); rename_i h intro x y π; constructor · intro hxy; exact h x y π hxy · intro hxy @@ -83,6 +83,7 @@ instance Function.Equivariant.comp _ = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f] /-- If a function is equivariant, its inverse is also equivariant. -/ +@[reducible] def Function.Equivariant.inv {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X} (hleft : Function.LeftInverse inv f) @@ -191,6 +192,7 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] : end Function.Equivariant /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/ +@[reducible] def NominalSet.ofEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) : @@ -385,6 +387,7 @@ instance EquivariantEquiv.invFunEquivariant equiv.invFun_equivariant /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/ +@[reducible] def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X := NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean index b6f59f8..c887f96 100644 --- a/Nominal/Helpers/CountableString.lean +++ b/Nominal/Helpers/CountableString.lean @@ -5,10 +5,10 @@ instance : Countable Char where use Char.toNat intro c₁ c₂ hc rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc - exact Char.eq_of_val_eq hc + exact Char.ext hc instance : Countable String := Countable.of_equiv (List Char) - { toFun := String.mk - invFun := String.data + { toFun := String.ofList + invFun := String.toList left_inv x := by simp right_inv x := by simp } diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index e03d67a..f1a711b 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -225,16 +225,12 @@ instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸 instAlphaEqEquivariant /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/ -def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X) +abbrev NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X) namespace NameAbstraction -/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ -abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := - Quotient.mk (setoid 𝔸 X) (.mk a x) - /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ -notation "⟪" a "⟫ " x:60 => mk a x +notation "⟪" a "⟫ " x:60 => (⟦⟨a, x⟩⟧ : NameAbstraction _ _) instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸 @@ -390,13 +386,13 @@ private lemma map_id : map 𝔸 (EquivariantMap.id 𝔸 : X →ₑ[𝔸] X) = Eq suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.id 𝔸) x = x by ext x; exact this x apply Quotient.ind intro x - simp [map', NameAbstraction.mk] + simp [map'] private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 (EquivariantMap.comp 𝔸 f g) = EquivariantMap.comp 𝔸 (map 𝔸 f) (map 𝔸 g) := by suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.comp 𝔸 f g) x = (map' 𝔸 f) ((map' 𝔸 g) x) by ext x; exact this x apply Quotient.ind intro x - simp [map', NameAbstraction.mk] + simp [map'] /-- Name abstractions form a functor `Nom ⥤ Nom`. -/ def Functor : Nom 𝔸 ⥤ Nom 𝔸 := diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index b627c1b..7a88eeb 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -59,6 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅. -/ section Discrete +@[reducible] def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where smul π x := x one_smul := by intro; rfl @@ -330,6 +331,7 @@ instance : PermSet 𝔸 (Quotient setoid) where instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by constructor; simp +@[reducible] def lift_equivariant {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f] (h : ∀ (a b : X), a ≈ b → f a = f b) : @@ -392,11 +394,11 @@ instance : PermSet 𝔸 S where rw [← Set.equivariant 𝔸 S] exact x.prop⟩ one_smul x := by - apply Subtype.eq + apply Subtype.ext exact MulAction.one_smul x.val mul_smul π τ x := by - apply Subtype.eq - exact MulAction.mul_smul π τ x.val + apply Subtype.ext + exact SemigroupAction.mul_smul π τ x.val @[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl @@ -410,7 +412,7 @@ instance : NominalSet 𝔸 S where use NominalSet.supp 𝔸 x.val constructor · intro π hπ - apply Subtype.eq + apply Subtype.ext exact NominalSet.supp_is_support 𝔸 hπ · exact NominalSet.supp_finite 𝔸 diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index 91f4fb8..7af82cd 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -53,40 +53,37 @@ instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by exact h /-- Define λ-terms as the quotient Preterm/≈. -/ -def Term := Quotient Preterm.setoid +abbrev Term := Quotient Preterm.setoid namespace Term -/-- The equivalence class of a λ-preterm. -/ -abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid - instance : NominalSet Var Term := Quotient.instNominalSet Var @[simp] -lemma smul {π : FPerm Var} {t : Preterm} : π • Term.mk t = Term.mk (π • t) := by congr +lemma smul {π : FPerm Var} {t : Preterm} : π • (⟦t⟧ : Term) = ⟦π • t⟧ := by congr private lemma alpha_eq {t u : Preterm} : t ≈ u ↔ AlphaEq t u := by rfl -lemma eq_iff_alpha_eq {t u : Preterm} : mk t = mk u ↔ t ≈ u := by +lemma eq_iff_alpha_eq {t u : Preterm} : (⟦t⟧ : Term) = (⟦u⟧ : Term) ↔ t ≈ u := by rw [Quotient.eq_iff_equiv] -def var : Var → Term := fun x => mk (.var x) +def var : Var → Term := fun x => ⟦.var x⟧ def abs : Var → Term → Term := fun x => Quotient.lift - (fun t => mk (.abs x t)) + (fun t => ⟦.abs x t⟧) (by intro t t'; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_abs) def app : Term → Term → Term := Quotient.lift₂ - (fun t u => mk (.app t u)) + (fun t u => ⟦.app t u⟧) (by intro t₁ t₂ u₁ u₂; rw [eq_iff_alpha_eq]; exact AlphaEq.cong_app) @[simp] -lemma abs_preterm {x : Var} {t : Preterm} : abs x (mk t) = mk (.abs x t) := rfl +lemma abs_preterm {x : Var} {t : Preterm} : abs x ⟦t⟧ = ⟦.abs x t⟧ := rfl @[simp] -lemma app_preterm {t u : Preterm} : app (mk t) (mk u) = mk (.app t u) := rfl +lemma app_preterm {t u : Preterm} : app ⟦t⟧ ⟦u⟧ = ⟦.app t u⟧ := rfl /-- Alternative characterization of α-equivalence for each preterm constructor. -/ inductive AlphaEq' : Preterm → Preterm → Prop where @@ -242,7 +239,6 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ obtain ⟨u', hu'⟩ := u.exists_rep simp only [abs, ← ht', Quotient.lift_mk, ← hu'] rw [Quotient.eq_iff_equiv, alpha_eq_abs] - rfl /-- Alternative characterization of α-equivalence for application preterms. -/ lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by @@ -295,7 +291,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (by intro t u htu rw [alpha_eq, alpha_eq_iff] at htu - cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption) + cases htu <;> simp [*]) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 0a4974a..f1115d3 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -42,7 +42,7 @@ lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by /-- The support of the inverse function is the same as the function's support. -/ lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by - simp [supp, set_support_inv_eq] + simp [supp, set_support_symm_eq] /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/ lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by @@ -199,10 +199,10 @@ instance : PermSet 𝔸 𝔸 where instance : OrbitFinite 𝔸 𝔸 where fin_orbits := Finite.of_equiv Unit - { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some + { toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some invFun _ := () right_inv := by - let chosen := (inferInstanceAs (Nonempty 𝔸)).some + let chosen := (inferInstance : Nonempty 𝔸).some apply Quotient.ind; intro a rw [Quotient.eq] show chosen ∈ MulAction.orbit (FPerm 𝔸) a diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 7888a68..fde20c7 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -79,7 +79,7 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite simp) let m' := (S \ T).restrict m rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective - obtain h_m_inv := Function.partialInv_of_injective h_m_injective + obtain h_m_inv := h_m_injective.isPartialInv have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ := Set.image_subset_iff.mpr h_m_preimage @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1764167966, - "narHash": "sha256-nXv6xb7cq+XpjBYIjWEGTLCqQetxJu6zvVlrqHMsCOA=", + "lastModified": 1775888245, + "narHash": "sha256-nwASzrRDD1JBEu/o8ekKYEXm/oJW6EMCzCRdrwcLe90=", "owner": "nixos", "repo": "nixpkgs", - "rev": "5c46f3bd98147c8d82366df95bbef2cab3a967ea", + "rev": "13043924aaa7375ce482ebe2494338e058282925", "type": "github" }, "original": { diff --git a/lake-manifest.json b/lake-manifest.json index 6dce1af..707a535 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1ccd71f89cbbd82ae7d097723ce1722ca7b01c33", + "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.25.0", + "inputRev": "v4.29.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d", + "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.79", + "inputRev": "v0.0.95", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c78955e8375f872c085514cb521216bac1bda17", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,11 +85,11 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.25.0", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], - "name": "CoalgebraicAutomata", + "name": "Nominal", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index 21e9fc9..513bf8e 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,7 +5,7 @@ defaultTargets = ["Nominal"] [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.25.0" +rev = "v4.29.0" [[lean_lib]] name = "Nominal" @@ -15,4 +15,4 @@ name = "Graded" [[lean_lib]] name = "Algebra" -needs = ["Nominal", "Graded"]
\ No newline at end of file +needs = ["Nominal", "Graded"] diff --git a/lean-toolchain b/lean-toolchain index e5ab73a..d324cad 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0 +leanprover/lean4:v4.29.0
\ No newline at end of file |