From 6d112db496f8528f4991fd7be32257e89861a4d7 Mon Sep 17 00:00:00 2001 From: thomaskwaring <51426330+thomaskwaring@users.noreply.github.com> Date: Wed, 29 Apr 2026 17:57:59 +0200 Subject: [PATCH 1/3] feat: add Logics/Propositional/NaturalDeduction/* (#91) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit # Natural deduction for minimal logic This PR adds the definitions and basic properties of natural deduction for propositional logic. Key developments: - Definition of `Theory.Derivation`, the type of derivation trees. - Definitions of derivability and equivalence. - Operations on derivations: weakening, substitution and cut. --------- Co-authored-by: twwar Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Claude Co-authored-by: Chris Henson Co-authored-by: Shrys Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou Co-authored-by: Fabrizio Montesi Co-authored-by: Maximiliano Onofre-Martínez Co-authored-by: Tristan F.-R. Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: euprunin Co-authored-by: kei <70096720+thelissimus@users.noreply.github.com> Co-authored-by: Juan Pablo Yamamoto Co-authored-by: Alexandre Rademaker Co-authored-by: Clark Barrett Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> Co-authored-by: Xueying Qin <32066429+XYUnknown@users.noreply.github.com> Co-authored-by: Jesse Alama Co-authored-by: mathlib4-bot Co-authored-by: milianoPhilosophyHub Co-authored-by: Tanner Duve <122851174+tannerduve@users.noreply.github.com> Co-authored-by: Tanner Duve Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: ADA <120643053+ADA-Projects@users.noreply.github.com> Co-authored-by: Aristotle Harmonic Co-authored-by: Sorrachai Yingchareonthawornchai Co-authored-by: Chris-F5 <60847556+Chris-F5@users.noreply.github.com> Co-authored-by: Garmelon Co-authored-by: Arjun Bhamra <33864884+abhamra@users.noreply.github.com> Co-authored-by: Bolton Bailey Co-authored-by: Benjamin Bisping Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com> Co-authored-by: Burkhardt Renz Co-authored-by: Eric Wieser Co-authored-by: Elimia <56419338+sehun1024@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Eric Wieser Co-authored-by: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com> Co-authored-by: Pieter Cuijpers Co-authored-by: Marcelo Lynch Co-authored-by: Kim Morrison --- Cslib.lean | 1 + Cslib/Logics/Propositional/Defs.lean | 52 ++- .../Propositional/NaturalDeduction/Basic.lean | 383 ++++++++++++++++++ 3 files changed, 408 insertions(+), 28 deletions(-) create mode 100644 Cslib/Logics/Propositional/NaturalDeduction/Basic.lean diff --git a/Cslib.lean b/Cslib.lean index 7db43680b0..37a038ee41 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -130,3 +130,4 @@ public import Cslib.Logics.LinearLogic.CLL.EtaExpansion public import Cslib.Logics.LinearLogic.CLL.MLL public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic public import Cslib.Logics.Propositional.Defs +public import Cslib.Logics.Propositional.NaturalDeduction.Basic diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index ef41651dee..fa3caf53e2 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -21,14 +21,16 @@ instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited. - `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion. - `IsClassical` : an intuitionistic theory is classical if it further contains double negation elimination. -- `Proposition.map`, `Theory.map` : a map between `Atom` types extends to a map between -propositions and theories. +- `Proposition.subst` : replace `atom x` in a `A : Proposition Atom` with `f x`, for a function + `f : Atom → Proposition Atom'`. This induces a monad structure on `Proposition`, with + `pure := Proposition.atom`. `Theory` is a functor, by mapping each proposition `A ∈ T` to + `f <$> A`. - `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given theory. ## Notation -We introduce notation for the logical connectives: `⊥ ⊤ ⋏ ⋎ ⟶ ~` for, respectively, falsum, verum, +We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum, conjunction, disjunction, implication and negation. -/ @@ -70,37 +72,31 @@ example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl @[inherit_doc] scoped infix:30 " → " => Proposition.impl @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg -/-- A function on atoms induces a function on propositions. -/ -def Proposition.map {Atom Atom' : Type u} (f : Atom → Atom') : Proposition Atom → Proposition Atom' - | atom x => atom (f x) - | and A B => (A.map f) ∧ (B.map f) - | or A B => (A.map f) ∨ (B.map f) - | impl A B => (A.map f) → (B.map f) - -instance {Atom Atom' : Type u} : FunLike (Atom → Atom') (Proposition Atom) (Proposition Atom') where - coe := Proposition.map - coe_injective' f f' h := by - ext x - have : (Proposition.atom x).map f = (Proposition.atom x).map f' := - congrFun h (Proposition.atom x) - grind [Proposition.map] +/-- Substitute each atom in a proposition for a proposition, possibly changing the atomic +language. -/ +def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') : + Proposition Atom → Proposition Atom' + | atom x => f x + | and A B => (A.subst f) ∧ (B.subst f) + | or A B => (A.subst f) ∨ (B.subst f) + | impl A B => (A.subst f) → (B.subst f) + +-- This is probably a lawful monad, but that doesn't seem to be important. +instance : Monad Proposition where + pure := .atom + bind A f := A.subst f /-- Theories are arbitrary sets of propositions. -/ abbrev Theory (Atom) := Set (Proposition Atom) namespace Theory -/-- Extend `Proposition.map` to theories. -/ -def map {Atom Atom' : Type u} (f : Atom → Atom') : Theory Atom → Theory Atom' := - Set.image (Proposition.map f) +/-- Extend a substitution from `Proposition` to `Theory`. -/ +protected def subst {Atom Atom' : Type u} (T : Theory Atom) (f : Atom → Proposition Atom') : + Theory Atom' := T.image (· >>= f) -instance {Atom Atom' : Type u} : FunLike (Atom → Atom') (Theory Atom) (Theory Atom') where - coe := Theory.map - coe_injective' f f' h := by - ext x - have : Theory.map f {Proposition.atom x} = Theory.map f' {Proposition.atom x} := - congrFun h {Proposition.atom x} - simpa [Theory.map, Proposition.map] using this +instance : Functor Theory where + map f := Set.image (f <$> ·) /-- The empty theory corresponds to minimal propositional logic. -/ abbrev MPL : Theory (Atom) := ∅ @@ -150,7 +146,7 @@ theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] /-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ @[reducible] def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) := - T.map (WithBot.some) ∪ IPL + (WithBot.some <$> T) ∪ IPL instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) : IsIntuitionistic T.intuitionisticCompletion := by grind diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean new file mode 100644 index 0000000000..ba3f5bbacb --- /dev/null +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -0,0 +1,383 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +module + +public import Cslib.Logics.Propositional.Defs +public import Cslib.Foundations.Logic.InferenceSystem +public import Mathlib.Data.Finset.Insert +public import Mathlib.Data.Finset.SDiff +public import Mathlib.Data.Finset.Image + +@[expose] public section + +/-! # Natural deduction for propositional logic + +We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a +`Theory` (set of propositions). + +## Main definitions + +- `Sequent` : a pair of a context and conclusion. +- `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit +hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction +and exchange, and the axiom rule derives `Γ ⊢ A` for any context `Γ` with `A ∈ Γ`, allowing +weakening to be a derived rule. The derivation may appeal to hypotheses from the `Theory T`. This +defines an instance of `InferenceSystem T Sequent`. +- `Theory.equiv` : `Type`-valued equivalence of propositions. +- `Theory.Equiv` : `Prop`-valued equivalence of propositions. + +## Main results + +- `Derivation.weak` : weakening as a derived rule. +- `Derivation.cut`, `Derivation.subs` : replace a hypothesis in a derivation — the two versions +differ in the construction of the relevant derivation. +- `Theory.equiv_equivalence` : equivalence of propositions is an equivalence relation. + +## Notation + +The sequent `⟨Γ, A⟩` is notated `Γ ⊢ A`, so that a derivation using axioms from a theory `T` is +noted `T⇓(Γ ⊢ A)`. We define also an `InferenceSystem T (Proposition Atom)`, so that `T⇓A` +abbreviates a derivation of `A` in the empty context: `T⇓(∅ ⊢ A)`. + +## Implementation notes + +We formalise here a single type of derivations, meaning there is a single collection of inference +rules (those for minimal logic). The extension to intuitionistic and classical logic are modelled +by adding *axioms* --- for instance, intuitionistic derivations are allowed to appeal to axioms of +the form `⊥ → A` for any proposition `A`. This differs from many on-paper presentations, which add +that principle as a deduction rule: from `Γ ⊢ ⊥` derive `Γ ⊢ A`. Discussion on proper way to +capture such developments in cslib is ongoing, see the following +[zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Logic/with/585843520). + +## References + +- Dag Prawitz, *Natural Deduction: a proof-theoretical study*. +- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely +presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*, and +in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (Suggestions of better +references welcome!) +-/ + +universe u + +namespace Cslib.Logic.PL + +open Proposition Theory InferenceSystem DerivableIn + +variable {Atom : Type u} [DecidableEq Atom] + +/-- Contexts are finsets of propositions. -/ +abbrev Ctx (Atom) := Finset (Proposition Atom) + +/-- Map a context along a substitution. -/ +def Ctx.subst {Atom Atom' : Type u} [DecidableEq Atom'] (f : Atom → Proposition Atom') : + Ctx Atom → Ctx Atom' := Finset.image (· >>= f) + +/-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ +abbrev Sequent {Atom} := Ctx Atom × Proposition Atom + +@[inherit_doc Sequent] +scoped notation Γ:60 " ⊢ " A => (⟨Γ, A⟩ : Sequent) + +/-- A `T`-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ, +possibly appealing to axioms from `T`. -/ +inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom → Type u where + /-- Axiom -/ + | ax {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ T) : Derivation Γ A + /-- Assumption -/ + | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A + /-- Conjunction introduction -/ + | andI {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B) + /-- Conjunction elimination left -/ + | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ A + /-- Conjunction elimination right -/ + | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ B + /-- Disjunction introduction left -/ + | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ (A ∨ B) + /-- Disjunction introduction right -/ + | orI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A ∨ B) + /-- Disjunction elimination -/ + | orE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A ∨ B) → + Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C + /-- Implication introduction -/ + | implI {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation (insert A Γ) B → Derivation Γ (A → B) + /-- Implication elimination -/ + | implE {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B + +/-- Inference system for derivations under the theory `T`. -/ +instance (T : Theory Atom) : InferenceSystem T (Sequent (Atom := Atom)) where + derivation S := T.Derivation S.1 S.2 + +/-- Inference system for propositions (using the empty context). -/ +instance (T : Theory Atom) : InferenceSystem T (Proposition Atom) where + derivation A := T.Derivation ∅ A + +variable {T : Theory Atom} + +theorem Theory.Derivation.emptySequent_eq {A : Proposition Atom} : T⇓A = T⇓(∅ ⊢ A) := rfl + +theorem DerivableIn.iff_derivableIn_empty {A : Proposition Atom} : + DerivableIn T A ↔ DerivableIn T (∅ ⊢ A) := by rfl + +/-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ +def Theory.equiv (A B : Proposition Atom) := + T⇓({A} ⊢ B) × T⇓({B} ⊢ A) + +/-- Forward direction of an equivalence. -/ +def Theory.equiv.mp {A B : Proposition Atom} (e : T.equiv A B) : T⇓({A} ⊢ B) := e.1 + +/-- Reverse direction of an equivalence. -/ +def Theory.equiv.mpr {A B : Proposition Atom} (e : T.equiv A B) : T⇓({B} ⊢ A) := e.2 + +/-- `A` and `B` are T-equivalent if `T.equiv A B` is nonempty. -/ +def Theory.Equiv (A B : Proposition Atom) := Nonempty (T.equiv A B) + +@[inherit_doc] +scoped notation A " ≡[" T' "] " B:29 => Theory.Equiv (T := T') A B + +lemma Theory.Equiv.mp {A B : Proposition Atom} (h : A ≡[T] B) : DerivableIn T ({A} ⊢ B) := + ⟨h.some.mp⟩ + +lemma Theory.Equiv.mpr {A B : Proposition Atom} (h : A ≡[T] B) : DerivableIn T ({B} ⊢ A) := + ⟨h.some.mpr⟩ + +theorem Theory.equiv_iff {A B : Proposition Atom} : + A ≡[T] B ↔ DerivableIn T ({A} ⊢ B) ∧ DerivableIn T ({B} ⊢ A) := by + constructor + · intro h + exact ⟨h.mp, h.mpr⟩ + · intro ⟨⟨D⟩, ⟨E⟩⟩ + exact ⟨D, E⟩ + +/-- Minimally equivalent propositions. -/ +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv + +@[inherit_doc] +scoped infix:29 " ≡ " => Equiv + +open Derivation DerivableIn + +/-! ### Operations on derivations -/ + +/-- Weakening is a derived rule. -/ +def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} + (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : T.Derivation Γ A → T'.Derivation Δ A + | ax hA => ax <| hTheory hA + | ass hA => ass <| hCtx hA + | andI D D' => andI (D.weak hTheory hCtx) (D'.weak hTheory hCtx) + | andE₁ D => andE₁ <| D.weak hTheory hCtx + | andE₂ D => andE₂ <| D.weak hTheory hCtx + | orI₁ D => orI₁ <| D.weak hTheory hCtx + | orI₂ D => orI₂ <| D.weak hTheory hCtx + | orE D D' D'' => + orE (D.weak hTheory hCtx) + (D'.weak hTheory <| Finset.insert_subset_insert _ hCtx) + (D''.weak hTheory <| Finset.insert_subset_insert _ hCtx) + | @implI _ _ _ A B Γ D => implI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx + | 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} + (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} + (hCtx : Γ ⊆ Δ) : T⇓(Γ ⊢ A) → T⇓(Δ ⊢ A) := + Derivation.weak Set.Subset.rfl hCtx + +/-- Proof irrelevant weakening. -/ +theorem DerivableIn.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} + (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : DerivableIn T (Γ ⊢ A) → DerivableIn T' (Δ ⊢ A) + | ⟨D⟩ => ⟨D.weak hTheory hCtx⟩ + +/-- Proof irrelevant weakening of the theory. -/ +theorem DerivableIn.weak_theory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} + (hTheory : T ⊆ T') : DerivableIn T (Γ ⊢ A) → DerivableIn T' (Γ ⊢ A) + | ⟨D⟩ => ⟨D.weak_theory hTheory⟩ + +/-- Proof irrelevant weakening of the context. -/ +theorem DerivableIn.weak_ctx {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} + (hCtx : Γ ⊆ Δ) : DerivableIn T (Γ ⊢ A) → DerivableIn T (Δ ⊢ A) + | ⟨D⟩ => ⟨D.weak_ctx hCtx⟩ + +/-- +Implement the cut rule, removing a hypothesis `A` from `E` using a derivation `D`. This is *not* +substitution, which would replace appeals to `A` in `E` by the whole derivation `D`. +-/ +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) + have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind + exact implI (Γ ∪ Δ) <| E.weak_ctx this + +/-- Proof irrelevant cut rule. -/ +theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} : + DerivableIn T (Γ ⊢ A) → DerivableIn T ((insert A Δ) ⊢ B) → DerivableIn T ((Γ ∪ Δ) ⊢ B) + | ⟨D⟩, ⟨E⟩ => ⟨D.cut E⟩ + +/-- Remove unnecessary hypotheses. This can't be computable because it requires picking an order +on the finset `Δ`. -/ +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 + | insert A Δ hA ih => + apply ih + · intro A' hA' + exact hΔ A' <| Finset.mem_insert_of_mem hA' + · apply Finset.union_left_idem Γ Δ ▸ DerivableIn.cut (Δ := Γ ∪ Δ) + · exact hΔ A <| Finset.mem_insert_self A Δ + · rwa [← Finset.union_insert A Γ Δ] + +/-- Substitution of a family of derivations `D` for hypotheses in the context `Γ` of `E`. TODO: +this implementation is not capture avoiding. -/ +def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} + (Ds : ∀ A ∈ Γ', T⇓(Δ ⊢ A)) : + T.Derivation Γ B → T.Derivation (Γ \ Γ' ∪ Δ) B + | ax hB => ax hB + | @ass _ _ _ _ B hB => by + by_cases B ∈ Γ' + case pos h => + exact (Ds B h).weak_ctx <| by grind + case neg h => + exact ass <| by grind + | andI E E' => andI (E.subs Ds) (E'.subs Ds) + | andE₁ E => andE₁ <| E.subs Ds + | andE₂ E => andE₂ <| E.subs Ds + | orI₁ E => orI₁ <| E.subs Ds + | orI₂ E => orI₂ <| E.subs Ds + | @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) + · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind] + exact E''.subs Ds |>.weak_ctx (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) + | implE E E' => implE (E.subs Ds) (E'.subs Ds) + +/-- Transport a derivation along a substitution of atoms. -/ +def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] + {T : Theory Atom} (f : Atom → Proposition Atom') {Γ : Ctx Atom} {B : Proposition Atom} : + T.Derivation Γ B → (T.subst f).Derivation (Γ.subst f) (B >>= f) + | ax h => ax <| Set.mem_image_of_mem (· >>= f) h + | ass h => ass <| Finset.mem_image_of_mem (· >>= f) h + | andI D E => andI (D.substAtom f) (E.substAtom f) + | andE₁ D => andE₁ (D.substAtom f) + | andE₂ D => andE₂ (D.substAtom f) + | orI₁ D => orI₁ (D.substAtom f) + | orI₂ D => orI₂ (D.substAtom f) + | orE D E E' => orE (D.substAtom f) + ((Finset.image_insert (· >>= f) _ _) ▸ E.substAtom f) + ((Finset.image_insert (· >>= f) _ _) ▸ E'.substAtom f) + | implI _ D => implI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) + | implE D E => implE (D.substAtom f) (E.substAtom f) + +theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] + {T : Theory Atom} + (f : Atom → Proposition Atom') {Γ : Ctx Atom} {B : Proposition Atom} : + DerivableIn T (Γ ⊢ B) → DerivableIn (T.subst f) ((Γ.subst f) ⊢ (B >>= f)) + | ⟨D⟩ => ⟨D.substAtom f⟩ + +/-! ### Properties of equivalence -/ + +/-- A derivation of the canonical tautology. -/ +def Theory.derivationTop [Inhabited Atom] : T⇓(⊤ : Proposition Atom) := + implI ∅ <| ass <| by grind + +theorem derivableIn_top [Inhabited Atom] : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩ + +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, ?_⟩ + let D := Classical.choice h + exact D.weak_ctx <| by grind + · have := DerivableIn.cut (derivableIn_top (T := T)) (B := A) (Δ := ∅) + rw [←show (∅ : Ctx Atom) = ∅ ∪ ∅ by rfl] at this + exact this h.mpr + +namespace Theory + +/-- Change the conclusion along an equivalence. -/ +def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : T.equiv A B) + (D : T⇓(Γ ⊢ A)) : T⇓(Γ ⊢ B) := + Γ.union_empty ▸ Derivation.cut (Δ := ∅) D e.1 + +/-- Replace a hypothesis along an equivalence. -/ +def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : T.equiv A B) + (C : Proposition Atom) (D : T⇓(insert A Γ ⊢ C)) : T⇓(insert B Γ ⊢ C) := by + have : insert B Γ = {B} ∪ Γ := rfl + exact this ▸ Derivation.cut e.2 D + +/-- An equivalence of a proposition with itself. -/ +def equiv.refl (A : Proposition Atom) : T.equiv A A := + let D : T⇓({A} ⊢ A) := ass <| Finset.mem_singleton_self A; + ⟨D, D⟩ + +/-- Reverse an equivalence. -/ +def equiv.symm {A B : Proposition Atom} (e : T.equiv A B) : T.equiv B A := + ⟨e.mpr, e.mp⟩ + +/-- Compose two equivalences. -/ +def equiv.trans {A B C : Proposition Atom} (eAB : T.equiv A B) + (eBC : T.equiv B C) : T.equiv A C := + ⟨mapEquivConclusion _ eBC eAB.mp, mapEquivConclusion _ eAB.symm eBC.mpr⟩ + +/-- `A` and `B` are equivalent (in `T`) iff they are provable from the same contexts. -/ +theorem equiv_iff_equiv_derivableIn {A B : Proposition Atom} : + A ≡[T] B ↔ ∀ Γ : Ctx Atom, DerivableIn T (Γ ⊢ A) ↔ DerivableIn T (Γ ⊢ B) := by + constructor + · intro ⟨e⟩ Γ + exact ⟨fun D => mapEquivConclusion Γ e D.some, fun D => mapEquivConclusion Γ e.symm D.some⟩ + · intro h + rw [equiv_iff] + constructor + · exact (h {A}).mp ⟨ass <| by grind⟩ + · exact (h {B}).mpr ⟨ass <| by grind⟩ + +/-- `A` and `B` are equivalent (in `T`) iff they have the same strength as hypotheses. -/ +theorem equiv_iff_equiv_derivableIn_hypothesis {A B : Proposition Atom} : + A ≡[T] B ↔ + ∀ (Γ : Ctx Atom) (C : Proposition Atom), + DerivableIn T ((insert A Γ) ⊢ C) ↔ DerivableIn T ((insert B Γ) ⊢ C) := by + constructor + · intro ⟨e⟩ Γ C + exact ⟨fun D => mapEquivHypothesis Γ e C D.some, fun E => mapEquivHypothesis Γ e.symm C E.some⟩ + · intro h + rw [equiv_iff] + constructor + · exact (h ∅ B).mpr ⟨ass <| by grind⟩ + · exact (h ∅ A).mp ⟨ass <| by grind⟩ + +@[refl] +theorem Equiv.refl {T : Theory Atom} (A : Proposition Atom) : A ≡[T] A := by + exact ⟨equiv.refl A⟩ + +theorem Equiv.symm {T : Theory Atom} {A B : Proposition Atom} : + (A ≡[T] B) → B ≡[T] A + | ⟨e⟩ => ⟨e.symm⟩ + +theorem Equiv.trans {T : Theory Atom} {A B C : Proposition Atom} : + (A ≡[T] B) → (B ≡[T] C) → A ≡[T] C + | ⟨e⟩, ⟨e'⟩ => ⟨e.trans e'⟩ + +/-- Equivalence is indeed an equivalence relation. -/ +theorem equiv_equivalence (T : Theory Atom) : Equivalence (T.Equiv (Atom := Atom)) := + ⟨Equiv.refl, Equiv.symm, Equiv.trans⟩ + +/-- The setoid of propositions under equivalence. -/ +protected def propositionSetoid (T : Theory Atom) : Setoid (Proposition Atom) := + ⟨T.Equiv, T.equiv_equivalence⟩ + +end Cslib.Logic.PL.Theory From 6be5d165bb6a6c85bcc574661a50dd22ee6efd68 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Wed, 29 Apr 2026 22:39:25 -0700 Subject: [PATCH 2/3] feat: prove the distributivity of forall over OmegaSequence.flatten (#532) Prove a small result that is useful in a separate work. --- Cslib/Foundations/Data/OmegaSequence/Flatten.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean index acff1fcd01..3f7ba3903a 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean @@ -150,7 +150,7 @@ theorem flatten_drop [Inhabited α] (flatten_take_drop h_ls n).2 /-- `ls n` is the segement from position `ls.cumLen n` to position `ls.cumLen (n + 1) - 1` -of ls.flatten` -/ +of `ls.flatten` -/ @[simp, scoped grind =] theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0) (n : ℕ) : ls.flatten.extract (ls.cumLen n) (ls.cumLen (n + 1)) = ls n := by @@ -159,6 +159,15 @@ theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k have h_take := flatten_take h_ls' 1 grind [extract_eq_drop_take] +/-- Distributivity of "forall" over `flatten`. -/ +theorem forall_flatten_iff [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0) + (p : α → Prop) : (∀ n, p (ls.flatten n)) ↔ ∀ k, (ls k).Forall p := by + constructor + · simp only [List.forall_iff_forall_mem, List.forall_mem_iff_getElem, ← extract_flatten h_ls] + grind + · have := segment_upper_bound (cumLen_strictMono h_ls) + grind [List.forall_iff_forall_mem, flatten_def] + /-- Given an ω-sequence `s` and a function `f : ℕ → ℕ`, `s.toSegs f` is the ω-sequence whose `n`-th element is the list `s.extract (f n) (f (n + 1))`. In all its uses, the function `f` will always be assumed to be strictly monotonic with `f 0 = 0`. -/ From 1ffe90657c494809afe2519ab54756e9a165aa6c Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 4 May 2026 12:28:47 +0200 Subject: [PATCH 3/3] Tape as int fun --- .../Machines/SingleTapeTuring/Basic.lean | 110 +++++++++------ Cslib/Foundations/Data/BiTape.lean | 126 +++++++++--------- 2 files changed, 133 insertions(+), 103 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 477ab60b14..6a64f5ba82 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -123,24 +123,23 @@ instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance /-- The configurations of a Turing machine consist of: an `Option`al state (or none for the halting state), -and a `BiTape` representing the tape contents. +and a `BiTape` representing the tape. -/ structure Cfg : Type where /-- the state of the TM (or none for the halting state) -/ state : Option tm.State - /-- the BiTape contents -/ + /-- the BiTape contents and head position -/ BiTape : BiTape Symbol deriving Inhabited /-- The step function corresponding to a `SingleTapeTM`. -/ -@[simp] def step : tm.Cfg → Option tm.Cfg | ⟨none, _⟩ => -- If in the halting state, there is no next configuration none | ⟨some q', t⟩ => -- If in state q', perform look up in the transition function - match tm.tr q' t.head with + match tm.tr q' t.read with -- and enter a new configuration with state q'' (or none for halting) -- and tape updated according to the Stmt | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ @@ -152,36 +151,13 @@ This is to ensure that distinct lists map to distinct initial configurations. -/ def initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩ + /-- The final configuration corresponding to a list in the output alphabet. (We demand that the head halts at the leftmost position of the output.) -/ +@[simp] def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩ -/-- -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 - -@[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 - -@[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.space_used_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg) - (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 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 - end Cfg open Cfg @@ -198,11 +174,45 @@ def TransitionRelation (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop := /-- A proof of `tm` outputting `l'` on input `l`. -/ def Outputs (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop := - ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') + ReflTransGen tm.TransitionRelation (initCfg tm l) (tm.haltCfg l') /-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/ def OutputsWithinTime (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) := - RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m + RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (tm.haltCfg l') m + +/-- A single step of `tm` increases the size of the support of the tape by at most one +(the position written to). -/ +private lemma step_supportSubset {tm : SingleTapeTM Symbol} {cfg cfg' : tm.Cfg} + {s : Finset ℤ} (hs : cfg.BiTape.supportSubset s) + (hstep : tm.step cfg = some cfg') : + ∃ s' : Finset ℤ, s'.card ≤ s.card + 1 ∧ cfg'.BiTape.supportSubset s' := by + obtain ⟨_ | q, tape⟩ := cfg + · simp [step] at hstep + · simp only [step] at hstep + cases htr : tm.tr q tape.read with + | mk wd q'' => + obtain ⟨wr, dir⟩ := wd + simp only [htr] at hstep + cases hstep + refine ⟨(insert 0 s).image (· + BiTape.optionMoveToInt dir), ?_, ?_⟩ + · exact Finset.card_image_le.trans <| + (Finset.card_insert_le _ _).trans (by omega) + · exact BiTape.supportSubset_optionMove _ _ _ + (BiTape.supportSubset_write_insert _ _ _ hs) + +/-- Iterating the support bound: after `n` steps, the support is contained in a finset +of cardinality at most the initial support's size plus `n`. -/ +private lemma relatesInSteps_supportSubset {tm : SingleTapeTM Symbol} + {cfg cfg' : tm.Cfg} {n : ℕ} + (h : RelatesInSteps tm.TransitionRelation cfg cfg' n) + {s : Finset ℤ} (hs : cfg.BiTape.supportSubset s) : + ∃ s' : Finset ℤ, s'.card ≤ s.card + n ∧ cfg'.BiTape.supportSubset s' := by + induction h with + | refl => exact ⟨s, by omega, hs⟩ + | tail _ _ _ _ hstep ih => + obtain ⟨s', hsc, hss⟩ := ih + obtain ⟨s'', hsc', hss''⟩ := step_supportSubset hss hstep + exact ⟨s'', by omega, hss''⟩ /-- This lemma bounds the size blow-up of the output of a Turing machine. @@ -214,9 +224,25 @@ is bounded by the output length of the first machine. lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ) (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)] + obtain ⟨m, hm, hsteps⟩ := h + have h_init : (tm.initCfg l).BiTape.supportSubset + ((Finset.range l.length).image (Int.ofNat ·)) := by + simpa [initCfg] using BiTape.supportSubset_mk₁ l + obtain ⟨s', hsc, hss⟩ := relatesInSteps_supportSubset hsteps h_init + have h_subset : (Finset.range l'.length).image (Int.ofNat ·) ⊆ s' := by + intro x hx + simp only [Finset.mem_image, Finset.mem_range] at hx + obtain ⟨n, hn, rfl⟩ := hx + apply hss + simp [BiTape.mk₁, hn] + have h_image_card : ((Finset.range l'.length).image (Int.ofNat ·)).card = l'.length := by + rw [Finset.card_image_of_injective _ (fun _ _ h => Int.ofNat.inj h)] + simp + have hcard0 : ((Finset.range l.length).image (Int.ofNat ·)).card ≤ l.length := + Finset.card_image_le.trans (by simp) + have h_le : l'.length ≤ s'.card := h_image_card ▸ Finset.card_le_card h_subset + omega + section Computers @@ -304,7 +330,7 @@ private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) : | none => grind | some q => simp only [step, toCompCfg_left, compComputer] - generalize hM : tm1.tr q BiTape.head = result + generalize hM : tm1.tr q BiTape.read = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result #adaptation_note /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ @@ -320,7 +346,7 @@ private theorem map_toCompCfg_right_step : | none => simp only [step, toCompCfg_right, Option.map_none, compComputer] | some q => - generalize hM : tm2.tr q BiTape.head = result + generalize hM : tm2.tr q BiTape.read = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result simp only [compComputer] grind [toCompCfg_right, step, compComputer] @@ -401,7 +427,12 @@ structure TimeComputable (f : List Symbol → List Symbol) where def TimeComputable.id : TimeComputable (Symbol := Symbol) id where tm := idComputer time_bound _ := 1 - outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩ + outputsFunInTime a := + ⟨1, le_rfl, RelatesInSteps.single (by + change idComputer.step (idComputer.initCfg a) = some (idComputer.haltCfg a) + simp only [step, idComputer, initCfg, haltCfg, BiTape.write_read, + BiTape.optionMove, BiTape.optionMoveToInt, BiTape.moveInt] + ext i; simp)⟩ /-- Time bounds for `compComputer`. @@ -449,9 +480,8 @@ def TimeComputable.comp {f g : List Symbol → List Symbol} 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) - · 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) + apply h_mono + exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a) end TimeComputable diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index ba71605564..6a3ecbfe4f 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -9,8 +9,12 @@ module public import Cslib.Foundations.Data.StackTape public import Mathlib.Computability.TuringMachine.Tape public import Mathlib.Data.Finset.Attr +public import Mathlib.Data.Finset.Range +public import Mathlib.Data.Finset.Card +public import Mathlib.Data.Finset.Image public import Mathlib.Tactic.SetLike public import Mathlib.Algebra.Order.Group.Nat +public import Mathlib.Tactic.Ring /-! # BiTape: Bidirectionally infinite TM tape representation using StackTape @@ -40,24 +44,17 @@ will not collide. namespace Turing -/-- -A structure for bidirectionally-infinite Turing machine tapes -that eventually take on blank `none` values --/ +@[ext] structure BiTape (Symbol : Type) where - /-- The symbol currently under the tape head -/ - head : Option Symbol - /-- The contents to the left of the head -/ - left : StackTape Symbol - /-- The contents to the right of the head -/ - right : StackTape Symbol + /-- the tape contents -/ + cells : ℤ → Option Symbol namespace BiTape variable {Symbol : Type} /-- The empty `BiTape` -/ -def nil : BiTape Symbol := ⟨none, ∅, ∅⟩ +def nil : BiTape Symbol := ⟨fun _ => none⟩ instance : Inhabited (BiTape Symbol) where default := nil @@ -73,75 +70,78 @@ Given a `List` of `Symbol`s, construct a `BiTape` by mapping the list to `some` and laying them out to the right side, 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 } +def mk₁ {Symbol : Type} (l : List Symbol) : BiTape Symbol := + { cells + | .ofNat n => l[n]? + | _ => none } section Move -/-- -Move the head left by shifting the left StackTape under the head. --/ -def move_left (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 := - ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩ +@[simp, local grind =] +def optionMoveToInt : Option Dir → ℤ + | none => 0 + | some .left => -1 + | some .right => 1 -/-- -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 +@[simp, local grind =] +def moveInt (t : BiTape Symbol) (δ : ℤ) : BiTape Symbol := ⟨ fun i => t.cells (i - δ) ⟩ /-- Optionally perform a `move`, or do nothing if `none`. -/ -def optionMove : BiTape Symbol → Option Dir → BiTape Symbol - | t, none => t - | 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] - -@[simp] -lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by - simp [move_left, move_right] +@[simp, local grind =] +def optionMove (t : BiTape Symbol) (dir : Option Dir) : BiTape Symbol := + t.moveInt (optionMoveToInt dir) end Move /-- Write a value under the head of the `BiTape`. -/ -def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } +@[local grind =] +def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := + ⟨ Function.update t.cells 0 a ⟩ + +@[local grind =] +def read (t : BiTape Symbol) : Option Symbol := t.cells 0 + +@[simp] +lemma write_read (t : BiTape Symbol) : t.write t.read = t := by simp [write, read] /-- -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`. +The cells of `t` are non-blank only at indices in `s`. -/ -@[scoped grind] -def space_used (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 space_used_mk₁ (l : List Symbol) : - (mk₁ l).space_used = 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 - -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] +def supportSubset (t : BiTape Symbol) (s : Finset ℤ) : Prop := + ∀ i, t.cells i ≠ none → i ∈ s + +lemma supportSubset_mk₁ (l : List Symbol) : + supportSubset (mk₁ l) ((Finset.range l.length).image (Int.ofNat ·)) := by + intro i hi + simp only [mk₁] at hi + match i with + | .ofNat n => grind + | .negSucc n => grind + +lemma supportSubset_write_insert (t : BiTape Symbol) (a : Option Symbol) (s : Finset ℤ) + (hs : supportSubset t s) : supportSubset (t.write a) (insert 0 s) := by + intro i hi + simp only [write] at hi + by_cases h : i = 0 + · simp [h] + · rw [Function.update_of_ne h] at hi + exact Finset.mem_insert_of_mem (hs i hi) + +lemma supportSubset_moveInt (t : BiTape Symbol) (δ : ℤ) (s : Finset ℤ) + (hs : supportSubset t s) : + supportSubset (t.moveInt δ) (s.image (· + δ)) := by + intro i hi + simp only [moveInt] at hi + exact Finset.mem_image.mpr ⟨i - δ, hs _ hi, by ring⟩ + +lemma supportSubset_optionMove (t : BiTape Symbol) (d : Option Dir) (s : Finset ℤ) + (hs : supportSubset t s) : + supportSubset (t.optionMove d) (s.image (· + optionMoveToInt d)) := + supportSubset_moveInt _ _ _ hs end BiTape