From e02ad2dcc0f93107c18f8316b386b92b45548e97 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 30 Nov 2025 22:20:35 +0100 Subject: update lean --- Nominal/Helpers/CountableString.lean | 4 +++- Nominal/LambdaCalculus/Preterms.lean | 2 +- Nominal/LambdaCalculus/Terms.lean | 7 ++++++- Nominal/Support.lean | 4 ++-- flake.lock | 6 +++--- lake-manifest.json | 26 +++++++++++++------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 8 files changed, 30 insertions(+), 23 deletions(-) diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean index 7d2fcb7..7d94516 100644 --- a/Nominal/Helpers/CountableString.lean +++ b/Nominal/Helpers/CountableString.lean @@ -9,4 +9,6 @@ instance : Countable Char where instance : Countable String := Countable.of_equiv (List Char) { toFun := String.mk - invFun := String.data } + invFun := String.data + left_inv x := by simp + right_inv x := by simp } diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean index 74f7397..c133343 100644 --- a/Nominal/LambdaCalculus/Preterms.lean +++ b/Nominal/LambdaCalculus/Preterms.lean @@ -114,7 +114,7 @@ instance : NominalSet Var Preterm where simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq] simp only [PermSet.fix, vars, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ exact ⟨hπ.left, a_ih.left hπ.right⟩ - · simp [vars, Set.Finite.insert, a_ih] + · simp [vars, a_ih] · constructor · intro π hπ simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq] diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index 2118156..c698b65 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -229,7 +229,12 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (by intro t u htu cases htu - sorry) + · sorry + · sorry + · sorry + · sorry + · sorry + · sorry) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x diff --git a/Nominal/Support.lean b/Nominal/Support.lean index b8e6809..93e7aaa 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -153,9 +153,9 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite /-- For a finite number of finite supports, the intersection is also a support. -/ lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by - suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite + suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) ∧ (⋂₀ (↑C : Set (Set 𝔸))).Finite · intro hfin - rw [show C = hfin.toFinset.toSet by simp] + rw [show C = hfin.toFinset by simp] intro hne h exact (this hfin.toFinset hne h).left · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸) diff --git a/flake.lock b/flake.lock index 6650c8f..99d3a8f 100644 --- a/flake.lock +++ b/flake.lock @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1758213207, - "narHash": "sha256-rqoqF0LEi+6ZT59tr+hTQlxVwrzQsET01U4uUdmqRtM=", + "lastModified": 1764167966, + "narHash": "sha256-nXv6xb7cq+XpjBYIjWEGTLCqQetxJu6zvVlrqHMsCOA=", "owner": "nixos", "repo": "nixpkgs", - "rev": "f4b140d5b253f5e2a1ff4e5506edbf8267724bde", + "rev": "5c46f3bd98147c8d82366df95bbef2cab3a967ea", "type": "github" }, "original": { diff --git a/lake-manifest.json b/lake-manifest.json index e793730..6dce1af 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "37df177aaa770670452312393d4e84aaad56e7b6", + "rev": "1ccd71f89cbbd82ae7d097723ce1722ca7b01c33", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.23.0", + "inputRev": "v4.25.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9", + "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957", + "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.71", + "inputRev": "v0.0.79", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "247ff80701c76760523b5d7c180b27b7708faf38", + "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65", + "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d117e2c28cba42e974bc22568ac999492a34e812", + "rev": "5c78955e8375f872c085514cb521216bac1bda17", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,11 +85,11 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc", + "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.25.0", "inherited": true, "configFile": "lakefile.toml"}], - "name": "Nominal", + "name": "CoalgebraicAutomata", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index 45c09ba..bf4beec 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,7 +5,7 @@ defaultTargets = ["Nominal"] [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.23.0" +rev = "v4.25.0" [[lean_lib]] name = "Nominal" diff --git a/lean-toolchain b/lean-toolchain index 7f254a9..e5ab73a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.23.0 +leanprover/lean4:v4.25.0 -- cgit v1.3.1