diff --git a/Cslib/Computability/Languages/ExampleEventuallyZero.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean index 7e03b8cfd..dc777d9a8 100644 --- a/Cslib/Computability/Languages/ExampleEventuallyZero.lean +++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean @@ -26,22 +26,22 @@ namespace Cslib.ωLanguage.Example open scoped LTS NA -/-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/ +/-- A sequence `xs` is in `eventuallyZero` iff `xs k = 0` for all large `k`. -/ @[scoped grind =] -def eventually_zero : ωLanguage (Fin 2) := +def eventuallyZero : ωLanguage (Fin 2) := { xs : ωSequence (Fin 2) | ∀ᶠ k in atTop, xs k = 0 } -/-- `eventually_zero` is accepted by a 2-state nondeterministic Buchi automaton. -/ +/-- `eventuallyZero` is accepted by a 2-state nondeterministic Buchi automaton. -/ @[scoped grind =] -def eventually_zero_na : NA.Buchi (Fin 2) (Fin 2) where +def eventuallyZeroNa : NA.Buchi (Fin 2) (Fin 2) where -- Once state 1 is reached, only symbol 0 is accepted and the next state is still 1 Tr s x s' := s = 1 → x = 0 ∧ s' = 1 start := {0} accept := {1} -theorem eventually_zero_accepted_by_na_buchi : - language eventually_zero_na = eventually_zero := by - ext xs; unfold eventually_zero_na; constructor +theorem eventuallyZero_accepted_by_na_buchi : + language eventuallyZeroNa = eventuallyZero := by + ext xs; unfold eventuallyZeroNa; constructor · rintro ⟨ss, h_run, h_acc⟩ obtain ⟨m, h_m⟩ := Frequently.exists h_acc apply eventually_atTop.mpr @@ -61,27 +61,27 @@ theorem eventually_zero_accepted_by_na_buchi : grind private lemma extend_by_zero (u : List (Fin 2)) : - u ++ω const 0 ∈ eventually_zero := by + u ++ω const 0 ∈ eventuallyZero := by apply eventually_atTop.mpr use u.length grind [get_append_right'] private lemma extend_by_one (u : List (Fin 2)) : - ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by + ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventuallyZero := by use [1] grind [extend_by_zero] -private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventually_zero) +private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventuallyZero) (u : List (Fin 2)) : ∃ v, 1 ∈ v ∧ u ++ v ∈ l := by obtain ⟨v, _, h_pfx⟩ := extend_by_one u rw [← h] at h_pfx have := frequently_atTop.mp h_pfx (u ++ v).length grind [extract_append_zero_right] -private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) := +private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventuallyZero) (n : ℕ) := Classical.choose <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten -private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) : +private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventuallyZero) (n : ℕ) : 1 ∈ oneSegs h n ∧ (List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k)).flatten ∈ l := by let P u v := 1 ∈ v ∧ u ++ v ∈ l have : P ((List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten) (oneSegs h n) := by @@ -92,13 +92,13 @@ private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero rw [List.ofFn_succ_last] simpa -theorem eventually_zero_not_omegaLim : - ¬ ∃ l : Language (Fin 2), l↗ω = eventually_zero := by +theorem eventuallyZero_not_omegaLim : + ¬ ∃ l : Language (Fin 2), l↗ω = eventuallyZero := by rintro ⟨l, h⟩ let ls := ωSequence.mk (oneSegs h) have h_segs := oneSegs_lemma h have h_pos : ∀ k, (ls k).length > 0 := by grind - have h_ev : ls.flatten ∈ eventually_zero := by + have h_ev : ls.flatten ∈ eventuallyZero := by rw [← h, mem_omegaLim, frequently_iff_strictMono] use (fun k ↦ ls.cumLen (k + 1)) constructor diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 1657c89e2..f3e799c63 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -61,11 +61,11 @@ where the automaton is not even required to be finite-state. -/ theorem IsRegular.not_da_buchi : ∃ (Symbol : Type) (p : ωLanguage Symbol), p.IsRegular ∧ ¬ ∃ (State : Type) (da : DA.Buchi State Symbol), language da = p := by - refine ⟨Fin 2, Example.eventually_zero, ?_, ?_⟩ - · use Fin 2, inferInstance, Example.eventually_zero_na, - Example.eventually_zero_accepted_by_na_buchi + refine ⟨Fin 2, Example.eventuallyZero, ?_, ?_⟩ + · use Fin 2, inferInstance, Example.eventuallyZeroNa, + Example.eventuallyZero_accepted_by_na_buchi · rintro ⟨State, ⟨da, acc⟩, _⟩ - have := Example.eventually_zero_not_omegaLim + have := Example.eventuallyZero_not_omegaLim grind [DA.buchi_eq_finAcc_omegaLim] /-- The ω-limit of a regular language is ω-regular. -/ diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 477ab60b1..b956b6286 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -160,27 +160,27 @@ def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, Bi /-- The space used by a configuration is the space used by its tape. -/ -def Cfg.space_used (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used +def Cfg.spaceUsed (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.spaceUsed @[scoped grind =] -lemma Cfg.space_used_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : - (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s +lemma Cfg.spaceUsed_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : + (tm.initCfg s).spaceUsed = max 1 s.length := BiTape.spaceUsed_mk₁ s @[scoped grind =] -lemma Cfg.space_used_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : - (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s +lemma Cfg.spaceUsed_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : + (tm.haltCfg s).spaceUsed = max 1 s.length := BiTape.spaceUsed_mk₁ s -lemma Cfg.space_used_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg) - (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by +lemma Cfg.spaceUsed_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg) + (hstep : tm.step cfg = some cfg') : cfg'.spaceUsed ≤ cfg.spaceUsed + 1 := by obtain ⟨_ | q, tape⟩ := cfg · simp [step] at hstep · simp only [step] at hstep generalize hM : tm.tr q tape.head = result at hstep obtain ⟨⟨wr, dir⟩, q''⟩ := result cases hstep; cases dir with - | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] - | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using - BiTape.space_used_move (tape.write wr) d + | none => simp [Cfg.spaceUsed, BiTape.optionMove, BiTape.spaceUsed_write, hM] + | some d => simpa [Cfg.spaceUsed, BiTape.optionMove, BiTape.spaceUsed_write, hM] using + BiTape.spaceUsed_move (tape.write wr) d end Cfg @@ -215,8 +215,8 @@ lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by obtain ⟨steps, hsteps_le, hevals⟩ := h - grind [hevals.apply_le_apply_add (Cfg.space_used tm) - fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)] + grind [hevals.apply_le_apply_add (Cfg.spaceUsed tm) + fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)] section Computers @@ -392,15 +392,15 @@ structure TimeComputable (f : List Symbol → List Symbol) where /-- the underlying bundled SingleTapeTM -/ tm : SingleTapeTM Symbol /-- a bound on runtime -/ - time_bound : ℕ → ℕ - /-- proof this machine outputs `f` in at most `time_bound(input.length)` steps -/ - outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (time_bound a.length) + timeBound : ℕ → ℕ + /-- proof this machine outputs `f` in at most `timeBound(input.length)` steps -/ + outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (timeBound a.length) /-- The identity map on Symbol is computable in constant time. -/ def TimeComputable.id : TimeComputable (Symbol := Symbol) id where tm := idComputer - time_bound _ := 1 + timeBound _ := 1 outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩ /-- @@ -419,36 +419,36 @@ then the time bound for the second machine still holds for that shorter input to -/ def TimeComputable.comp {f g : List Symbol → List Symbol} (hf : TimeComputable f) (hg : TimeComputable g) - (h_mono : Monotone hg.time_bound) : + (h_mono : Monotone hg.timeBound) : (TimeComputable (g ∘ f)) where tm := compComputer hf.tm hg.tm -- perhaps it would be good to track the blow up separately? - time_bound l := (hf.time_bound l) + hg.time_bound (max 1 l + hf.time_bound l) + timeBound l := (hf.timeBound l) + hg.timeBound (max 1 l + hf.timeBound l) outputsFunInTime a := by have hf_outputsFun := hf.outputsFunInTime a have hg_outputsFun := hg.outputsFunInTime (f a) simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, haltCfg] at hg_outputsFun hf_outputsFun ⊢ - -- The computer reduces a to f a in time hf.time_bound a.length + -- The computer reduces a to f a in time hf.timeBound a.length have h_a_reducesTo_f_a : RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation (initialCfg hf.tm hg.tm a) (intermediateCfg hf.tm hg.tm (f a)) - (hf.time_bound a.length) := + (hf.timeBound a.length) := comp_left_relatesWithinSteps hf.tm hg.tm a (f a) - (hf.time_bound a.length) hf_outputsFun - -- The computer reduces f a to g (f a) in time hg.time_bound (f a).length + (hf.timeBound a.length) hf_outputsFun + -- The computer reduces f a to g (f a) in time hg.timeBound (f a).length have h_f_a_reducesTo_g_f_a : RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation (intermediateCfg hf.tm hg.tm (f a)) (finalCfg hf.tm hg.tm (g (f a))) - (hg.time_bound (f a).length) := + (hg.timeBound (f a).length) := comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a)) - (hg.time_bound (f a).length) hg_outputsFun + (hg.timeBound (f a).length) hg_outputsFun -- Therefore, the computer reduces a to g (f a) in the sum of those times. have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a - refine Nat.add_le_add_left ?_ (hf.time_bound a.length) + refine Nat.add_le_add_left ?_ (hf.timeBound a.length) · apply h_mono -- Use the lemma about output length being bounded by input length + time exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a) @@ -478,7 +478,7 @@ structure PolyTimeComputable (f : List Symbol → List Symbol) extends TimeCompu /-- a polynomial time bound -/ poly : Polynomial ℕ /-- proof that this machine outputs `f` in at most `time(input.length)` steps -/ - bounds : ∀ n, time_bound n ≤ poly.eval n + bounds : ∀ n, timeBound n ≤ poly.eval n /-- A proof that the identity map on Symbol is computable in polytime. -/ noncomputable def PolyTimeComputable.id : PolyTimeComputable (Symbol := Symbol) id where @@ -493,7 +493,7 @@ A proof that the composition of two polytime computable functions is polytime co -/ noncomputable def PolyTimeComputable.comp {f g : List Symbol → List Symbol} (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) - (h_mono : Monotone hg.time_bound) : + (h_mono : Monotone hg.timeBound) : PolyTimeComputable (g ∘ f) where toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono poly := hf.poly + hg.poly.comp (1 + X + hf.poly) diff --git a/Cslib/Computability/URM/StraightLine.lean b/Cslib/Computability/URM/StraightLine.lean index bde52823e..750a8c51d 100644 --- a/Cslib/Computability/URM/StraightLine.lean +++ b/Cslib/Computability/URM/StraightLine.lean @@ -20,7 +20,7 @@ they always halt exactly at their length. ## Main results - `straight_line_halts`: straight-line programs always halt -- `straightLine_finalState`: final state after running a straight-line program +- `straightLinefinalState`: final state after running a straight-line program -/ @[expose] public section @@ -100,27 +100,27 @@ theorem straight_line_halts {p : Program} (hsl : p.IsStraightLine) (inputs : Lis /-- The halting state for a straight-line program starting from registers r. Wraps Classical.choose to hide it from the API. -/ -noncomputable def straightLine_finalState {p : Program} +noncomputable def straightLinefinalState {p : Program} (hsl : p.IsStraightLine) (r : Regs) : State := Classical.choose (straight_line_halts_from_regs hsl r) -/-- Specification: the state from straightLine_finalState satisfies Steps, isHalted, +/-- Specification: the state from straightLinefinalState satisfies Steps, isHalted, and has pc = p.length. -/ -theorem straightLine_finalState_spec {p : Program} (hsl : p.IsStraightLine) (r : Regs) : - let s := straightLine_finalState hsl r +theorem straightLinefinalState_spec {p : Program} (hsl : p.IsStraightLine) (r : Regs) : + let s := straightLinefinalState hsl r Steps p ⟨0, r⟩ s ∧ s.isHalted p ∧ s.pc = p.length := Classical.choose_spec (straight_line_halts_from_regs hsl r) /-- The final registers after running a straight-line program from given starting registers. -/ -noncomputable def straightLine_finalRegs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : Regs := - (straightLine_finalState hsl r).regs +noncomputable def straightLineFinalRegs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : Regs := + (straightLinefinalState hsl r).regs -/-- For a straight-line program, s.regs equals straightLine_finalRegs if halted from r. -/ -theorem straightLine_finalRegs_eq_of_halted {p : Program} (hsl : p.IsStraightLine) +/-- For a straight-line program, s.regs equals straightLineFinalRegs if halted from r. -/ +theorem straightLineFinalRegs_eq_of_halted {p : Program} (hsl : p.IsStraightLine) (r : Regs) (s : State) (hsteps : Steps p ⟨0, r⟩ s) (hhalted : s.isHalted p) : - s.regs = straightLine_finalRegs hsl r := - Steps.eq_of_halts hsteps hhalted (straightLine_finalState_spec hsl r).1 - (straightLine_finalState_spec hsl r).2.1 ▸ rfl + s.regs = straightLineFinalRegs hsl r := + Steps.eq_of_halts hsteps hhalted (straightLinefinalState_spec hsl r).1 + (straightLinefinalState_spec hsl r).2.1 ▸ rfl /-- In a straight-line program, we can characterize the state at any intermediate pc. This gives us the state after executing instructions 0..pc-1. -/ diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index ba7160556..e61272d57 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -33,7 +33,7 @@ will not collide. * `BiTape`: A tape with a head symbol and left/right contents stored as `StackTape` * `BiTape.move`: Move the tape head left or right * `BiTape.write`: Write a symbol at the current head position -* `BiTape.space_used`: The space used by the tape +* `BiTape.spaceUsed`: The space used by the tape -/ @[expose] public section @@ -76,28 +76,28 @@ with the head under the first element of the list if it exists. def mk₁ (l : List Symbol) : BiTape Symbol := match l with | [] => ∅ - | h :: t => { head := some h, left := ∅, right := StackTape.map_some t } + | h :: t => { head := some h, left := ∅, right := StackTape.mapSome t } section Move /-- Move the head left by shifting the left StackTape under the head. -/ -def move_left (t : BiTape Symbol) : BiTape Symbol := +def moveLeft (t : BiTape Symbol) : BiTape Symbol := ⟨t.left.head, t.left.tail, StackTape.cons t.head t.right⟩ /-- Move the head right by shifting the right StackTape under the head. -/ -def move_right (t : BiTape Symbol) : BiTape Symbol := +def moveRight (t : BiTape Symbol) : BiTape Symbol := ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩ /-- Move the head to the left or right, shifting the tape underneath it. -/ def move (t : BiTape Symbol) : Dir → BiTape Symbol - | .left => t.move_left - | .right => t.move_right + | .left => t.moveLeft + | .right => t.moveRight /-- Optionally perform a `move`, or do nothing if `none`. @@ -107,12 +107,12 @@ def optionMove : BiTape Symbol → Option Dir → BiTape Symbol | t, some d => t.move d @[simp] -lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := by - simp [move_right, move_left] +lemma moveLeft_moveRight (t : BiTape Symbol) : t.moveLeft.moveRight = t := by + simp [moveRight, moveLeft] @[simp] -lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by - simp [move_left, move_right] +lemma moveRight_moveLeft (t : BiTape Symbol) : t.moveRight.moveLeft = t := by + simp [moveLeft, moveRight] end Move @@ -126,22 +126,22 @@ The space used by a `BiTape` is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`. -/ @[scoped grind] -def space_used (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length +def spaceUsed (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length @[simp, grind =] -lemma space_used_write (t : BiTape Symbol) (a : Option Symbol) : - (t.write a).space_used = t.space_used := by rfl +lemma spaceUsed_write (t : BiTape Symbol) (a : Option Symbol) : + (t.write a).spaceUsed = t.spaceUsed := by rfl -lemma space_used_mk₁ (l : List Symbol) : - (mk₁ l).space_used = max 1 l.length := by +lemma spaceUsed_mk₁ (l : List Symbol) : + (mk₁ l).spaceUsed = max 1 l.length := by cases l with - | nil => simp [mk₁, space_used, nil, StackTape.length_nil] - | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega + | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil] + | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_mapSome]; omega -lemma space_used_move (t : BiTape Symbol) (d : Dir) : - (t.move d).space_used ≤ t.space_used + 1 := by - cases d <;> grind [move_left, move_right, move, - space_used, StackTape.length_tail_le, StackTape.length_cons_le] +lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) : + (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by + cases d <;> grind [moveLeft, moveRight, move, + spaceUsed, StackTape.length_tail_le, StackTape.length_cons_le] end BiTape diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index 689fe0a26..6c095a334 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -134,7 +134,7 @@ instance HasFresh.to_infinite (α : Type u) [HasFresh α] : Infinite α := by /-- All infinite types have an associated (at least noncomputable) fresh function. This, in conjunction with `HasFresh.to_infinite`, characterizes `HasFresh`. -/ -noncomputable instance HasFresh.of_infinite (α : Type u) [Infinite α] : HasFresh α where +noncomputable instance (α : Type u) [Infinite α] : HasFresh α where fresh s := Infinite.exists_notMem_finset s |>.choose fresh_notMem s := by grind diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 29635bee6..4ff14dfb0 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -294,21 +294,19 @@ theorem ChurchRosser.normal_eq (cr : ChurchRosser r) (nx : Normal r x) (ny : Nor /-- A pair of subrelations lifts to transitivity on the relation. -/ @[implicit_reducible] -def trans_of_subrelation (s s' r : α → α → Prop) (hr : IsTrans α r) - (h : Subrelation s r) (h' : Subrelation s' r) : Trans s s' r where - trans hab hbc := hr.trans _ _ _ (h hab) (h' hbc) +def transLeftRight (s s' r : α → α → Prop) [IsTrans α r] (h : s ≤ r) (h' : s' ≤ r) : + Trans s s' r where + trans hab hbc := _root_.trans (h _ _ hab) (h' _ _ hbc) /-- A subrelation lifts to transitivity on the left of the relation. -/ @[implicit_reducible] -def trans_of_subrelation_left (s r : α → α → Prop) (hr : IsTrans α r) - (h : Subrelation s r) : Trans s r r where - trans hab hbc := hr.trans _ _ _ (h hab) hbc +def transLeft (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s r r where + trans hab hbc := _root_.trans (h _ _ hab) hbc /-- A subrelation lifts to transitivity on the right of the relation. -/ @[implicit_reducible] -def trans_of_subrelation_right (s r : α → α → Prop) (hr : IsTrans α r) - (h : Subrelation s r) : Trans r s r where - trans hab hbc := hr.trans _ _ _ hab (h hbc) +def transRight (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r where + trans hab hbc := _root_.trans hab (h _ _ hbc) /-- Confluence implies that multi-step joinability is an equivalence. -/ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) : @@ -559,7 +557,7 @@ theorem Commute.join_confluent (c₁ : Confluent r₁) (c₂ : Confluent r₂) ( exact ⟨w, yw, cz.trans zw⟩ /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/ -theorem reflTransGen_mono_closed (h₁ : Subrelation r₁ r₂) (h₂ : Subrelation r₂ (ReflTransGen r₁)) : +theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) : ReflTransGen r₁ = ReflTransGen r₂ := by ext exact ⟨ReflTransGen.mono @h₁, reflTransGen_closed @h₂⟩ @@ -638,10 +636,10 @@ macro_rules def PredReduction (a b : ℕ) : Prop := a = b + 1 ``` -/ -syntax (name := reduction_sys) "reduction_sys" (ppSpace str)? : attr +syntax (name := reductionSys) "reduction_sys" (ppSpace str)? : attr initialize Lean.registerBuiltinAttribute { - name := `reduction_sys + name := `reductionSys descr := "Register notation for a relation and its closures." add := fun decl stx _ => MetaM.run' do let currNamespace ← getCurrNamespace diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index f495d897a..a252582b0 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -140,7 +140,7 @@ lemma cons_head_tail (l : StackTape Symbol) : /-- Create a `StackTape` from a list by mapping all elements to `some` -/ @[scoped grind] -def map_some (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ +def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ section Length @@ -169,7 +169,7 @@ lemma length_cons_le (o : Option Symbol) (l : StackTape Symbol) : cases o <;> grind @[simp, scoped grind =] -lemma length_map_some (l : List Symbol) : (map_some l).length = l.length := by grind +lemma length_mapSome (l : List Symbol) : (mapSome l).length = l.length := by grind @[simp, scoped grind =] lemma length_nil : (nil : StackTape Symbol).length = 0 := by grind diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean index e08755f01..7f6c0d332 100644 --- a/Cslib/Foundations/Logic/LogicalEquivalence.lean +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -26,7 +26,7 @@ class LogicalEquivalence /-- Proof that `eqv` is a congruence. -/ [congruence : Congruence Proposition eqv] /-- Validity is preserved for any judgemental context. -/ - eqv_fill_valid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition) + eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition) (h : Valid (c<[a])) : Valid (c<[b]) @[inherit_doc] diff --git a/Cslib/Foundations/Semantics/LTS/Notation.lean b/Cslib/Foundations/Semantics/LTS/Notation.lean index ea71ec88e..59198c133 100644 --- a/Cslib/Foundations/Semantics/LTS/Notation.lean +++ b/Cslib/Foundations/Semantics/LTS/Notation.lean @@ -77,10 +77,10 @@ macro_rules ) /-- This attribute calls the `lts_transition_notation` command for the annotated declaration. -/ -syntax (name := lts_attr) "lts" ident (ppSpace str)? : attr +syntax (name := ltsAttr) "lts" ident (ppSpace str)? : attr initialize Lean.registerBuiltinAttribute { - name := `lts_attr + name := `ltsAttr descr := "Register notation for an LTS" add := fun decl stx _ => MetaM.run' do let currNamespace ← getCurrNamespace diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index d8df3b227..d78dd6eb3 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -68,17 +68,17 @@ variable {Γ Δ : Context α β} /-- A mapping of values within a context. -/ @[simp, scoped grind] -def map_val (f : β → β) (Γ : Context α β) : Context α β := +def mapVal (f : β → β) (Γ : Context α β) : Context α β := Γ.map (fun ⟨var,ty⟩ => ⟨var,f ty⟩) omit [DecidableEq α] in /-- A mapping of values preserves keys. -/ @[scoped grind .] -lemma map_val_keys (f) : Γ.keys = (Γ.map_val f).keys := by +lemma mapVal_keys (f) : Γ.keys = (Γ.mapVal f).keys := by induction Γ <;> grind /-- A mapping of values maps lookups. -/ -lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dlookup x := by +lemma mapVal_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.mapVal f).dlookup x := by induction Γ <;> grind end LambdaCalculus.LocallyNameless.Context diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean index 2b7483d3d..51098b693 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean @@ -90,21 +90,21 @@ def Binding.fv : Binding Var → Finset Var /-- Free type variables of a term. -/ @[scoped grind =] -def Term.fv_ty : Term Var → Finset Var +def Term.fvTy : Term Var → Finset Var | bvar _ | fvar _ => {} -| abs σ t₁ | tabs σ t₁ | tapp t₁ σ => σ.fv ∪ t₁.fv_ty -| inl t₁ | inr t₁ => t₁.fv_ty -| app t₁ t₂ | let' t₁ t₂ => t₁.fv_ty ∪ t₂.fv_ty -| case t₁ t₂ t₃ => t₁.fv_ty ∪ t₂.fv_ty ∪ t₃.fv_ty +| abs σ t₁ | tabs σ t₁ | tapp t₁ σ => σ.fv ∪ t₁.fvTy +| inl t₁ | inr t₁ => t₁.fvTy +| app t₁ t₂ | let' t₁ t₂ => t₁.fvTy ∪ t₂.fvTy +| case t₁ t₂ t₃ => t₁.fvTy ∪ t₂.fvTy ∪ t₃.fvTy /-- Free term variables of a term. -/ @[scoped grind =] -def Term.fv_tm : Term Var → Finset Var +def Term.fvTm : Term Var → Finset Var | bvar _ => {} | fvar x => {x} -| abs _ t₁ | tabs _ t₁ | tapp t₁ _ | inl t₁ | inr t₁ => t₁.fv_tm -| app t₁ t₂ | let' t₁ t₂ => t₁.fv_tm ∪ t₂.fv_tm -| case t₁ t₂ t₃ => t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm +| abs _ t₁ | tabs _ t₁ | tapp t₁ _ | inl t₁ | inr t₁ => t₁.fvTm +| app t₁ t₂ | let' t₁ t₂ => t₁.fvTm ∪ t₂.fvTm +| case t₁ t₂ t₃ => t₁.fvTm ∪ t₂.fvTm ∪ t₃.fvTm /-- A context of bindings. -/ abbrev Env (Var : Type*) := Context Var (Binding Var) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean index 489791ddc..1d7060916 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -144,51 +144,51 @@ open scoped Ty /-- Variable opening (term opening to type) of the ith bound variable. -/ @[scoped grind =] -def openRec_ty (X : ℕ) (δ : Ty Var) : Term Var → Term Var +def openRecTy (X : ℕ) (δ : Ty Var) : Term Var → Term Var | bvar x => bvar x | fvar x => fvar x -| abs σ t₁ => abs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty X δ t₁) -| app t₁ t₂ => app (openRec_ty X δ t₁) (openRec_ty X δ t₂) -| tabs σ t₁ => tabs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty (X + 1) δ t₁) -| tapp t₁ σ => tapp (openRec_ty X δ t₁) (σ⟦X ↝ δ⟧ᵞ) -| let' t₁ t₂ => let' (openRec_ty X δ t₁) (openRec_ty X δ t₂) -| inl t₁ => inl (openRec_ty X δ t₁) -| inr t₂ => inr (openRec_ty X δ t₂) -| case t₁ t₂ t₃ => case (openRec_ty X δ t₁) (openRec_ty X δ t₂) (openRec_ty X δ t₃) +| abs σ t₁ => abs (σ⟦X ↝ δ⟧ᵞ) (openRecTy X δ t₁) +| app t₁ t₂ => app (openRecTy X δ t₁) (openRecTy X δ t₂) +| tabs σ t₁ => tabs (σ⟦X ↝ δ⟧ᵞ) (openRecTy (X + 1) δ t₁) +| tapp t₁ σ => tapp (openRecTy X δ t₁) (σ⟦X ↝ δ⟧ᵞ) +| let' t₁ t₂ => let' (openRecTy X δ t₁) (openRecTy X δ t₂) +| inl t₁ => inl (openRecTy X δ t₁) +| inr t₂ => inr (openRecTy X δ t₂) +| case t₁ t₂ t₃ => case (openRecTy X δ t₁) (openRecTy X δ t₂) (openRecTy X δ t₃) @[inherit_doc] -scoped notation:68 t "⟦" X " ↝ " δ "⟧ᵗᵞ"=> openRec_ty X δ t +scoped notation:68 t "⟦" X " ↝ " δ "⟧ᵗᵞ"=> openRecTy X δ t /-- Variable opening (term opening to type) of the closest binding. -/ @[scoped grind =] -def open_ty (t : Term Var) (δ : Ty Var) := openRec_ty 0 δ t +def openTy (t : Term Var) (δ : Ty Var) := openRecTy 0 δ t @[inherit_doc] -scoped infixr:80 " ^ᵗᵞ " => open_ty +scoped infixr:80 " ^ᵗᵞ " => openTy /-- Variable opening (term opening to term) of the ith bound variable. -/ @[scoped grind =] -def openRec_tm (x : ℕ) (s : Term Var) : Term Var → Term Var +def openRecTm (x : ℕ) (s : Term Var) : Term Var → Term Var | bvar y => if x = y then s else (bvar y) | fvar x => fvar x -| abs σ t₁ => abs σ (openRec_tm (x + 1) s t₁) -| app t₁ t₂ => app (openRec_tm x s t₁) (openRec_tm x s t₂) -| tabs σ t₁ => tabs σ (openRec_tm x s t₁) -| tapp t₁ σ => tapp (openRec_tm x s t₁) σ -| let' t₁ t₂ => let' (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) -| inl t₁ => inl (openRec_tm x s t₁) -| inr t₂ => inr (openRec_tm x s t₂) -| case t₁ t₂ t₃ => case (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) (openRec_tm (x + 1) s t₃) +| abs σ t₁ => abs σ (openRecTm (x + 1) s t₁) +| app t₁ t₂ => app (openRecTm x s t₁) (openRecTm x s t₂) +| tabs σ t₁ => tabs σ (openRecTm x s t₁) +| tapp t₁ σ => tapp (openRecTm x s t₁) σ +| let' t₁ t₂ => let' (openRecTm x s t₁) (openRecTm (x + 1) s t₂) +| inl t₁ => inl (openRecTm x s t₁) +| inr t₂ => inr (openRecTm x s t₂) +| case t₁ t₂ t₃ => case (openRecTm x s t₁) (openRecTm (x + 1) s t₂) (openRecTm (x + 1) s t₃) @[inherit_doc] -scoped notation:68 t "⟦" x " ↝ " s "⟧ᵗᵗ"=> openRec_tm x s t +scoped notation:68 t "⟦" x " ↝ " s "⟧ᵗᵗ"=> openRecTm x s t /-- Variable opening (term opening to term) of the closest binding. -/ @[scoped grind =] -def open_tm (t₁ t₂ : Term Var) := openRec_tm 0 t₂ t₁ +def openTm (t₁ t₂ : Term Var) := openRecTm 0 t₂ t₁ @[inherit_doc] -scoped infixr:80 " ^ᵗᵗ " => open_tm +scoped infixr:80 " ^ᵗᵗ " => openTm /-- Locally closed terms. -/ inductive LC : Term Var → Prop @@ -212,189 +212,189 @@ variable {t : Term Var} {δ : Ty Var} omit [HasFresh Var] [DecidableEq Var] in /-- An opening (term to type) appearing in both sides of an equality of terms can be removed. -/ -lemma openRec_ty_neq_eq (neq : X ≠ Y) (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦X ↝ τ⟧ᵗᵞ) : +lemma openRecTy_neq_eq (neq : X ≠ Y) (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦X ↝ τ⟧ᵗᵞ) : t = t⟦X ↝ τ⟧ᵗᵞ := by induction t generalizing X Y <;> grind [Ty.openRec_neq_eq] omit [HasFresh Var] [DecidableEq Var] in /-- Elimination of mixed term and type opening. -/ @[scoped grind .] -lemma openRec_tm_ty_eq (eq : t⟦x ↝ s⟧ᵗᵗ = t⟦x ↝ s⟧ᵗᵗ⟦y ↝ δ⟧ᵗᵞ) : t = t⟦y ↝ δ⟧ᵗᵞ +lemma openRecTm_ty_eq (eq : t⟦x ↝ s⟧ᵗᵗ = t⟦x ↝ s⟧ᵗᵗ⟦y ↝ δ⟧ᵗᵞ) : t = t⟦y ↝ δ⟧ᵗᵞ := by induction t generalizing x y <;> grind /-- A locally closed term is unchanged by type opening. -/ @[scoped grind =_] -lemma openRec_ty_lc {t : Term Var} (lc : t.LC) : t = t⟦X ↝ σ⟧ᵗᵞ := by +lemma openRecTy_lc {t : Term Var} (lc : t.LC) : t = t⟦X ↝ σ⟧ᵗᵞ := by induction lc generalizing X with | let' | case | tabs | abs => - grind [fresh_exists <| free_union Var, Ty.openRec_lc, openRec_ty_neq_eq] + grind [fresh_exists <| free_union Var, Ty.openRec_lc, openRecTy_neq_eq] | _ => grind [Ty.openRec_lc] /-- Substitution of a type within a term. -/ @[scoped grind =] -def subst_ty (X : Var) (δ : Ty Var) : Term Var → Term Var +def substTy (X : Var) (δ : Ty Var) : Term Var → Term Var | bvar x => bvar x | fvar x => fvar x -| abs σ t₁ => abs (σ [X := δ]) (subst_ty X δ t₁) -| app t₁ t₂ => app (subst_ty X δ t₁) (subst_ty X δ t₂) -| tabs σ t₁ => tabs (σ [X := δ]) (subst_ty X δ t₁) -| tapp t₁ σ => tapp (subst_ty X δ t₁) (σ[X := δ]) -| let' t₁ t₂ => let' (subst_ty X δ t₁) (subst_ty X δ t₂) -| inl t₁ => inl (subst_ty X δ t₁) -| inr t₁ => inr (subst_ty X δ t₁) -| case t₁ t₂ t₃ => case (subst_ty X δ t₁) (subst_ty X δ t₂) (subst_ty X δ t₃) +| abs σ t₁ => abs (σ [X := δ]) (substTy X δ t₁) +| app t₁ t₂ => app (substTy X δ t₁) (substTy X δ t₂) +| tabs σ t₁ => tabs (σ [X := δ]) (substTy X δ t₁) +| tapp t₁ σ => tapp (substTy X δ t₁) (σ[X := δ]) +| let' t₁ t₂ => let' (substTy X δ t₁) (substTy X δ t₂) +| inl t₁ => inl (substTy X δ t₁) +| inr t₁ => inr (substTy X δ t₁) +| case t₁ t₂ t₃ => case (substTy X δ t₁) (substTy X δ t₂) (substTy X δ t₃) instance : HasSubstitution (Term Var) Var (Ty Var) where - subst t X δ := Term.subst_ty X δ t + subst t X δ := Term.substTy X δ t omit [HasFresh Var] in @[scoped grind _=_] -lemma subst_ty_def : subst_ty (X : Var) (δ : Ty Var) (t : Term Var) = t[X := δ] := by rfl +lemma substTy_def : substTy (X : Var) (δ : Ty Var) (t : Term Var) = t[X := δ] := by rfl omit [HasFresh Var] in /-- Substitution of a free type variable not present in a term leaves it unchanged. -/ -lemma subst_ty_fresh (nmem : X ∉ t.fv_ty) (δ : Ty Var) : t = t [X := δ] := +lemma substTy_fresh (nmem : X ∉ t.fvTy) (δ : Ty Var) : t = t [X := δ] := by induction t <;> grind [Ty.subst_fresh] /-- Substitution of a locally closed type distributes with term opening to a type . -/ -lemma openRec_ty_subst_ty (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : +lemma openRecTy_substTy (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : (t⟦Y ↝ σ⟧ᵗᵞ)[X := δ] = (t[X := δ])⟦Y ↝ σ[X := δ]⟧ᵗᵞ := by induction t generalizing Y <;> grind [Ty.openRec_subst] -/-- Specialize `Term.openRec_ty_subst` to the first opening. -/ -lemma open_ty_subst_ty (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : - (t ^ᵗᵞ σ)[X := δ] = t[X := δ] ^ᵗᵞ σ[X := δ] := openRec_ty_subst_ty 0 t σ lc X +/-- Specialize `Term.openRecTy_subst` to the first opening. -/ +lemma openTy_substTy (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : + (t ^ᵗᵞ σ)[X := δ] = t[X := δ] ^ᵗᵞ σ[X := δ] := openRecTy_substTy 0 t σ lc X -/-- Specialize `Term.open_ty_subst` to free type variables. -/ -lemma open_ty_subst_ty_var (t : Term Var) (neq : Y ≠ X) (lc : δ.LC) : - (t ^ᵗᵞ .fvar Y)[X := δ] = t[X := δ] ^ᵗᵞ .fvar Y := by grind [open_ty_subst_ty] +/-- Specialize `Term.openTy_subst` to free type variables. -/ +lemma openTy_substTy_var (t : Term Var) (neq : Y ≠ X) (lc : δ.LC) : + (t ^ᵗᵞ .fvar Y)[X := δ] = t[X := δ] ^ᵗᵞ .fvar Y := by grind [openTy_substTy] omit [HasFresh Var] /-- Opening a term to a type is equivalent to opening to a free variable and substituting. -/ -lemma openRec_ty_subst_ty_intro (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fv_ty) : +lemma openRecTy_substTy_intro (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fvTy) : t⟦Y ↝ δ⟧ᵗᵞ = (t⟦Y ↝ Ty.fvar X⟧ᵗᵞ)[X := δ] := by induction t generalizing X δ Y <;> grind [Ty.openRec_subst_intro] -/-- Specialize `Term.openRec_ty_subst_ty_intro` to the first opening. -/ -lemma open_ty_subst_ty_intro (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fv_ty) : - t ^ᵗᵞ δ = (t ^ᵗᵞ Ty.fvar X)[X := δ] := openRec_ty_subst_ty_intro _ _ nmem +/-- Specialize `Term.openRecTy_substTy_intro` to the first opening. -/ +lemma openTy_substTy_intro (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fvTy) : + t ^ᵗᵞ δ = (t ^ᵗᵞ Ty.fvar X)[X := δ] := openRecTy_substTy_intro _ _ nmem /-- Substitution of a term within a term. -/ @[scoped grind =] -def subst_tm (x : Var) (s : Term Var) : Term Var → Term Var +def substTm (x : Var) (s : Term Var) : Term Var → Term Var | bvar x => bvar x | fvar y => if y = x then s else fvar y -| abs σ t₁ => abs σ (subst_tm x s t₁) -| app t₁ t₂ => app (subst_tm x s t₁) (subst_tm x s t₂) -| tabs σ t₁ => tabs σ (subst_tm x s t₁) -| tapp t₁ σ => tapp (subst_tm x s t₁) σ -| let' t₁ t₂ => let' (subst_tm x s t₁) (subst_tm x s t₂) -| inl t₁ => inl (subst_tm x s t₁) -| inr t₁ => inr (subst_tm x s t₁) -| case t₁ t₂ t₃ => case (subst_tm x s t₁) (subst_tm x s t₂) (subst_tm x s t₃) +| abs σ t₁ => abs σ (substTm x s t₁) +| app t₁ t₂ => app (substTm x s t₁) (substTm x s t₂) +| tabs σ t₁ => tabs σ (substTm x s t₁) +| tapp t₁ σ => tapp (substTm x s t₁) σ +| let' t₁ t₂ => let' (substTm x s t₁) (substTm x s t₂) +| inl t₁ => inl (substTm x s t₁) +| inr t₁ => inr (substTm x s t₁) +| case t₁ t₂ t₃ => case (substTm x s t₁) (substTm x s t₂) (substTm x s t₃) instance : HasSubstitution (Term Var) Var (Term Var) where - subst t x s := Term.subst_tm x s t + subst t x s := Term.substTm x s t @[scoped grind _=_] -lemma subst_tm_def : subst_tm (x : Var) (s : Term Var) (t : Term Var) = t[x := s] := by rfl +lemma substTm_def : substTm (x : Var) (s : Term Var) (t : Term Var) = t[x := s] := by rfl omit [DecidableEq Var] in /-- An opening (term to term) appearing in both sides of an equality of terms can be removed. -/ -lemma openRec_tm_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ᵗᵗ = t⟦y ↝ s₁⟧ᵗᵗ⟦x ↝ s₂⟧ᵗᵗ) : +lemma openRecTm_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ᵗᵗ = t⟦y ↝ s₁⟧ᵗᵗ⟦x ↝ s₂⟧ᵗᵗ) : t = t⟦x ↝ s₂⟧ᵗᵗ := by induction t generalizing x y <;> grind omit [DecidableEq Var] in /-- Elimination of mixed term and type opening. -/ -lemma openRec_ty_tm_eq (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦x ↝ s⟧ᵗᵗ) : t = t⟦x ↝ s⟧ᵗᵗ := by +lemma openRecTy_tm_eq (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦x ↝ s⟧ᵗᵗ) : t = t⟦x ↝ s⟧ᵗᵗ := by induction t generalizing x Y <;> grind variable [HasFresh Var] /-- A locally closed term is unchanged by term opening. -/ @[scoped grind =_] -lemma openRec_tm_lc (lc : t.LC) : t = t⟦x ↝ s⟧ᵗᵗ := by +lemma openRecTm_lc (lc : t.LC) : t = t⟦x ↝ s⟧ᵗᵗ := by induction lc generalizing x with | let' | case | tabs | abs => - grind [fresh_exists <| free_union Var, openRec_tm_neq_eq, openRec_ty_tm_eq] + grind [fresh_exists <| free_union Var, openRecTm_neq_eq, openRecTy_tm_eq] | _ => grind variable {t s : Term Var} {δ : Ty Var} {x : Var} omit [HasFresh Var] in /-- Substitution of a free term variable not present in a term leaves it unchanged. -/ -lemma subst_tm_fresh (nmem : x ∉ t.fv_tm) (s : Term Var) : t = t[x := s] := by +lemma substTm_fresh (nmem : x ∉ t.fvTm) (s : Term Var) : t = t[x := s] := by induction t <;> grind /-- Substitution of a locally closed term distributes with term opening to a term. -/ -lemma openRec_tm_subst_tm (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : +lemma openRecTm_substTm (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : (t₁⟦y ↝ t₂⟧ᵗᵗ)[x := s] = (t₁[x := s])⟦y ↝ t₂[x := s]⟧ᵗᵗ := by induction t₁ generalizing y <;> grind -/-- Specialize `Term.openRec_tm_subst_tm` to the first opening. -/ -lemma open_tm_subst_tm (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : - (t₁ ^ᵗᵗ t₂)[x := s] = (t₁[x := s]) ^ᵗᵗ t₂[x := s] := openRec_tm_subst_tm 0 t₁ t₂ lc x +/-- Specialize `Term.openRecTm_substTm` to the first opening. -/ +lemma openTm_substTm (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : + (t₁ ^ᵗᵗ t₂)[x := s] = (t₁[x := s]) ^ᵗᵗ t₂[x := s] := openRecTm_substTm 0 t₁ t₂ lc x -/-- Specialize `Term.openRec_tm_subst_tm` to free term variables. -/ -lemma open_tm_subst_tm_var (t : Term Var) (neq : y ≠ x) (lc : s.LC) : - (t ^ᵗᵗ fvar y)[x := s] = (t[x := s]) ^ᵗᵗ fvar y := by grind [open_tm_subst_tm] +/-- Specialize `Term.openRecTm_substTm` to free term variables. -/ +lemma openTm_substTm_var (t : Term Var) (neq : y ≠ x) (lc : s.LC) : + (t ^ᵗᵗ fvar y)[x := s] = (t[x := s]) ^ᵗᵗ fvar y := by grind [openTm_substTm] /-- Substitution of a locally closed type distributes with term opening to a term. -/ -lemma openRec_tm_subst_ty (y : ℕ) (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : +lemma openRecTm_substTy (y : ℕ) (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : (t₁⟦y ↝ t₂⟧ᵗᵗ)[X := δ] = (t₁[X := δ])⟦y ↝ t₂[X := δ]⟧ᵗᵗ := by induction t₁ generalizing y <;> grind -/-- Specialize `Term.openRec_tm_subst_ty` to the first opening -/ -lemma open_tm_subst_ty (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : - (t₁ ^ᵗᵗ t₂)[X := δ] = (t₁[X := δ]) ^ᵗᵗ t₂[X := δ] := openRec_tm_subst_ty 0 t₁ t₂ δ X +/-- Specialize `Term.openRecTm_substTy` to the first opening -/ +lemma openTm_substTy (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : + (t₁ ^ᵗᵗ t₂)[X := δ] = (t₁[X := δ]) ^ᵗᵗ t₂[X := δ] := openRecTm_substTy 0 t₁ t₂ δ X -/-- Specialize `Term.open_tm_subst_ty` to free term variables -/ -lemma open_tm_subst_ty_var (t₁ : Term Var) (δ : Ty Var) (X y : Var) : - (t₁ ^ᵗᵗ fvar y)[X := δ] = (t₁[X := δ]) ^ᵗᵗ fvar y := by grind [open_tm_subst_ty] +/-- Specialize `Term.openTm_substTy` to free term variables -/ +lemma openTm_substTy_var (t₁ : Term Var) (δ : Ty Var) (X y : Var) : + (t₁ ^ᵗᵗ fvar y)[X := δ] = (t₁[X := δ]) ^ᵗᵗ fvar y := by grind [openTm_substTy] /-- Substitution of a locally closed term distributes with term opening to a type. -/ -lemma openRec_ty_subst_tm (Y : ℕ) (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : +lemma openRecTy_substTm (Y : ℕ) (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : (t⟦Y ↝ δ⟧ᵗᵞ)[x := s] = t[x := s]⟦Y ↝ δ⟧ᵗᵞ := by induction t generalizing Y <;> grind -/-- Specialize `Term.openRec_ty_subst_tm` to the first opening. -/ -lemma open_ty_subst_tm (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : - (t ^ᵗᵞ δ)[x := s] = t[x := s] ^ᵗᵞ δ := openRec_ty_subst_tm 0 t δ lc x +/-- Specialize `Term.openRecTy_substTm` to the first opening. -/ +lemma openTy_substTm (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : + (t ^ᵗᵞ δ)[x := s] = t[x := s] ^ᵗᵞ δ := openRecTy_substTm 0 t δ lc x -/-- Specialize `Term.open_ty_subst_tm` to free type variables. -/ -lemma open_ty_subst_tm_var (t : Term Var) (lc : s.LC) (x Y : Var) : - (t ^ᵗᵞ .fvar Y)[x := s] = t[x := s] ^ᵗᵞ .fvar Y := open_ty_subst_tm _ _ lc _ +/-- Specialize `Term.openTy_substTm` to free type variables. -/ +lemma openTy_substTm_var (t : Term Var) (lc : s.LC) (x Y : Var) : + (t ^ᵗᵞ .fvar Y)[x := s] = t[x := s] ^ᵗᵞ .fvar Y := openTy_substTm _ _ lc _ omit [HasFresh Var] /-- Opening a term to a term is equivalent to opening to a free variable and substituting. -/ -lemma openRec_tm_subst_tm_intro (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fv_tm) : +lemma openRecTm_substTm_intro (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fvTm) : t⟦y ↝ s⟧ᵗᵗ = (t⟦y ↝ fvar x⟧ᵗᵗ)[x := s] := by induction t generalizing y <;> grind -/-- Specialize `Term.openRec_tm_subst_tm_intro` to the first opening. -/ -lemma open_tm_subst_tm_intro (t s : Term Var) (nmem : x ∉ t.fv_tm) : - t ^ᵗᵗs = (t ^ᵗᵗ fvar x)[x := s] := openRec_tm_subst_tm_intro _ _ _ nmem +/-- Specialize `Term.openRecTm_substTm_intro` to the first opening. -/ +lemma openTm_substTm_intro (t s : Term Var) (nmem : x ∉ t.fvTm) : + t ^ᵗᵗs = (t ^ᵗᵗ fvar x)[x := s] := openRecTm_substTm_intro _ _ _ nmem variable [HasFresh Var] -lemma subst_ty_lc (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X := δ].LC := by +lemma substTy_lc (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X := δ].LC := by induction t_lc case' abs => apply LC.abs (free_union Var) case' tabs => apply LC.tabs (free_union Var) case' let' => apply LC.let' (free_union Var) case' case => apply LC.case (free_union Var) - all_goals grind [Ty.subst_lc, open_tm_subst_ty_var, openRec_ty_subst_ty] + all_goals grind [Ty.subst_lc, openTm_substTy_var, openRecTy_substTy] -lemma subst_tm_lc (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x := s].LC := by +lemma substTm_lc (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x := s].LC := by induction t_lc case' abs => apply LC.abs (free_union Var) case' let' => apply LC.let' (free_union Var) case' case => apply LC.case (free_union Var) case' tabs => apply LC.tabs (free_union Var) - all_goals grind [open_tm_subst_tm_var, open_ty_subst_tm_var] + all_goals grind [openTm_substTm_var, openTy_substTm_var] end Term @@ -414,10 +414,10 @@ instance : HasSubstitution (Binding Var) Var (Ty Var) where variable {δ γ : Ty Var} {X : Var} @[scoped grind _=_] -lemma subst_sub : (sub γ)[X := δ] = sub (γ[X := δ]) := by rfl +lemma substSub : (sub γ)[X := δ] = sub (γ[X := δ]) := by rfl @[scoped grind _=_] -lemma subst_ty : (ty γ)[X := δ] = ty (γ[X := δ]) := by rfl +lemma substTy : (ty γ)[X := δ] = ty (γ[X := δ]) := by rfl open scoped Ty in /-- Substitution of a free variable not present in a binding leaves it unchanged. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean index 8263fe295..b9969aa49 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean @@ -68,7 +68,7 @@ variable [HasFresh Var] @[scoped grind <=] lemma open_tm_body (body : t₁.body) (lc : t₂.LC) : (t₁ ^ᵗᵗ t₂).LC := by cases body - grind [fresh_exists <| free_union [fv_tm] Var, subst_tm_lc, open_tm_subst_tm_intro] + grind [fresh_exists <| free_union [fvTm] Var, substTm_lc, openTm_substTm_intro] end @@ -109,8 +109,8 @@ lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by · grind · cases lc grind [ - fresh_exists <| free_union [fv_tm, fv_ty] Var, subst_tm_lc, - subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro] + fresh_exists <| free_union [fvTm, fvTy] Var, substTm_lc, + substTy_lc, openTm_substTm_intro, openTy_substTy_intro] all_goals grind end Term diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index c5e0116db..cf294d3b1 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -42,22 +42,22 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing case abs der _ _ => have sub : Sub Γ (σ.arrow τ) (σ.arrow τ) := by grind [Sub.refl] have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub - grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm, Sub.weaken] + grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm, Sub.weaken] case tapp Γ _ σ τ σ' _ _ _ => cases step case tabs der _ _ => have sub : Sub Γ (σ.all τ) (σ.all τ) := by grind [Sub.refl] have ⟨_, _, ⟨_, _⟩⟩ := der.tabs_inv sub - have ⟨X, mem⟩ := fresh_exists <| free_union [Ty.fv, fv_ty] Var + have ⟨X, mem⟩ := fresh_exists <| free_union [Ty.fv, fvTy] Var simp at mem - have : Γ = (Context.map_val (·[X:=σ']) []) ++ Γ := by grind - rw [open_ty_subst_ty_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty] + have : Γ = (Context.mapVal (·[X:=σ']) []) ++ Γ := by grind + rw [openTy_substTy_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty] case tapp => grind case let' Γ _ _ _ _ L der _ ih₁ _ => cases step case let_bind red₁ _ => apply Typing.let' L (ih₁ red₁); grind case let_body => - grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm] + grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm] case case Γ _ σ τ _ _ _ L _ _ _ ih₁ _ _ => have sub : Sub Γ (σ.sum τ) (σ.sum τ) := by grind [Sub.refl] have : Γ = [] ++ Γ := by rfl @@ -65,10 +65,10 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing case «case» red₁ _ _ => apply Typing.case L (ih₁ red₁) <;> grind case case_inl der _ _ => have ⟨_, ⟨_, _⟩⟩ := der.inl_inv sub - grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm] + grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm] case case_inr der _ _ => have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub - grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm] + grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm] all_goals grind [cases Red] /-- Any typable term either has a reduction step or is a value. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index 4f0635f5e..1a8abe649 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -144,7 +144,7 @@ lemma narrow (sub_δ : Sub Δ δ δ') (sub_narrow : Sub (Γ ++ ⟨X, Binding.sub variable [HasFresh Var] in /-- Subtyping of substitutions. -/ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ δ') : - Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := by + Sub (Γ.mapVal (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := by generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at sub₁ induction sub₁ generalizing Γ case all => apply Sub.all (free_union Var) <;> grind [open_subst_var] @@ -152,7 +152,7 @@ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub have := map_subst_nmem Δ X δ have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle have : .sub σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup] - have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) + have := @mapVal_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) by_cases X = X' · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head] · grind diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index d0edd7896..7a9e8efe0 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -124,29 +124,29 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typi -/ grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen, -append_assoc] · grind [Env.Wf.strengthen, => List.perm_dlookup] - case abs => grind [abs (free_union Var), open_tm_subst_tm_var] - case tabs => grind [tabs (free_union Var), open_ty_subst_tm_var] - case let' der _ => grind [let' (free_union Var) (der eq), open_tm_subst_tm_var] + case abs => grind [abs (free_union Var), openTm_substTm_var] + case tabs => grind [tabs (free_union Var), openTy_substTm_var] + case let' der _ => grind [let' (free_union Var) (der eq), openTm_substTm_var] case case der _ _ => - apply case (free_union Var) (der eq) <;> grind [open_tm_subst_tm_var] + apply case (free_union Var) (der eq) <;> grind [openTm_substTm_var] all_goals grind [Env.Wf.strengthen, Ty.Wf.strengthen, Sub.strengthen] /-- Type substitution within a typing. -/ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Δ δ δ') : - Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := by + Typing (Γ.mapVal (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := by generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der induction der generalizing Γ X case var σ _ X' _ mem => have := map_subst_nmem Δ X δ - have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) + have := @mapVal_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) grind [Env.Wf.map_subst, → notMem_keys_of_nodupKeys_cons] - case abs => grind [abs (free_union [Ty.fv] Var), Ty.subst_fresh, open_tm_subst_ty_var] - case tabs => grind [tabs (free_union Var), open_ty_subst_ty_var, open_subst_var] + case abs => grind [abs (free_union [Ty.fv] Var), Ty.subst_fresh, openTm_substTy_var] + case tabs => grind [tabs (free_union Var), openTy_substTy_var, open_subst_var] case let' der _ => apply let' (free_union Var) (der eq) - grind [open_tm_subst_ty_var] + grind [openTm_substTy_var] case case der _ _ => - apply case (free_union Var) (der eq) <;> grind [open_tm_subst_ty_var] + apply case (free_union Var) (der eq) <;> grind [openTm_substTy_var] case tapp => grind [Ty.open_subst, Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst] all_goals grind [Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst] diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index 423312304..ffb6f3023 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -121,8 +121,8 @@ lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ + variable [HasFresh Var] in /-- A type remains well-formed under context substitution (of a well-formed type). -/ lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) - (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by - have := @map_val_mem Var (Binding Var) + (ok : (Γ.mapVal (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.mapVal (·[X:=τ']) ++ Δ := by + have := @mapVal_mem Var (Binding Var) generalize eq : Γ ++ ⟨X, Binding.sub τ⟩ :: Δ = Θ at wf_σ induction wf_σ generalizing Γ τ' with | all => apply all (free_union [dom] Var) <;> grind [open_subst_var] @@ -133,7 +133,7 @@ variable [HasFresh Var] in lemma open_lc (ok_Γ : Γ✓) (wf_all : (Ty.all σ τ).Wf Γ) (wf_δ : δ.Wf Γ) : (τ ^ᵞ δ).Wf Γ := by cases wf_all with | all => let ⟨X, _⟩ := fresh_exists <| free_union [fv, Context.dom] Var - have : Γ = Context.map_val (·[X:=δ]) [] ++ Γ := by grind + have : Γ = Context.mapVal (·[X:=δ]) [] ++ Γ := by grind grind [open_subst_intro, map_subst] /-- A type bound in a context is well formed. -/ @@ -176,7 +176,7 @@ lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| variable [HasFresh Var] in /-- A context remains well-formed under substitution (of a well-formed type). -/ lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : - Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by + Env.Wf <| Γ.mapVal (·[X:=τ']) ++ Δ := by induction Γ generalizing wf_τ' Δ τ' <;> cases wf_env case nil => grind case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst] @@ -185,7 +185,7 @@ variable [HasFresh Var] /-- A well-formed context is unchanged by substituting for a free key. -/ lemma map_subst_nmem (Γ : Env Var) (X : Var) (σ : Ty Var) (wf : Γ.Wf) (nmem : X ∉ Γ.dom) : - Γ = Γ.map_val (·[X:=σ]) := by + Γ = Γ.mapVal (·[X:=σ]) := by induction wf <;> grind [Ty.Wf.nmem_fv, Binding.subst_fresh] end Env.Wf diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index 9c98b17da..d9ab413bd 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -71,32 +71,32 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := · intro M N P _ _ _ s _ grind [ih₂.multiApp M N (s :: P)] -/-- The `entails_context` predicate ensures that each variable in the context +/-- The `entailsContext` predicate ensures that each variable in the context is mapped to a term in the corresponding semantic map. -/ -abbrev entails_context (E : Term.Env Var) (Γ : Context Var (Ty Base)) := +abbrev entailsContext (E : Term.Env Var) (Γ : Context Var (Ty Base)) := ∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (multiSubst E (fvar x)) ∈ semanticMap τ /-- The empty context is entailed by any environment. -/ -lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context [] Γ := by +lemma entailsContext_empty {Γ : Context Var (Ty Base)} : entailsContext [] Γ := by have := semanticMap_saturated (Var := Var) (Base := Base) grind open scoped Context in omit [HasFresh Var] in -/-- The `entails_context` predicate is preserved when extending the context +/-- The `entailsContext` predicate is preserved when extending the context with a new variable, provided the new variable is fresh and its substitution is in the corresponding semantic map. -/ -lemma entails_context_cons (E : Term.Env Var) (Γ : Context Var (Ty Base)) +lemma entailsContext_cons (E : Term.Env Var) (Γ : Context Var (Ty Base)) (x : Var) (τ : Ty Base) (sub : Term Var) (h_fresh : x ∉ E.dom ∪ E.fv ∪ Γ.dom) (h_mem : sub ∈ semanticMap τ) : - entails_context E Γ → entails_context (⟨ x, sub ⟩ :: E) (⟨ x, τ ⟩ :: Γ) := by + entailsContext E Γ → entailsContext (⟨ x, sub ⟩ :: E) (⟨ x, τ ⟩ :: Γ) := by grind [multiSubst_fvar_fresh, subst_fresh, multiSubst_preserves_not_fvar] /-- The `entails` predicate states that a term `t` is semantically valid with respect to a context `Γ` and a type `τ` -/ abbrev entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) := - ∀ E, env_LC E → (entails_context E Γ) → (multiSubst E t) ∈ semanticMap τ + ∀ E, envLC E → entailsContext E Γ → multiSubst E t ∈ semanticMap τ /-- The `soundness` lemma states that if a term `t` has type `τ` in context `Γ`, then `t` is semantically valid with respect to `Γ` and `τ` -/ @@ -111,7 +111,7 @@ lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : let := multiSubst E t have ⟨x, _⟩ := fresh_exists <| E.dom ∪ free_union [fv, Context.dom, Env.fv] Var have := IH (x := x) (E := ⟨x,s⟩ :: E) - grind [multiSubst_abs, entails_context_cons, multiSubst_open_var] + grind [multiSubst_abs, entailsContext_cons, multiSubst_open_var] | app => grind [multiSubst_app] /-- Using soundness and the fact that the empty context @@ -119,7 +119,7 @@ lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : a well-typed term is strongly normalizing. -/ theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN FullBeta t := by apply (semanticMap_saturated τ).sn - apply (soundness der [] (by grind) entails_context_empty) + apply (soundness der [] (by grind) entailsContext_empty) end LambdaCalculus.LocallyNameless.Stlc diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean index 05db5bab3..548b3d2c0 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean @@ -51,10 +51,10 @@ def Env.fv (E : Env Var) : Finset Var := attribute [scoped grind =] Env.fv /-- An environment is locally closed if all terms in the environment are locally closed -/ -abbrev env_LC (E : Env Var) : Prop := ∀ {x M}, ⟨x, M⟩ ∈ E → LC M +abbrev envLC (E : Env Var) : Prop := ∀ {x M}, ⟨x, M⟩ ∈ E → LC M /-- Adding a locally closed term to an environment preserves local closure -/ -lemma env_LC_cons (lc_sub : LC sub) (lc_E : env_LC E) : env_LC (⟨ x, sub ⟩ :: E) := by +lemma envLC_cons (lc_sub : LC sub) (lc_E : envLC E) : envLC (⟨ x, sub ⟩ :: E) := by grind /-- Multi-substitution of a fresh variable does nothing -/ @@ -81,7 +81,7 @@ lemma multiSubst_abs (M : Term Var) (E : Env Var) : provided that the variable is not in the domain of the environment and the environment is locally closed -/ lemma multiSubst_open_var [HasFresh Var] (M : Term Var) (E : Env Var) (x : Var) - (h_ndom : x ∉ E.dom) (h_lc : env_LC E) : + (h_ndom : x ∉ E.dom) (h_lc : envLC E) : multiSubst E (M ^ fvar x) = multiSubst E M ^ fvar x := by induction E with grind diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 3bd8c11bf..5bad96e46 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -105,7 +105,7 @@ instance judgementalContext : instance : LogicalEquivalence (Proposition Label) (Satisfies.Judgement State Label) (Satisfies.Bundled) where eqv := Proposition.Equiv - eqv_fill_valid {a b : Proposition Label} (heqv : a.Equiv (State := State) b) + eqvFillValid {a b : Proposition Label} (heqv : a.Equiv (State := State) b) (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label)) (h : Satisfies.Bundled c<[a]) : Satisfies.Bundled c<[b] := by simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill] diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index bb9b145de..c331ae2ae 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -114,11 +114,11 @@ def Proposition.negative : Proposition Atom → Bool | _ => false /-- Whether a `Proposition` is positive is decidable. -/ -instance Proposition.positive_decidable (a : Proposition Atom) : Decidable a.positive := +instance Proposition.positiveDecidable (a : Proposition Atom) : Decidable a.positive := a.positive.decEq true /-- Whether a `Proposition` is negative is decidable. -/ -instance Proposition.negative_decidable (a : Proposition Atom) : Decidable a.negative := +instance Proposition.negativeDecidable (a : Proposition Atom) : Decidable a.negative := a.negative.decEq true /-- Propositional duality. -/ @@ -225,21 +225,21 @@ def Proof.cut' (p : ⇓(a⫠ ::ₘ Γ)) (q : ⇓(a ::ₘ Δ)) : ⇓(Γ + Δ) := p.cut r /-- Inversion of the ⅋ rule. -/ -def Proof.parr_inversion {Γ : Sequent Atom} (h : ⇓((a ⅋ b) ::ₘ Γ)) : ⇓(a ::ₘ b ::ₘ Γ) := +def Proof.parrInversion {Γ : Sequent Atom} (h : ⇓((a ⅋ b) ::ₘ Γ)) : ⇓(a ::ₘ b ::ₘ Γ) := show a ::ₘ b ::ₘ Γ = {a, b} + Γ by simp ▸ cut' (show ({a, b} : Sequent Atom) = {a} + {b} by simp ▸ tensor ax' ax') h /-- Inversion of the ⊥ rule. -/ -def Proof.bot_inversion {Γ : Sequent Atom} (h : ⇓(⊥ ::ₘ Γ)) : ⇓Γ := by +def Proof.botInversion {Γ : Sequent Atom} (h : ⇓(⊥ ::ₘ Γ)) : ⇓Γ := by convert Proof.cut' (a := ⊥) (Γ := {}) (Δ := Γ) Proof.one h simp /-- Inversion of the & rule, first component. -/ -def Proof.with_inversion₁ {Γ : Sequent Atom} (h : ⇓((a & b) ::ₘ Γ)) : ⇓(a ::ₘ Γ) := +def Proof.withInversion₁ {Γ : Sequent Atom} (h : ⇓((a & b) ::ₘ Γ)) : ⇓(a ::ₘ Γ) := cut' (a := a & b) (oplus₁ ax') h /-- Inversion of the & rule, second component. -/ -def Proof.with_inversion₂ {Γ : Sequent Atom} (h : ⇓((a & b) ::ₘ Γ)) : ⇓(b ::ₘ Γ) := +def Proof.withInversion₂ {Γ : Sequent Atom} (h : ⇓((a & b) ::ₘ Γ)) : ⇓(b ::ₘ Γ) := cut' (a := a & b) (oplus₂ ax') h section LogicalEquiv @@ -314,23 +314,23 @@ instance : IsEquiv (Proposition Atom) Proposition.Equiv where /-- !⊤ ≡⇓ 1 -/ @[scoped grind =] -def bang_top_eqv_one : (!⊤ : Proposition Atom) ≡⇓ 1 := +def bangTopEqvOne : (!⊤ : Proposition Atom) ≡⇓ 1 := ⟨.weaken .one, .bot (.bang rfl .top)⟩ /-- ʔ0 ≡⇓ ⊥ -/ @[scoped grind =] -def quest_zero_eqv_bot : (ʔ0 : Proposition Atom) ≡⇓ ⊥ := +def questZeroEqvBot : (ʔ0 : Proposition Atom) ≡⇓ ⊥ := ⟨rwConclusion (Multiset.pair_comm ..) <| .bot (.bang rfl .top), rwConclusion (Multiset.pair_comm ..) <| .weaken .one⟩ /-- a ⊗ 0 ≡⇓ 0 -/ @[scoped grind =] -def tensor_zero_eqv_zero (a : Proposition Atom) : a ⊗ 0 ≡⇓ 0 := +def tensorZeroEqvZero (a : Proposition Atom) : a ⊗ 0 ≡⇓ 0 := ⟨.parr <| .rwConclusion (Multiset.cons_swap ..) .top, .top⟩ /-- a ⅋ ⊤ ≡⇓ ⊤ -/ @[scoped grind =] -def parr_top_eqv_top (a : Proposition Atom) : a ⅋ ⊤ ≡⇓ ⊤ := +def parrTopEqvTop (a : Proposition Atom) : a ⅋ ⊤ ≡⇓ ⊤ := ⟨.rwConclusion (Multiset.cons_swap ..) .top, .rwConclusion (Multiset.cons_swap ..) <| .parr <| .rwConclusion (Multiset.cons_swap ..) .top⟩ @@ -343,7 +343,7 @@ attribute [local grind =] Multiset.insert_eq_cons open scoped Multiset in /-- ⊗ distributes over ⊕. -/ -def tensor_distrib_oplus (a b c : Proposition Atom) : a ⊗ (b ⊕ c) ≡⇓ (a ⊗ b) ⊕ (a ⊗ c) := +def tensorDistribOplus (a b c : Proposition Atom) : a ⊗ (b ⊕ c) ≡⇓ (a ⊗ b) ⊕ (a ⊗ c) := ⟨.parr <| .rwConclusion (Multiset.cons_swap ..) <| .with @@ -362,7 +362,7 @@ def tensor_distrib_oplus (a b c : Proposition Atom) : a ⊗ (b ⊕ c) ≡⇓ (a /-- The proposition at the head of a proof can be substituted by an equivalent proposition. -/ @[scoped grind =] -def subst_eqv_head {Γ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(a ::ₘ Γ)) : ⇓(b ::ₘ Γ) := +def substEqvHead {Γ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(a ::ₘ Γ)) : ⇓(b ::ₘ Γ) := show b ::ₘ Γ = Γ + {b} by grind ▸ p.cut heqv.1 theorem add_middle_eq_cons {a : Proposition Atom} : Γ + {a} + Δ = a ::ₘ (Γ + Δ) := by @@ -372,8 +372,8 @@ open scoped Multiset in /-- Any proposition in a proof (regardless of its position) can be substituted by an equivalent proposition. -/ @[scoped grind =] -def subst_eqv {Γ Δ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ) := - add_middle_eq_cons ▸ subst_eqv_head heqv (add_middle_eq_cons ▸ p) +def substEqv {Γ Δ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ) := + add_middle_eq_cons ▸ substEqvHead heqv (add_middle_eq_cons ▸ p) open scoped Context @@ -652,14 +652,14 @@ instance : Congruence (Proposition Atom) Proposition.Equiv where noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where eqv := Proposition.Equiv - eqv_fill_valid {a b : Proposition Atom} (heqv : a.Equiv b) + eqvFillValid {a b : Proposition Atom} (heqv : a.Equiv b) (c : HasHContext.Context (Sequent Atom) (Proposition Atom)) (h : ⇓c<[a]) : ⇓c<[b] := by - apply subst_eqv_head (chooseEquiv heqv) h + apply substEqvHead (chooseEquiv heqv) h /-- Tensor is commutative. -/ @[scoped grind ←] -def tensor_symm {a b : Proposition Atom} : a ⊗ b ≡⇓ b ⊗ a := +def tensorSymm {a b : Proposition Atom} : a ⊗ b ≡⇓ b ⊗ a := ⟨.parr <| show a⫠ ::ₘ b⫠ ::ₘ {b ⊗ a} = (b ⊗ a) ::ₘ {b⫠} + {a⫠} by grind ▸ .tensor .ax .ax, .parr <| show b⫠ ::ₘ a⫠ ::ₘ {a ⊗ b} = (a ⊗ b) ::ₘ {a⫠} + {b⫠} by grind ▸ .tensor .ax .ax⟩ @@ -667,7 +667,7 @@ def tensor_symm {a b : Proposition Atom} : a ⊗ b ≡⇓ b ⊗ a := open scoped Multiset in /-- ⊗ is associative. -/ @[scoped grind ←] -def tensor_assoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) ⊗ c := +def tensorAssoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) ⊗ c := ⟨.parr <| Multiset.cons_swap .. ▸ (.parr <| @@ -679,17 +679,17 @@ def tensor_assoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) (.tensor .ax <| .tensor .ax .ax)⟩ instance {Γ : Sequent Atom} : Std.Symm (fun a b => Derivable ((a ⊗ b) ::ₘ Γ)) where - symm _ _ h := DerivableIn.fromDerivation (subst_eqv_head tensor_symm (DerivableIn.toDerivation h)) + symm _ _ h := DerivableIn.fromDerivation (substEqvHead tensorSymm (DerivableIn.toDerivation h)) /-- ⊕ is idempotent. -/ @[scoped grind ←] -def oplus_idem {a : Proposition Atom} : a ⊕ a ≡⇓ a := +def oplusIdem {a : Proposition Atom} : a ⊕ a ≡⇓ a := ⟨.with .ax' .ax', show ({a⫠, a ⊕ a} : Sequent Atom) = {a ⊕ a, a⫠} by grind ▸ .oplus₁ .ax⟩ /-- & is idempotent. -/ @[scoped grind ←] -def with_idem {a : Proposition Atom} : a & a ≡⇓ a := +def withIdem {a : Proposition Atom} : a & a ≡⇓ a := ⟨.oplus₁ .ax', show ({a⫠, a & a} : Sequent Atom) = {a & a, a⫠} by grind ▸ .with .ax .ax⟩ diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index 7f7a23713..df33df215 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -179,7 +179,7 @@ lemma of_Fact {G : Fact P} {p : P} @[scoped grind =, simp] lemma mem_carrier (G : Fact P) : G.carrier = (G : Set P) := rfl /-- Construct a fact from a set G and a proof that its biorthogonal closure is contained in G. -/ -@[simps] def Fact.mk_subset (G : Set P) (h : G⫠⫠ ⊆ G) : Fact P where +@[simps] def Fact.mkSubset (G : Set P) (h : G⫠⫠ ⊆ G) : Fact P where carrier := G property := by grind [isFact, orth_extensive] @@ -187,8 +187,8 @@ lemma dual_subset_dual {G H : Set P} (h : G ⊆ H) : H⫠ ⊆ G⫠ := fun _ hp _ hq => hp _ (h hq) /-- Construct a fact from a set G and a proof that G equals the orthogonal of some set H. -/ -@[simps!] def Fact.mk_dual (G H : Set P) (h : G = H⫠) : Fact P := - Fact.mk_subset G <| by rw [h, triple_orth] +@[simps!] def Fact.mkDual (G H : Set P) (h : G = H⫠) : Fact P := + Fact.mkSubset G <| by rw [h, triple_orth] lemma coe_mk {X : Set P} {h : isFact X} : ((⟨X, h⟩ : Fact P) : Set P) = X := rfl @@ -205,7 +205,7 @@ lemma orth_one_eq_bot : simpa [orthogonal, mem_setOf, mul_one] using hm /-- The fact given by the dual of G. -/ -@[simps!] def dualFact (G : Set P) : Fact P := Fact.mk_dual (G⫠) G rfl +@[simps!] def dualFact (G : Set P) : Fact P := Fact.mkDual (G⫠) G rfl lemma dual_dual_subset_Fact_iff {G : Set P} {H : Fact P} : G⫠⫠ ⊆ H ↔ G ⊆ H := by constructor <;> rw [H.eq] <;> grind @@ -227,7 +227,7 @@ lemma mul_mem_one (hp : p ∈ (1 : Fact P)) (hq : q ∈ (1 : Fact P)) : p * q grind instance : Top (Fact P) where - top := Fact.mk_subset Set.univ <| fun _ _ => Set.mem_univ _ + top := Fact.mkSubset Set.univ <| fun _ _ => Set.mem_univ _ @[scoped grind =, simp] lemma coe_top : ((⊤ : Fact P) : Set P) = Set.univ := rfl @@ -246,7 +246,7 @@ lemma mem_zero : p ∈ (0 : Fact P) ↔ ∀ q, p * q ∈ PhaseSpace.bot := by simp [← SetLike.mem_coe] instance : Bot (Fact P) where - bot := Fact.mk_dual (PhaseSpace.bot : Set P) {1} (orth_one_eq_bot).symm + bot := Fact.mkDual (PhaseSpace.bot : Set P) {1} (orth_one_eq_bot).symm /-- In a phase space, `G⫠⫠` is the smallest fact containing `G`. -/ lemma biorth_least_fact (G : Set P) : @@ -326,7 +326,7 @@ lemma inter_eq_orth_union_orth (G H : Fact P) : grind [Fact.eq] instance : Min (Fact P) where - min G H := Fact.mk_dual (G ∩ H) (G⫠ ∪ H⫠) <| by simp + min G H := Fact.mkDual (G ∩ H) (G⫠ ∪ H⫠) <| by simp @[simp] lemma coe_min {G H : Fact P} : ((G ⊓ H : Fact P) : Set P) = (G : Set P) ∩ H := rfl @@ -394,7 +394,7 @@ def parr (X Y : Fact P) : Fact P := dualFact ((X⫠) * (Y⫠)) refine SetLike.coe_injective ?_ rw [tensor] refine Set.Subset.antisymm ?_ ?_ - · simp only [dualFact, mk_dual, mk_subset, coe_mk] + · simp only [dualFact, mkDual, mkSubset, coe_mk] rw [dual_dual_subset_Fact_iff] grind [SetLike.mem_coe, Set.mem_mul] · exact Set.Subset.trans (orth_extensive _) <| orth_antitone <| orth_antitone <| @@ -417,7 +417,7 @@ lemma coe_tensor_assoc {G H K : Fact P} : ((G ⊗ H) ⊗ K : Set P) = ((G : Set P) * ((H : Set P) * (K : Set P)))⫠⫠ := by simp only [tensor] refine Set.Subset.antisymm ?_ ?_ - · simp only [dualFact, mk_dual, mk_subset, coe_mk, dual_dual_subset_dual_iff] + · simp only [dualFact, mkDual, mkSubset, coe_mk, dual_dual_subset_dual_iff] rw [K.eq] refine tensor_assoc_aux.trans ?_ rw [← K.eq] @@ -442,7 +442,7 @@ lemma tensor_le_tensor {G K H} {L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : (G lemma tensor_of_par {G H : Fact P} : (G ⊗ H) = (Gᗮ ⅋ Hᗮ)ᗮ := SetLike.coe_injective <| by - simp only [tensor, parr, dualFact, mk_dual, mk_subset, coe_mk] + simp only [tensor, parr, dualFact, mkDual, mkSubset, coe_mk] rw [G.eq, H.eq] #adaptation_note /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ @@ -471,7 +471,7 @@ def linImpl (X Y : Fact P) : Fact P := dualFact ((X : Set P) * (Y : Set P)⫠) lemma linImpl_of_tensor {G H : Fact P} : (G ⊸ H) = (G ⊗ Hᗮ)ᗮ := SetLike.coe_injective <| by - simp only [linImpl, tensor, coe_neg, dualFact, mk_dual, mk_subset, coe_mk] + simp only [linImpl, tensor, coe_neg, dualFact, mkDual, mkSubset, coe_mk] apply Set.Subset.antisymm <;> grind lemma par_of_linImpl {G H : Fact P} : (G ⅋ H) = (Gᗮ ⊸ H) := @@ -589,14 +589,14 @@ lemma le_plus_right {G H : Fact P} : H ≤ G ⊕ H := fun _ hx ↦ lemma tensor_distrib_plus : (G ⊗ (H ⊕ K) : Fact P) = (G ⊗ H) ⊕ (G ⊗ K) := by refine SetLike.coe_injective <| Set.Subset.antisymm ?_ ?_ - · rw [tensor, dualFact, mk_dual_coe, oplus, dualFact, mk_dual_coe] + · rw [tensor, dualFact, mkDual_coe, oplus, dualFact, mkDual_coe] rw [dual_dual_subset_Fact_iff, G.eq] refine tensor_assoc_aux.trans ?_ - rw [Set.mul_union, oplus, dualFact, mk_dual_coe, tensor, dualFact, mk_dual_coe] + rw [Set.mul_union, oplus, dualFact, mkDual_coe, tensor, dualFact, mkDual_coe] exact dual_subset_dual <| dual_subset_dual <| Set.union_subset_union subset_dual_dual subset_dual_dual - · rw [oplus, dualFact, mk_dual_coe, dual_dual_subset_Fact_iff, tensor, dualFact, mk_dual_coe, - tensor, dualFact, mk_dual_coe, Set.union_subset_iff] + · rw [oplus, dualFact, mkDual_coe, dual_dual_subset_Fact_iff, tensor, dualFact, mkDual_coe, + tensor, dualFact, mkDual_coe, Set.union_subset_iff] simp only [dual_dual_subset_Fact_iff] exact ⟨(Set.mul_subset_mul_left le_plus_left).trans mul_subset_tensor, (Set.mul_subset_mul_left le_plus_right).trans mul_subset_tensor⟩ @@ -640,7 +640,7 @@ lemma par_semi_distrib_plus : ((G ⅋ H) ⊕ (G ⅋ K) : Fact P) ≤ G ⅋ (H rw [coe_top] rw [Set.eq_univ_iff_forall] intro x - simp only [parr, dualFact, mk_dual, mk_subset, coe_mk, coe_top] + simp only [parr, dualFact, mkDual, mkSubset, coe_mk, coe_top] rw [PhaseSpace.orthogonal_def, Set.mem_setOf_eq] intro w hw rcases Set.mem_mul.mp hw with ⟨y, hy, z, hz, rfl⟩ diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index fd3853c56..b1a8947e2 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -183,12 +183,12 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit | implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx) /-- Weakening the theory only. -/ -def Theory.Derivation.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} +def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') : T⇓(Γ ⊢ A) → T'⇓(Γ ⊢ A):= Derivation.weak hTheory Finset.Subset.rfl /-- Weakening the context only. -/ -def Theory.Derivation.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} +def Theory.Derivation.weakCtx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hCtx : Γ ⊆ Δ) : T⇓(Γ ⊢ A) → T⇓(Δ ⊢ A) := Derivation.weak Set.Subset.rfl hCtx @@ -198,14 +198,14 @@ theorem DerivableIn.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Propositio | ⟨D⟩ => ⟨D.weak hTheory hCtx⟩ /-- Proof irrelevant weakening of the theory. -/ -theorem DerivableIn.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} +theorem DerivableIn.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') : DerivableIn T (Γ ⊢ A) → DerivableIn T' (Γ ⊢ A) - | ⟨D⟩ => ⟨D.weak_theory hTheory⟩ + | ⟨D⟩ => ⟨D.weakTheory hTheory⟩ /-- Proof irrelevant weakening of the context. -/ -theorem DerivableIn.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} +theorem DerivableIn.weakCtx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hCtx : Γ ⊆ Δ) : DerivableIn T (Γ ⊢ A) → DerivableIn T (Δ ⊢ A) - | ⟨D⟩ => ⟨D.weak_ctx hCtx⟩ + | ⟨D⟩ => ⟨D.weakCtx hCtx⟩ /-- Implement the cut rule, removing a hypothesis `A` from `E` using a derivation `D`. This is *not* @@ -213,9 +213,9 @@ substitution, which would replace appeals to `A` in `E` by the whole derivation -/ def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} (D : T⇓(Γ ⊢ A)) (E : T⇓(insert A Δ ⊢ B)) : T⇓((Γ ∪ Δ) ⊢ B) := by - refine implE (A := A) ?_ (D.weak_ctx Finset.subset_union_left) + refine implE (A := A) ?_ (D.weakCtx Finset.subset_union_left) have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind - exact implI (Γ ∪ Δ) <| E.weak_ctx this + exact implI (Γ ∪ Δ) <| E.weakCtx this /-- Proof irrelevant cut rule. -/ theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} : @@ -228,7 +228,7 @@ theorem DerivableIn.cut_away {Γ Γ' : Ctx Atom} {B : Proposition Atom} (hΔ : ∀ A ∈ Γ', DerivableIn T (Γ ⊢ A)) (hDer : DerivableIn T ((Γ ∪ Γ') ⊢ B)) : DerivableIn T (Γ ⊢ B) := by induction Γ' using Finset.induction with - | empty => exact DerivableIn.weak_ctx (by grind) hDer + | empty => exact DerivableIn.weakCtx (by grind) hDer | insert A Δ hA ih => apply ih · intro A' hA' @@ -246,7 +246,7 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} | @ass _ _ _ _ B hB => by by_cases B ∈ Γ' case pos h => - exact (Ds B h).weak_ctx <| by grind + exact (Ds B h).weakCtx <| by grind case neg h => exact ass <| by grind | andI E E' => andI (E.subs Ds) (E'.subs Ds) @@ -257,13 +257,13 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} | @orE _ _ _ _ C C' _ E E' E'' .. => by apply orE (E.subs Ds) · rw [show insert C (Γ \ Γ' ∪ Δ) = (insert C Γ \ Γ') ∪ insert C Δ by grind] - exact E'.subs Ds |>.weak_ctx (by grind) + exact E'.subs Ds |>.weakCtx (by grind) · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind] - exact E''.subs Ds |>.weak_ctx (by grind) + exact E''.subs Ds |>.weakCtx (by grind) | @implI _ _ _ A' _ _ E .. => by apply implI rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind] - exact E.subs Ds |>.weak_ctx (by grind) + exact E.subs Ds |>.weakCtx (by grind) | implE E E' => implE (E.subs Ds) (E'.subs Ds) /-- Transport a derivation along a substitution of atoms. -/ @@ -300,9 +300,9 @@ theorem derivableIn_top [Inhabited Atom] : DerivableIn T (⊤ : Proposition Atom theorem derivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) : DerivableIn T A ↔ A ≡[T] ⊤ := by constructor <;> intro h - · refine ⟨derivationTop.weak_ctx <| by grind, ?_⟩ + · refine ⟨derivationTop.weakCtx <| by grind, ?_⟩ let D := Classical.choice h - exact D.weak_ctx <| by grind + exact D.weakCtx <| by grind · have := DerivableIn.cut (derivableIn_top (T := T)) (B := A) (Δ := ∅) rw [←show (∅ : Ctx Atom) = ∅ ∪ ∅ by rfl] at this exact this h.mpr diff --git a/CslibTests/CLL.lean b/CslibTests/CLL.lean index 47c6bda61..55f15b98f 100644 --- a/CslibTests/CLL.lean +++ b/CslibTests/CLL.lean @@ -119,15 +119,15 @@ example (h : (a : P) ≡ b) : b ≡ a := Proposition.Equiv.symm h example (hab : (a : P) ≡ b) (hbc : b ≡ c) : a ≡ c := Proposition.Equiv.trans hab hbc -- Coercion from proof-relevant to proof-irrelevant (via .toProp) -example : (!⊤ : P) ≡ 1 := Proposition.bang_top_eqv_one.toProp -example : (ʔ0 : P) ≡ ⊥ := Proposition.quest_zero_eqv_bot.toProp -example : (a ⊗ 0 : P) ≡ 0 := (Proposition.tensor_zero_eqv_zero a).toProp -example : (a ⅋ ⊤ : P) ≡ ⊤ := (Proposition.parr_top_eqv_top a).toProp -example : (a ⊗ b : P) ≡ b ⊗ a := Proposition.tensor_symm.toProp -example : (a ⊗ (b ⊗ c) : P) ≡ (a ⊗ b) ⊗ c := Proposition.tensor_assoc.toProp -example : (a ⊗ (b ⊕ c) : P) ≡ (a ⊗ b) ⊕ (a ⊗ c) := (Proposition.tensor_distrib_oplus a b c).toProp -example : (a ⊕ a : P) ≡ a := Proposition.oplus_idem.toProp -example : (a & a : P) ≡ a := Proposition.with_idem.toProp +example : (!⊤ : P) ≡ 1 := Proposition.bangTopEqvOne.toProp +example : (ʔ0 : P) ≡ ⊥ := Proposition.questZeroEqvBot.toProp +example : (a ⊗ 0 : P) ≡ 0 := (Proposition.tensorZeroEqvZero a).toProp +example : (a ⅋ ⊤ : P) ≡ ⊤ := (Proposition.parrTopEqvTop a).toProp +example : (a ⊗ b : P) ≡ b ⊗ a := Proposition.tensorSymm.toProp +example : (a ⊗ (b ⊗ c) : P) ≡ (a ⊗ b) ⊗ c := Proposition.tensorAssoc.toProp +example : (a ⊗ (b ⊕ c) : P) ≡ (a ⊗ b) ⊕ (a ⊗ c) := (Proposition.tensorDistribOplus a b c).toProp +example : (a ⊕ a : P) ≡ a := Proposition.oplusIdem.toProp +example : (a & a : P) ≡ a := Proposition.withIdem.toProp /-! ## Proof-relevant equivalence tests -/ @@ -142,25 +142,25 @@ example (h : (a : P) ≡⇓ b) : b ≡⇓ a := Proposition.equiv.symm a h example (hab : (a : P) ≡⇓ b) (hbc : (b : P) ≡⇓ c) : a ≡⇓ c := Proposition.equiv.trans hab hbc -- Proof-relevant versions of logical equivalences -example : (!⊤ : P) ≡⇓ 1 := Proposition.bang_top_eqv_one -example : (ʔ0 : P) ≡⇓ ⊥ := Proposition.quest_zero_eqv_bot -example : (a ⊗ b : P) ≡⇓ b ⊗ a := Proposition.tensor_symm -example : (a ⊗ (b ⊗ c) : P) ≡⇓ (a ⊗ b) ⊗ c := Proposition.tensor_assoc -example : (a ⊕ a : P) ≡⇓ a := Proposition.oplus_idem -example : (a & a : P) ≡⇓ a := Proposition.with_idem +example : (!⊤ : P) ≡⇓ 1 := Proposition.bangTopEqvOne +example : (ʔ0 : P) ≡⇓ ⊥ := Proposition.questZeroEqvBot +example : (a ⊗ b : P) ≡⇓ b ⊗ a := Proposition.tensorSymm +example : (a ⊗ (b ⊗ c) : P) ≡⇓ (a ⊗ b) ⊗ c := Proposition.tensorAssoc +example : (a ⊕ a : P) ≡⇓ a := Proposition.oplusIdem +example : (a & a : P) ≡⇓ a := Proposition.withIdem /-! ## Inversion tests -/ --- parr_inversion -example (h : ⇓({a ⅋ b} : Sequent Nat)) : ⇓({a, b} : Sequent Nat) := Proof.parr_inversion h +-- parrInversion +example (h : ⇓({a ⅋ b} : Sequent Nat)) : ⇓({a, b} : Sequent Nat) := Proof.parrInversion h --- bot_inversion -example (h : ⇓({⊥, 1} : Sequent Nat)) : ⇓({1} : Sequent Nat) := Proof.bot_inversion h +-- botInversion +example (h : ⇓({⊥, 1} : Sequent Nat)) : ⇓({1} : Sequent Nat) := Proof.botInversion h -- with_inversion -example (h : ⇓({a & b} : Sequent Nat)) : ⇓({a} : Sequent Nat) := Proof.with_inversion₁ h -example (h : ⇓({a & b} : Sequent Nat)) : ⇓({b} : Sequent Nat) := Proof.with_inversion₂ h +example (h : ⇓({a & b} : Sequent Nat)) : ⇓({a} : Sequent Nat) := Proof.withInversion₁ h +example (h : ⇓({a & b} : Sequent Nat)) : ⇓({b} : Sequent Nat) := Proof.withInversion₂ h /-! ## Positive/Negative classification tests -/ diff --git a/lake-manifest.json b/lake-manifest.json index ca8591cf3..1b6933333 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "rev": "d8de6b61f073daf518577b643724875545b98e89", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "inputRev": "d8de6b61f073daf518577b643724875545b98e89", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "4ee56e687ce2b9b51b097bfa65947a499da0c453", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 4169d4b8e..92c711279 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5" +rev = "d8de6b61f073daf518577b643724875545b98e89" [[lean_lib]] name = "Cslib"