From 7fb3422a10959a999bcbddeec459f0542a4511a3 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 28 Aug 2025 05:00:45 -0400 Subject: [PATCH] add to lakefile.toml --- Cslib/Foundations/Semantics/Lts/Basic.lean | 32 ++----- .../Semantics/Lts/Bisimulation.lean | 92 +++++++------------ Cslib/Foundations/Semantics/Lts/TraceEq.lean | 10 +- Cslib/Languages/CCS/BehaviouralTheory.lean | 24 ++--- .../Languages/CombinatoryLogic/Recursion.lean | 2 +- Cslib/Logics/LinearLogic/CLL/Basic.lean | 2 +- CslibTests/Bisimulation.lean | 1 - CslibTests/Lts.lean | 15 +-- lakefile.toml | 1 + 9 files changed, 54 insertions(+), 125 deletions(-) diff --git a/Cslib/Foundations/Semantics/Lts/Basic.lean b/Cslib/Foundations/Semantics/Lts/Basic.lean index a01d21d5..24b62305 100644 --- a/Cslib/Foundations/Semantics/Lts/Basic.lean +++ b/Cslib/Foundations/Semantics/Lts/Basic.lean @@ -90,9 +90,7 @@ theorem Lts.MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3 := by intro h1 h2 induction h1 - case refl s1' => - simp - apply Lts.MTr.single lts h2 + case refl s1' => exact Lts.MTr.single lts h2 case stepL s1' μ' s2' μs' s3' h1' h3 ih => apply Lts.MTr.stepL · exact h1' @@ -104,9 +102,7 @@ theorem Lts.MTr.comp {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List lts.MTr s1 (μs1 ++ μs2) s3 := by intro h1 h2 induction h1 - case refl => - simp - assumption + case refl => assumption case stepL s1 μ s' μs1' s'' h1' h3 ih => apply Lts.MTr.stepL · exact h1' @@ -218,31 +214,27 @@ def Lts.unionSum {State1} {State2} (lts1 : Lts State1 Label) (lts2 : Lts State2 Sum.isRightP (Function.const Label True) (by - simp [DecidablePred] intro s cases h : s · apply Decidable.isTrue trivial - · simp [Sum.isLeftP] + · simp only [Sum.isLeftP, Sum.isLeft_inr, Bool.false_eq_true] apply Decidable.isFalse trivial) (by intro μ - simp [Function.const] apply Decidable.isTrue trivial) (by - simp [DecidablePred] intro s cases h : s - · simp [Sum.isRightP] + · simp only [Sum.isRightP, Sum.isRight_inl, Bool.false_eq_true] apply Decidable.isFalse trivial · apply Decidable.isTrue trivial) (by intro μ - simp [Function.const] apply Decidable.isTrue trivial) lts1.inl @@ -295,10 +287,10 @@ theorem Lts.deterministic_imageFinite : cases hDet case inl hDet => obtain ⟨s', hDet'⟩ := hDet - simp [hDet'] + simp only [hDet'] apply Set.finite_singleton case inr hDet => - simp [hDet] + simp only [hDet] apply Set.finite_empty /-- A state has an outgoing label `μ` if it has a `μ`-derivative. -/ @@ -320,8 +312,6 @@ def Lts.FiniteState (_ : Lts State Label) : Prop := Finite State /-- Every finite-state Lts is also image-finite. -/ theorem Lts.finiteState_imageFinite (hFinite : lts.FiniteState) : lts.ImageFinite := by - simp [ImageFinite, Image] - simp [FiniteState] at hFinite intro s μ apply @Subtype.finite State hFinite @@ -329,8 +319,6 @@ theorem Lts.finiteState_imageFinite (hFinite : lts.FiniteState) : theorem Lts.finiteState_finitelyBranching (hFiniteLabel : Finite Label) (hFiniteState : lts.FiniteState) : lts.FinitelyBranching := by - simp [FinitelyBranching, OutgoingLabels, HasOutLabel] - simp [FiniteState] at hFiniteState constructor case left => apply Lts.finiteState_imageFinite lts hFiniteState @@ -409,9 +397,7 @@ theorem Lts.strN.trans_τ (h1 : lts.strN n s1 HasTau.τ s2) (h2 : lts.strN m s2 HasTau.τ s3) : lts.strN (n + m) s1 HasTau.τ s3 := by cases h1 - case refl => - simp - exact h2 + case refl => grind case tr n1 sb sb' n2 hstr1 htr hstr2 => have ih := Lts.strN.trans_τ lts hstr2 h2 have conc := Lts.strN.tr hstr1 htr ih @@ -434,9 +420,7 @@ theorem Lts.strN.append (h2 : lts.strN n2 s2 HasTau.τ s3) : lts.strN (n1 + n2) s1 μ s3 := by cases h1 - case refl => - simp - exact h2 + case refl => grind case tr n11 sb sb' n12 hstr1 htr hstr2 => have hsuffix := Lts.strN.trans_τ lts hstr2 h2 have n_eq : n11 + (n12 + n2) + 1 = (n11 + n12 + 1 + n2) := by omega diff --git a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean b/Cslib/Foundations/Semantics/Lts/Bisimulation.lean index 48472146..c5a2796d 100644 --- a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/Lts/Bisimulation.lean @@ -248,7 +248,6 @@ theorem Bisimilarity.is_bisimulation : Bisimulation lts (Bisimilarity lts) := by intro s1 s2 h μ obtain ⟨r, hr, hb⟩ := h have hrBisim := hb - simp [Bisimulation] at hb specialize hb s1 s2 constructor case left => @@ -367,8 +366,6 @@ def BisimulationUpTo (lts : Lts State Label) (r : State → State → Prop) : Pr /-- Any bisimulation up to bisimilarity is a bisimulation. -/ theorem Bisimulation.upTo_bisimulation (r : State → State → Prop) (h : BisimulationUpTo lts r) : Bisimulation lts (Relation.upTo r (Bisimilarity lts)) := by - simp [Bisimulation] - simp [BisimulationUpTo] at h intro s1 s2 hr μ rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩ obtain ⟨r1, hr1, hr1b⟩ := hr1b @@ -434,7 +431,6 @@ theorem Bisimulation.bisim_trace intro s1' hmtr1 cases hmtr1 case stepL s1'' htr hmtr => - simp [Bisimulation] at hb specialize hb s1 s2 hr μ have hf := hb.1 s1'' htr obtain ⟨s2'', htr2, hb2⟩ := hf @@ -455,7 +451,6 @@ theorem Bisimulation.bisim_trace theorem Bisimulation.bisim_traceEq (hb : Bisimulation lts r) (hr : r s1 s2) : s1 ~tr[lts] s2 := by - simp [TraceEq, Lts.traces, setOf] funext μs simp only [eq_iff_iff] constructor @@ -475,7 +470,6 @@ theorem Bisimulation.bisim_traceEq /-- Bisimilarity is included in trace equivalence. -/ theorem Bisimilarity.le_traceEq : Bisimilarity lts ≤ TraceEq lts := by - simp [LE.le] intro s1 s2 h obtain ⟨r, hr, hb⟩ := h apply Bisimulation.bisim_traceEq lts hb hr @@ -502,12 +496,10 @@ theorem Bisimulation.traceEq_not_bisim : let lts := Lts.mk BisimMotTr exists lts intro h - simp [Bisimulation] at h specialize h 1 5 have htreq : (1 ~tr[lts] 5) := by simp [TraceEq] have htraces1 : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -519,27 +511,31 @@ theorem Bisimulation.traceEq_not_bisim : simp case intro.stepL μ sb μs' htr hmtr => cases htr - simp - cases hmtr <;> simp + cases hmtr case one2two.stepL μ sb μs' htr hmtr => - cases htr <;> cases hmtr <;> simp <;> contradiction + cases htr <;> cases hmtr <;> + simp only [↓Char.isValue, Set.mem_insert_iff, reduceCtorEq, List.cons.injEq, + List.cons_ne_self, and_false, Set.mem_singleton_iff, Char.reduceEq, and_true, + or_false, or_true] <;> + contradiction + simp case mpr => intro h1 cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 1 constructor case inr h1 => cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 2 apply Lts.MTr.single; constructor case inr h1 => cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 3 constructor; apply BisimMotTr.one2two; apply Lts.MTr.single; apply BisimMotTr.two2three @@ -549,7 +545,6 @@ theorem Bisimulation.traceEq_not_bisim : constructor; apply BisimMotTr.one2two; apply Lts.MTr.single; apply BisimMotTr.two2four have htraces2 : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -562,18 +557,16 @@ theorem Bisimulation.traceEq_not_bisim : case intro.stepL μ sb μs' htr hmtr => cases htr case five2six => - simp cases hmtr case refl => simp case stepL μ sb μs' htr hmtr => cases htr cases hmtr - case refl => right; left; simp + case refl => simp case stepL μ sb μs' htr hmtr => cases htr case five2eight => - simp cases hmtr case refl => simp @@ -587,19 +580,19 @@ theorem Bisimulation.traceEq_not_bisim : intro h1 cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 5 constructor case inr h1 => cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 6 apply Lts.MTr.single; constructor case inr h1 => cases h1 case inl h1 => - simp [h1] + simp only [h1] exists 7 constructor; apply BisimMotTr.five2six; apply Lts.MTr.single; apply BisimMotTr.six2seven @@ -618,7 +611,6 @@ theorem Bisimulation.traceEq_not_bisim : case five2six => simp [TraceEq] at cih have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -630,9 +622,9 @@ theorem Bisimulation.traceEq_not_bisim : case stepL μ sb μs' htr hmtr => cases htr case two2three => - cases hmtr <;> simp - case stepL μ sb μs' htr hmtr => - cases htr + cases hmtr + case stepL μ sb μs' htr hmtr => cases htr + simp case two2four => cases hmtr case refl => simp @@ -642,12 +634,10 @@ theorem Bisimulation.traceEq_not_bisim : intro h cases h case inl h => - simp exists 2 simp [h] constructor case inr h => - simp cases h case inl h => exists 3; simp [h]; constructor; constructor; constructor @@ -657,7 +647,6 @@ theorem Bisimulation.traceEq_not_bisim : simp [h] constructor; constructor; constructor have htraces6 : lts.traces 6 = {[], ['b']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -668,28 +657,25 @@ theorem Bisimulation.traceEq_not_bisim : case refl => simp case stepL μ sb μs' htr hmtr => cases htr - cases hmtr <;> simp - case stepL μ sb μs' htr hmtr => - cases htr + cases hmtr + case stepL μ sb μs' htr hmtr => cases htr + simp case mpr => intro h cases h case inl h => - simp exists 6 simp [h] constructor case inr h => - simp exists 7 simp at h simp [h] constructor; constructor; constructor grind case five2eight => - simp [TraceEq] at cih + simp only [TraceEq] at cih have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -701,9 +687,9 @@ theorem Bisimulation.traceEq_not_bisim : case stepL μ sb μs' htr hmtr => cases htr case two2three => - cases hmtr <;> simp - case stepL μ sb μs' htr hmtr => - cases htr + cases hmtr + case stepL μ sb μs' htr hmtr => cases htr + simp case two2four => cases hmtr case refl => simp @@ -713,12 +699,10 @@ theorem Bisimulation.traceEq_not_bisim : intro h cases h case inl h => - simp exists 2 simp [h] constructor case inr h => - simp cases h case inl h => exists 3; simp [h]; constructor; constructor; constructor @@ -728,7 +712,6 @@ theorem Bisimulation.traceEq_not_bisim : simp [h] constructor; constructor; constructor have htraces8 : lts.traces 8 = {[], ['c']} := by - simp [Lts.traces] apply Set.ext_iff.2 intro μs apply Iff.intro @@ -739,23 +722,21 @@ theorem Bisimulation.traceEq_not_bisim : case refl => simp case stepL μ sb μs' htr hmtr => cases htr - cases hmtr <;> simp - case stepL μ sb μs' htr hmtr => - cases htr + cases hmtr + case stepL μ sb μs' htr hmtr => cases htr + simp case mpr => intro h cases h case inl h => - simp exists 8 simp [h] constructor case inr h => - simp exists 9 simp at h simp [h] - constructor; constructor; constructor + repeat constructor rw [htraces2, htraces8] at cih apply Set.ext_iff.1 at cih specialize cih ['b'] @@ -771,7 +752,6 @@ theorem Bisimilarity.bisimilarity_neq_traceEq : ∃ (State : Type) (Label : Type) (lts : Lts State Label), Bisimilarity lts ≠ TraceEq lts := by obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim exists State; exists Label; exists lts - simp intro heq have hb := Bisimilarity.is_bisimulation lts rw [heq] at hb @@ -814,7 +794,7 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq (lts : Lts State Label) (hdet : lts.Deterministic) : Bisimilarity lts = TraceEq lts := by funext s1 s2 - simp [eq_iff_iff] + simp only [eq_iff_iff] constructor case mp => apply Bisimilarity.le_traceEq @@ -888,7 +868,6 @@ theorem SWBisimulation.follow_internal_fst_n cases hstrN rename_i n1 sb sb' n2 hstrN1 htr hstrN2 let hswb_m := hswb - simp [SWBisimulation] at hswb have ih1 := SWBisimulation.follow_internal_fst_n lts r hswb hr hstrN1 obtain ⟨sb2, hstrs2, hrsb⟩ := ih1 have h := (hswb sb sb2 hrsb HasTau.τ).1 sb' htr @@ -916,7 +895,6 @@ theorem SWBisimulation.follow_internal_snd_n cases hstrN rename_i n1 sb sb' n2 hstrN1 htr hstrN2 let hswb_m := hswb - simp [SWBisimulation] at hswb have ih1 := SWBisimulation.follow_internal_snd_n lts r hswb hr hstrN1 obtain ⟨sb1, hstrs1, hrsb⟩ := ih1 have h := (hswb sb1 sb hrsb HasTau.τ).2 sb' htr @@ -954,8 +932,6 @@ theorem WeakBisimulation.iff_swBisimulation apply Iff.intro case mp => intro h - simp [WeakBisimulation, Bisimulation] at h - simp [SWBisimulation] intro s1 s2 hr μ apply And.intro case left => @@ -972,7 +948,6 @@ theorem WeakBisimulation.iff_swBisimulation exists s1' case mpr => intro h - simp [WeakBisimulation, Bisimulation] intro s1 s2 hr μ apply And.intro case left => @@ -988,8 +963,7 @@ theorem WeakBisimulation.iff_swBisimulation obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst lts r h hrb' hstr2 exists s2' constructor - · simp [Lts.saturate] - apply Lts.STr.comp lts hstr2b hstr2b' hstr2' + · exact Lts.STr.comp lts hstr2b hstr2b' hstr2' · exact hrb2 case right => intro s2' hstr @@ -1004,8 +978,7 @@ theorem WeakBisimulation.iff_swBisimulation obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd lts r h hrb' hstr2 exists s1' constructor - · simp [Lts.saturate] - apply Lts.STr.comp lts hstr1b hstr1b' hstr1' + · exact Lts.STr.comp lts hstr1b hstr1b' hstr1' · exact hrb2 theorem WeakBisimulation.toSwBisimulation @@ -1029,7 +1002,7 @@ theorem WeakBisimilarity.by_swBisimulation [HasTau Label] theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State Label) : WeakBisimilarity lts = SWBisimilarity lts := by funext s1 s2 - simp [WeakBisimilarity, SWBisimilarity] + simp only [eq_iff_iff] constructor case mp => intro h @@ -1048,7 +1021,6 @@ theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State La /-- sw-bisimilarity is reflexive. -/ theorem SWBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : s ≈sw[lts] s := by - simp [SWBisimilarity] exists Eq constructor · rfl diff --git a/Cslib/Foundations/Semantics/Lts/TraceEq.lean b/Cslib/Foundations/Semantics/Lts/TraceEq.lean index 7ac979ba..0ecd49e0 100644 --- a/Cslib/Foundations/Semantics/Lts/TraceEq.lean +++ b/Cslib/Foundations/Semantics/Lts/TraceEq.lean @@ -39,8 +39,7 @@ def Lts.traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } /-- If there is a multi-step transition from `s` labelled by `μs`, then `μs` is in the traces of `s`. -/ theorem Lts.traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : - μs ∈ lts.traces s := by - simp [Lts.traces] + μs ∈ lts.traces s := by exists s' /-- Two states are trace equivalent if they have the same set of traces. -/ @@ -68,9 +67,7 @@ theorem TraceEq.symm (lts : Lts State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2 /-- Trace equivalence is transitive. -/ theorem TraceEq.trans {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts] s3) : s1 ~tr[lts] s3 := by - simp only [TraceEq] - simp only [TraceEq] at h1 - simp only [TraceEq] at h2 + simp only [TraceEq] at * rw [h1, h2] /-- Trace equivalence is an equivalence relation. -/ @@ -90,7 +87,6 @@ theorem TraceEq.deterministic_sim ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2' := by intro μ s1' htr1 have hmtr1 := Lts.MTr.single lts htr1 - simp [TraceEq] at h have hin := Lts.traces_in lts s1 [μ] s1' hmtr1 rw [h] at hin obtain ⟨s2', hmtr2⟩ := hin @@ -108,7 +104,6 @@ theorem TraceEq.deterministic_sim have hmtr1comp := Lts.MTr.comp lts hmtr1 hmtr1' have hin := Lts.traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp rw [h] at hin - simp [Lts.traces] at hin obtain ⟨s', hmtr2'⟩ := hin cases hmtr2' case stepL s2'' htr2 hmtr2' => @@ -123,7 +118,6 @@ theorem TraceEq.deterministic_sim have hmtr2comp := Lts.MTr.comp lts hmtr2 hmtr2' have hin := Lts.traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp rw [← h] at hin - simp [Lts.traces] at hin obtain ⟨s', hmtr1'⟩ := hin cases hmtr1' case stepL s1'' htr1 hmtr1' => diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 15e5ab18..404a956d 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -420,15 +420,9 @@ theorem bisimilarity_congr (c : Context Name Constant) (p q : Process Name Constant) (h : p ~[@lts Name Constant defs] q) : (c.fill p) ~[@lts Name Constant defs] (c.fill q) := by induction c - case hole => - simp only [Context.fill] - exact h - case pre μ c ih => - simp [Context.fill] - apply bisimilarity_congr_pre ih - case parL c r ih => - simp [Context.fill] - apply bisimilarity_congr_par ih + case hole => exact h + case pre _ _ ih => exact bisimilarity_congr_pre ih + case parL _ _ ih => exact bisimilarity_congr_par ih case parR r c ih => apply Bisimilarity.trans · apply bisimilarity_par_comm @@ -436,20 +430,14 @@ theorem bisimilarity_congr · apply bisimilarity_congr_par exact ih · apply bisimilarity_par_comm - case choiceL c r ih => - simp [Context.fill] - apply bisimilarity_congr_choice - exact ih + case choiceL _ _ ih => exact bisimilarity_congr_choice ih case choiceR r c ih => - simp [Context.fill] apply Bisimilarity.trans · apply bisimilarity_choice_comm · apply Bisimilarity.trans - · apply bisimilarity_congr_choice - exact ih - · apply bisimilarity_choice_comm + · exact bisimilarity_congr_choice ih + · exact bisimilarity_choice_comm case res => - simp [Context.fill] apply bisimilarity_congr_res assumption diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index 8bd68808..1c5e3ef8 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -374,7 +374,7 @@ theorem le_def (a b : SKI) : SKI.LE ⬝ a ⬝ b ⇒* IsZero ⬝ (SKI.Sub ⬝ a theorem le_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : IsBool (n ≤ m) (SKI.LE ⬝ a ⬝ b) := by - simp [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] + simp only [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] apply isBool_trans (a' := IsZero ⬝ (SKI.Sub ⬝ a ⬝ b)) (h := le_def _ _) apply isZero_correct apply sub_correct <;> assumption diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 64a79502..60ae3e0c 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -266,7 +266,7 @@ theorem subst_eqv_head {Γ : Sequent Atom} {a b : Proposition Atom} (heqv : a an equivalent proposition. -/ theorem subst_eqv {Γ Δ : Sequent Atom} {a b : Proposition Atom} (heqv : a ≡ b) : ⊢(Γ ++ [a] ++ Δ) → ⊢(Γ ++ [b] ++ Δ) := by - simp + simp only [List.append_assoc, List.cons_append, List.nil_append] intro h apply Proof.exchange (List.perm_middle.symm) apply Proof.exchange (List.perm_middle) at h diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean index d3869954..5b2f3818 100644 --- a/CslibTests/Bisimulation.lean +++ b/CslibTests/Bisimulation.lean @@ -28,7 +28,6 @@ private inductive Bisim15 : ℕ → ℕ → Prop where example : 1 ~[lts1] 5 := by exists Bisim15 apply And.intro; constructor - simp [Bisimulation] intro s1 s2 hr μ constructor case left => diff --git a/CslibTests/Lts.lean b/CslibTests/Lts.lean index 10f0bb12..4f292dc2 100644 --- a/CslibTests/Lts.lean +++ b/CslibTests/Lts.lean @@ -33,8 +33,7 @@ example : 1 ~[natLts] 2 := by exists NatBisim constructor · constructor - · simp [Bisimulation] - intro s1 s2 hr μ + · intro s1 s2 hr μ constructor · intro s1' htr cases htr <;> (cases hr <;> repeat constructor) @@ -57,31 +56,23 @@ def natInfiniteExecution : Stream' ℕ := fun n => n theorem natInfiniteExecution.infiniteExecution : natDivLts.DivergentExecution natInfiniteExecution := by - simp [Lts.DivergentExecution] intro n constructor example : natDivLts.Divergent 0 := by - simp [Lts.Divergent] exists natInfiniteExecution constructor; constructor exact natInfiniteExecution.infiniteExecution example : natDivLts.Divergent 3 := by - simp [Lts.Divergent] exists natInfiniteExecution.drop 3 - simp [Stream'.drop] constructor · constructor - · simp [Lts.DivergentExecution] - simp [Stream'.drop] - intro n - constructor + · intro; constructor example : natDivLts.Divergent n := by - simp [Lts.Divergent] exists natInfiniteExecution.drop n - simp [Stream'.drop] + simp only [Stream'.drop, zero_add] constructor · constructor · apply Lts.divergent_drop diff --git a/lakefile.toml b/lakefile.toml index 225d1be1..020fe1c6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,6 +5,7 @@ testDriver = "CslibTests" [leanOptions] weak.linter.mathlibStandardSet = true +weak.linter.flexible = true [[require]] name = "mathlib"