Local
Difficulty: optional — 9 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.
Rules that are schematic in the premises at hand, and the deductions that use only them.
A rule fixes the premises it draws on. Most rules of interest do not care what those premises are: they say what further assumptions each branch may use, and leave everything already available untouched. Such a rule is really a schema, standing for one rule for each list of premises it might be read against.
DeductionsFrom using schemata alone need no pasting: everything a branch draws on is already there. The next module shows that pasting is then never needed at all.
Source: Hiep, New Foundations for Separation Logic (PhD thesis, 2024), appendix A.3, on simple and complex proof rules and on rule schemata.
Logic.ProofTheory.Schema
A rule schema: every entry says what further assumptions that branch may use and what it must establish, and the schema then concludes. Read against a list of premises, every entry keeps those premises and adds its own. An entry adding nothing is a simple branch, and a schema with no entries is an axiom.
structure Logic.ProofTheory.Schema (Obj : Type) : Type
What each branch must establish, and the assumptions it may discharge.
premises : List (List Obj × Obj)
What the schema yields.
conclusion : Obj
Show details
Outer dependencies: (none)
Used by: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf, Logic.ProofTheory.CutFree.mono, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.DerivableCutFree.graft, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf.forall_toCutFree, Logic.ProofTheory.Instances, Logic.ProofTheory.Schema.IsAxiom, Logic.ProofTheory.Schema.IsComplexRule, Logic.ProofTheory.Schema.IsSimpleRule, Logic.ProofTheory.Schema.IsSimpleRule.of_isAxiom, Logic.ProofTheory.Schema.instance, Logic.ProofTheory.Schema.system, Logic.ProofTheory.derivable_iff_derivableCutFree, Logic.PropositionalLogic.HilbertSchema, Logic.PropositionalLogic.HilbertSchema.isAxiom_of_ne_mp, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom
Logic.ProofTheory.Schema.instance
Reading a schema against a given list of premises.
def Logic.ProofTheory.Schema.instance {Obj : Type} (s : Logic.ProofTheory.Schema Obj) (Γ : List Obj) : Logic.ProofTheory.Application Obj
Show details
| s.instance Γ = { premises := List.map (fun p => (⟪p.1, Γ⟫, p.2)) s.premises, conclusion := (Γ, s.conclusion) }
Complexity: 139 (size of the value term)
Outer dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.Schema
Inner dependencies: instToSeqList
Logic.ProofTheory.Instances
The applications that a collection of schemata allows: every schema, read against every list of premises.
def Logic.ProofTheory.Instances {Obj : Type} (S : Logic.ProofTheory.Schema Obj → Prop) : Logic.ProofTheory.Application Obj → Prop
Show details
| Logic.ProofTheory.Instances S r = ∃ s Γ, S s ∧ r = s.instance Γ
Complexity: 53 (size of the value term)
Outer dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.Schema
Inner dependencies: Logic.ProofTheory.Schema.instance
Used by: Logic.ProofTheory.Schema.system
Logic.ProofTheory.Schema.system
The proof system a collection of schemata determines.
def Logic.ProofTheory.Schema.system {Obj : Type} (S : Logic.ProofTheory.Schema Obj → Prop) : Logic.ProofTheory.ProofSystem Obj
Show details
| Logic.ProofTheory.Schema.system S = { rules := Logic.ProofTheory.Instances S }
Complexity: 17 (size of the value term)
Outer dependencies: Logic.ProofTheory.ProofSystem, Logic.ProofTheory.Schema
Inner dependencies: Logic.ProofTheory.Instances
Logic.ProofTheory.CutFree
A cut-free deduction: one that appeals to premises and applies schemata, and never pastes.
inductive Logic.ProofTheory.CutFree {Obj : Type} (S : Logic.ProofTheory.Schema Obj → Prop) : List Obj → Obj → Type
A premise stands as a deduction of itself.
assumption : {P : List Obj} → {a : Obj} → a ∈ P → Logic.ProofTheory.CutFree S P a
A schema applies once each of its branches has been established.
apply : {P : List Obj} → (s : Logic.ProofTheory.Schema Obj) → S s → Logic.ProofTheory.CutFree.DerivationsOf S P s.premises → Logic.ProofTheory.CutFree S P s.conclusion
Show details
Outer dependencies: Logic.ProofTheory.Schema
Inner dependencies: Logic.ProofTheory.CutFree.DerivationsOf, instToSeqList
Lean core dependencies: Eq, Eq.symm, HEq, List, Nat, Nat.ble, PProd, PULift, PUnit, Prod, SizeOf, cond, eq_of_heq
Used by: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf, Logic.ProofTheory.CutFree.mono, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.DerivableCutFree.graft, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.derivable_iff_derivableCutFree
Logic.ProofTheory.CutFree.DerivationsOf
A cut-free deduction for each branch of a schema, each reading the premises at hand together with the assumptions that branch discharges.
inductive Logic.ProofTheory.CutFree.DerivationsOf {Obj : Type} (S : Logic.ProofTheory.Schema Obj → Prop) : List Obj → List (List Obj × Obj) → Type
No branches left.
nil : {P : List Obj} → Logic.ProofTheory.CutFree.DerivationsOf S P []
One branch established, and the rest.
cons : {P Δ : List Obj} → {a : Obj} → {rest : List (List Obj × Obj)} → Logic.ProofTheory.CutFree S ⟪Δ, P⟫ a → Logic.ProofTheory.CutFree.DerivationsOf S P rest → Logic.ProofTheory.CutFree.DerivationsOf S P ((Δ, a) :: rest)
Show details
Outer dependencies: Logic.ProofTheory.Schema
Inner dependencies: Logic.ProofTheory.CutFree, instToSeqList
Lean core dependencies: Eq, Eq.symm, HEq, List, Nat, Nat.ble, PProd, PULift, PUnit, Prod, SizeOf, cond, eq_of_heq
Used by: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf, Logic.ProofTheory.CutFree.mono, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.DerivableCutFree.graft, Logic.ProofTheory.Derivation.toCutFree
Logic.ProofTheory.DerivableCutFree
A conclusion is cut-free deducible when some cut-free deduction of it exists.
def Logic.ProofTheory.DerivableCutFree {Obj : Type} (S : Logic.ProofTheory.Schema Obj → Prop) (P : List Obj) (a : Obj) : Prop
Show details
| Logic.ProofTheory.DerivableCutFree S P a = Nonempty (Logic.ProofTheory.CutFree S P a)
Complexity: 25 (size of the value term)
Outer dependencies: Logic.ProofTheory.Schema
Inner dependencies: Logic.ProofTheory.CutFree
Logic.ProofTheory.CutFree.toDerivation
A cut-free deduction is a deduction.
def Logic.ProofTheory.CutFree.toDerivation {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop} {P : List Obj} {a : Obj} : Logic.ProofTheory.CutFree S P a → Logic.ProofTheory.Derivation (Logic.ProofTheory.Schema.system S) P a
Show details
| (Logic.ProofTheory.CutFree.assumption h).toDerivation = Logic.ProofTheory.Derivation.assumption h | (Logic.ProofTheory.CutFree.apply s hs es).toDerivation = Logic.ProofTheory.Derivation.apply (s.instance x✝) ⋯ es.toDerivationsOf
Complexity: 217 (size of the value term)
Outer dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.Derivation, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.system
Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf
The same, branch by branch.
def Logic.ProofTheory.CutFree.DerivationsOf.toDerivationsOf {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop} {P : List Obj} {ps : List (List Obj × Obj)} : Logic.ProofTheory.CutFree.DerivationsOf S P ps → Logic.ProofTheory.DerivationsOf (Logic.ProofTheory.Schema.system S) (List.map (fun p => (⟪p.1, P⟫, p.2)) ps)
Show details
| Logic.ProofTheory.CutFree.DerivationsOf.nil.toDerivationsOf = Logic.ProofTheory.DerivationsOf.nil | (Logic.ProofTheory.CutFree.DerivationsOf.cons d es).toDerivationsOf = Logic.ProofTheory.DerivationsOf.cons d.toDerivation es.toDerivationsOf
Complexity: 225 (size of the value term)
Outer dependencies: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.system, instToSeqList
Inner dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.Derivation
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.