From 05db6d4b0b762d28d4ae5cf8150e6a15a12257c0 Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Fri, 11 Oct 2024 18:56:21 +0200 Subject: [PATCH] update to Lean 4.12 --- Bml/Partitions.lean | 6 ++--- Bml/Tableau.lean | 10 ++++--- Bml/Tableauexamples.lean | 20 ++------------ Makefile | 4 +-- Pdl/LocalTableau.lean | 57 +++++++++++++++++++++++++++++----------- Pdl/MultisetOrder.lean | 11 +------- Pdl/Soundness.lean | 6 ++--- Pdl/UnfoldBox.lean | 30 ++++++++++++--------- lake-manifest.json | 26 ++++++++++++------ lakefile.lean | 4 ++- lean-toolchain | 2 +- 11 files changed, 97 insertions(+), 79 deletions(-) diff --git a/Bml/Partitions.lean b/Bml/Partitions.lean index fdc1383..b3f1a30 100644 --- a/Bml/Partitions.lean +++ b/Bml/Partitions.lean @@ -307,9 +307,9 @@ theorem endNodesOfChildSublistEndNodes (c_in_C : cLR ∈ C) lrApp : (endNodesOf ⟨cLR, subTabs cLR c_in_C⟩).Sublist (endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩) := by - simp_all [endNodesOf] - apply List.sublist_join - simp_all + simp_all only [lrEndNodes] + apply List.sublist_join_of_mem + simp_all only [List.mem_map, List.mem_attach, true_and, Subtype.exists] use cLR, c_in_C open List diff --git a/Bml/Tableau.lean b/Bml/Tableau.lean index 3000217..e144955 100644 --- a/Bml/Tableau.lean +++ b/Bml/Tableau.lean @@ -59,7 +59,7 @@ def SimpleForm : Formula → Prop | _ => False instance : Decidable (SimpleForm φ) := - match h : φ with + match φ with | ⊥ | ·_ | □_ => Decidable.isTrue <| by aesop @@ -204,13 +204,13 @@ inductive LocalRuleApp : TNode → List TNode → Type theorem oneSidedRule_preserves_other_side_L {ruleApp : LocalRuleApp (L, R) C} - (hmyrule : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (res, ∅)) _) _ _ rule hC preproof)) + (_ : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (res, ∅)) _) _ _ rule hC preproof)) (rule_is_left : rule = LocalRule.oneSidedL orule ) : ∀ c ∈ C, c.2 = R := by aesop theorem oneSidedRule_preserves_other_side_R {ruleApp : LocalRuleApp (L, R) C} - (hmyrule : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (∅, res)) _) _ _ rule hC preproof)) + (_ : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (∅, res)) _) _ _ rule hC preproof)) (rule_is_right : rule = LocalRule.oneSidedR orule ) : ∀ c ∈ C, c.1 = L := by aesop @@ -820,7 +820,9 @@ theorem existsLocalTableauFor LR : Nonempty (LocalTableau LR) := apply LocalTableau.fromSimple by_contra hyp have := notSimpleThenLocalRule hyp - aesop + rcases this with ⟨Lcond, Rcond, ress, lr, Lin, Rin⟩ + absurd canApplyRule + tauto case inr canApplyRule => rw [not_not] at canApplyRule rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩ diff --git a/Bml/Tableauexamples.lean b/Bml/Tableauexamples.lean index 47f51ea..721803f 100644 --- a/Bml/Tableauexamples.lean +++ b/Bml/Tableauexamples.lean @@ -139,23 +139,7 @@ example : ClosedTableau ({r⋀~(□p), r↣□(p⋀q)}, {}) := intro Y Y_in simp (config := {decide := true}) at * have : Y = ({·'r', ~(□p), □(p⋀q)}, {}) := by - rcases Y_in with ⟨l, ⟨a, ⟨a_def, def_l⟩⟩, Y_in_l⟩ - subst_eqs - simp [endNodesOf] at * - rcases Y_in_l with ⟨l, ⟨a, ⟨a_def, def_l⟩⟩, Y_in_l⟩ - cases a_def - · subst_eqs - simp [endNodesOf] at * - · subst_eqs - simp [endNodesOf] at * - have : ({·'r', ~(□p), ~~(□(p⋀q))}, ∅) ≠ (({·'r', ~(□p), ~·'r'}: Finset Formula), (∅ : Finset Formula)) := by decide - simp only [this] at Y_in_l - simp at Y_in_l - clear this -- hmm - rcases Y_in_l with ⟨l, ⟨a, ⟨ a_def, def_l⟩ ⟩, Y_in_l⟩ - subst_eqs - simp [endNodesOf] at * - subst Y_in_l - decide + subst Y_in + decide subst this exact subTabForEx2 diff --git a/Makefile b/Makefile index 65b379a..d56c252 100644 --- a/Makefile +++ b/Makefile @@ -22,7 +22,7 @@ dependencies.svg: Pdl/*.lean update-fix: rm -rf .lake - echo "leanprover/lean4:v4.11.0" > lean-toolchain + echo "leanprover/lean4:v4.12.0" > lean-toolchain echo "If next command fails, edit lakefile.lean manually." - grep v4.11.0 lakefile.lean + grep v4.12.0 lakefile.lean lake update -R diff --git a/Pdl/LocalTableau.lean b/Pdl/LocalTableau.lean index 59afdd1..434467f 100644 --- a/Pdl/LocalTableau.lean +++ b/Pdl/LocalTableau.lean @@ -89,13 +89,13 @@ theorem tautImp_iff_TNodeUnsat {φ ψ} {X : TNode} : /-! ## Different kinds of formulas as elements of TNode -/ @[simp] -instance : Membership Formula TNode := ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩ +instance : Membership Formula TNode := ⟨fun X φ => φ ∈ X.L ∨ φ ∈ X.R⟩ @[simp] -def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop := +def NegLoadFormula.mem_TNode (X : TNode) (nlf : NegLoadFormula) : Prop := X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf) -instance : Decidable (NegLoadFormula_in_TNode nlf ⟨L,R,O⟩) := by +instance : Decidable (NegLoadFormula.mem_TNode ⟨L,R,O⟩ nlf) := by refine if h : O = some (Sum.inl nlf) then isTrue ?_ else if h2 : O = some (Sum.inr nlf) then isTrue ?_ else isFalse ?_ @@ -103,17 +103,17 @@ instance : Decidable (NegLoadFormula_in_TNode nlf ⟨L,R,O⟩) := by def TNode.without : (LRO : TNode) → (naf : AnyNegFormula) → TNode | ⟨L,R,O⟩, ⟨.normal f⟩ => ⟨L \ {~f}, R \ {~f}, O⟩ -| ⟨L,R,O⟩, ⟨.loaded lf⟩ => if (NegLoadFormula_in_TNode (~'lf) ⟨L,R,O⟩) then ⟨L, R, none⟩ else ⟨L,R,O⟩ +| ⟨L,R,O⟩, ⟨.loaded lf⟩ => if ((~'lf).mem_TNode ⟨L,R,O⟩) then ⟨L, R, none⟩ else ⟨L,R,O⟩ @[simp] -instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩ +instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula.mem_TNode⟩ -def AnyNegFormula_in_TNode : (anf : AnyNegFormula) → (X : TNode) → Prop -| ⟨.normal φ⟩, X => (~φ) ∈ X -| ⟨.loaded χ⟩, X => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here +def AnyNegFormula.mem_TNode : (X : TNode) → (anf : AnyNegFormula) → Prop +| X, ⟨.normal φ⟩ => (~φ) ∈ X +| X, ⟨.loaded χ⟩ => (~'χ).mem_TNode X -- FIXME: ∈ not working here @[simp] -instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩ +instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula.mem_TNode⟩ /-! ## Local Tableaux -/ @@ -660,21 +660,32 @@ theorem preconP_to_submultiset (preconditionProof : List.Subperm Lcond L ∧ Lis have := List.Subperm.count_le (List.Subperm.append preconditionProof.1 preconditionProof.2.1) f cases g <;> (rename_i nlform; cases nlform; simp_all) +-- easier way to do this? +theorem Multiset.sub_of_le [DecidableEq α] {M N X Y: Multiset α} (h : N ≤ M) : + M - N + Y = X ↔ M + Y = X + N := by + constructor + · intro hyp + have := @tsub_eq_iff_eq_add_of_le _ _ _ _ _ _ _ _ _ Y _ h + sorry + · intro hyp + sorry + /-- Applying `node_to_multiset` before or after `applyLocalRule` gives the same. -/ theorem node_to_multiset_of_precon (precon : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) : node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond) + node_to_multiset (Lnew, Rnew, Onew) = node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, Olf.change O Ocond Onew) := by have := preconP_to_submultiset precon -- TODO: can we use this to avoid the `-`? + rw [Multiset.sub_of_le] simp only [node_to_multiset_eq] - simp only [Multiset.coe_add, List.append_assoc, Multiset.coe_sub, List.diff_append, - Multiset.coe_eq_coe] + -- simp only [Multiset.coe_add, List.append_assoc, Multiset.coe_sub, List.diff_append, Multiset.coe_eq_coe] rcases precon with ⟨Lpre, Rpre, Opre⟩ -- we now get 3 * 3 * 3 = 27 cases all_goals cases O <;> try (rename_i O; cases O) all_goals cases Onew <;> try (rename_i Onew; cases Onew) all_goals cases Ocond <;> try (rename_i cond; cases cond) - all_goals simp_all -- deals with 12 out of 27 cases + all_goals try (simp_all; done) -- deals with 12 out of 27 cases all_goals + simp sorry @[simp] @@ -783,20 +794,30 @@ theorem H_goes_down (α : Program) φ {Fs δ} (in_H : (Fs, δ) ∈ H α) {ψ} (i · have IHα := H_goes_down α φ in_H in_Fs' cases α all_goals - simp_all [testsOfProgram, lmOfFormula, List.attach_map_val] + simp [lmOfFormula] at IHα + all_goals + simp only [List.attach_map_val, testsOfProgram] at * + simp_all [lmOfFormula] try linarith · have IHβ := H_goes_down β φ in_Hβ in_Fs'' cases β all_goals simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val] try linarith - · simp_all [testsOfProgram] + all_goals + simp_all only [Function.comp_def, List.attach_map_val] + linarith + · simp_all only [ite_false, List.mem_singleton, Prod.mk.injEq, testsOfProgram, + List.attach_append, List.map_append, List.map_map, List.sum_append] + rw [Function.comp_def, Function.comp_def, List.attach_map_val, List.attach_map_val] cases in_l subst_eqs have IHα := H_goes_down α φ in_H in_Fs cases α all_goals simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val] + all_goals + try rw [Function.comp_def, Function.comp_def, List.attach_map_val, List.attach_map_val] at IHα try linarith case union α β => simp [H] at in_H @@ -806,11 +827,15 @@ theorem H_goes_down (α : Program) φ {Fs δ} (in_H : (Fs, δ) ∈ H α) {ψ} (i all_goals simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val] try linarith + all_goals + sorry · have IHβ := H_goes_down β φ hyp in_Fs cases β all_goals simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val] try linarith + all_goals + sorry case star α => simp [H] at in_H rcases in_H with _ | ⟨l, ⟨Fs', δ', in_H', def_l⟩, in_l⟩ @@ -838,7 +863,7 @@ theorem unfoldDiamond.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X · cases α <;> simp_all [Program.isAtomic, testsOfProgram, List.attach_map_val] case sequence α β => suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α;'β))).sum.succ by - simp_all [testsOfProgram] + simp_all [testsOfProgram, Function.comp_def, List.attach_map_val] linarith suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by rw [Nat.lt_succ] @@ -850,7 +875,7 @@ theorem unfoldDiamond.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X aesop case union α β => suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α⋓β))).sum.succ by - simp_all [testsOfProgram] + simp_all [testsOfProgram, Function.comp_def, List.attach_map_val] linarith suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by rw [Nat.lt_succ] diff --git a/Pdl/MultisetOrder.lean b/Pdl/MultisetOrder.lean index 19813e0..32a7c71 100644 --- a/Pdl/MultisetOrder.lean +++ b/Pdl/MultisetOrder.lean @@ -45,7 +45,6 @@ lemma singleton_add_sub_of_cons_add [DecidableEq α] {a a0: α} {M X : Multiset theorem sub_singleton [DecidableEq α] (a : α) (s : Multiset α) : s - {a} = s.erase a := by ext simp [Multiset.erase_singleton, Multiset.count_singleton] - split <;> simp_all theorem mem_sub_of_not_mem_of_mem {α} [DecidableEq α] (x : α) (X Y: Multiset α) (x_in_X : x ∈ X) (x_notin_Y : x ∉ Y) : x ∈ X - Y := by @@ -136,13 +135,6 @@ lemma not_redLT_zero [DecidableEq α] [LT α] (M: Multiset α) : ¬ MultisetRedL simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true] contradiction --- Should be added to 'mathlib4/Mathlib/Data/Multiset/Basic.lean' -lemma mul_singleton_erase [DecidableEq α] {a : α} {M : Multiset α} : - M - {a} = M.erase a := by - ext - simp [Multiset.erase_singleton, Multiset.count_singleton] - split <;> simp_all - lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : MultisetRedLT N (a ::ₘ M)) : ∃ M', N = (a ::ₘ M') ∧ (MultisetRedLT M' M) ∨ (N = M + M') ∧ (∀ x : α, x ∈ M' → x < a) := by @@ -165,7 +157,6 @@ lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : Mult · have := h0 b aesop · have := h0 b - simp [mul_singleton_erase] aesop subst this rw [add_comm] @@ -179,7 +170,7 @@ lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : Mult have a0M: a0 ∈ M := by apply in_of_ne_of_cons_erase · change M = Multiset.erase (a0 ::ₘ X) a - rw [mul_singleton_erase, add_comm] at this0 + rw [Multiset.sub_singleton, add_comm] at this0 exact this0 · exact hyp rw [add_comm] diff --git a/Pdl/Soundness.lean b/Pdl/Soundness.lean index c2f3fd0..731f085 100644 --- a/Pdl/Soundness.lean +++ b/Pdl/Soundness.lean @@ -126,8 +126,8 @@ theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := b The `loc` ad `pdl` steps correspond to two out of three constructors of `Tableau`. -/ inductive PathIn : ∀ {H X}, Tableau H X → Type | nil : PathIn _ -| loc : (Y_in : Y ∈ endNodesOf lt) → (tail : PathIn (next Y Y_in)) → PathIn (Tableau.loc lt next) -| pdl : (r : PdlRule Γ Δ) → PathIn (child : Tableau (Γ :: Hist) Δ) → PathIn (Tableau.pdl r child) +| loc {Y lt next} : (Y_in : Y ∈ endNodesOf lt) → (tail : PathIn (next Y Y_in)) → PathIn (Tableau.loc lt next) +| pdl {Γ Δ Hist child} : (r : PdlRule Γ Δ) → PathIn (child : Tableau (Γ :: Hist) Δ) → PathIn (Tableau.pdl r child) deriving DecidableEq def tabAt : PathIn tab → Σ H X, Tableau H X @@ -368,7 +368,7 @@ theorem not_edge_nil (tab : Tableau Hist X) (t : PathIn tab) : ¬ edge t .nil := subst X_eq_Z rw [heq_eq_eq] at hyp subst hyp - simp_all only + simp_all theorem nodeAt_loc_nil {H : List TNode} {lt : LocalTableau X} (next : (Y : TNode) → Y ∈ endNodesOf lt → Tableau (X :: H) Y) (Y_in : Y ∈ endNodesOf lt) : diff --git a/Pdl/UnfoldBox.lean b/Pdl/UnfoldBox.lean index f85cbfc..0c75c65 100644 --- a/Pdl/UnfoldBox.lean +++ b/Pdl/UnfoldBox.lean @@ -121,7 +121,7 @@ theorem signature_contradiction_of_neq_TPs {ℓ ℓ' : TP α} : constructor · use τ, τ_in simp_all - · assumption + · simp_all -- unused? theorem equiv_iff_TPequiv : φ ≡ ψ ↔ ∀ ℓ : TP α, φ ⋀ signature α ℓ ≡ ψ ⋀ signature α ℓ := by @@ -270,15 +270,16 @@ theorem P_goes_down : γ ∈ δ → δ ∈ P α ℓ → (if α.isAtomic then γ case nil => exfalso; cases γ_in case cons => - simp_all only [false_or] - rcases δ_in with ⟨αs, αs_in, def_δ⟩ + simp only [reduceCtorEq, false_or] at δ_in + rcases δ_in with ⟨αs, ⟨αs_in, αs_not_null⟩, def_δ⟩ cases em (γ ∈ αs) case inl γ_in => - have IH := P_goes_down γ_in αs_in.1 + have IH := P_goes_down γ_in αs_in cases em (α.isAtomic) <;> cases em α.isStar all_goals (simp_all;try linarith) case inr γ_not_in => - have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto + have : γ = (∗α) := by + rw [← def_δ] at γ_in; simp at γ_in; tauto subst_eqs simp case test τ => @@ -746,9 +747,9 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) : simp only [evaluate, and_congr_left_iff, relate] at * intro w_sign_ℓ specialize IHα ?_ - · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop + · simp_all [signature, conEval, testsOfProgram] specialize IHβ ?_ - · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop + · simp_all [signature, conEval, testsOfProgram] -- rewrite using semantics of union and the two IH: have : (∀ (v : W), relate M α w v ∨ relate M β w v → evaluate M v ψ) ↔ ((∀ (v : W), relate M α w v → evaluate M v ψ) @@ -825,9 +826,9 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) : simp only [evaluate, relate, forall_exists_index, and_imp, and_congr_left_iff] at * intro w_sign_ℓ specialize IHα ?_ - · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop + · simp_all [signature, conEval, testsOfProgram] specialize IHβ ?_ - · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop + · simp_all [signature, conEval, testsOfProgram] -- only rewriting with IHα here, but not yet IHβ have : (∀ (v x : W), relate M α w x → relate M β x v → evaluate M v ψ) ↔ ∀ (v : W), relate M α w v → ∀ (v_1 : W), relate M β v v_1 → evaluate M v_1 ψ := by @@ -843,9 +844,12 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) : · tauto · rw [F_mem_iff_neg β ℓ φ] at φ_in_Fβ rcases φ_in_Fβ with ⟨τ, τ_in, def_φ, not_ℓ_τ⟩ - apply w_sign_ℓ _ τ - · simp_all - · simp_all [testsOfProgram] + apply w_sign_ℓ φ + subst def_φ + simp_all only [testsOfProgram] + right + use τ, τ_in + simp_all · subst def_φ apply lhs right @@ -859,7 +863,7 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) : apply IHβ.1 ?_ (⌈⌈δ⌉⌉ψ) <;> clear IHβ · right; aesop · have := lhs (⌈β⌉ψ) - simp at this; apply this; clear this -- sounds like daft punk ;-) + simp only [evaluate] at this; apply this; clear this -- sounds like daft punk ;-) right use [] simp_all diff --git a/lake-manifest.json b/lake-manifest.json index 1ed0589..241517d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f", + "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738", + "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.41", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,20 +55,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620", + "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308", + "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.11.0", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "pdl", diff --git a/lakefile.lean b/lakefile.lean index c2303d5..61849d4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,9 @@ package «pdl» where -- add any package configuration options here require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"v4.11.0" + "https://github.com/leanprover-community/mathlib4.git"@"v4.12.0" + +-- require "marcusrossel" / "egg" @ git "main" @[default_target] lean_lib «Pdl» where diff --git a/lean-toolchain b/lean-toolchain index 5a9c76d..8998520 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0 +leanprover/lean4:v4.12.0