Inference systems

This module defines the basic classes and notation for inference systems -- systems for deriving conclusions from premises.

We intend inference systems broadly, as in theory of programming languages. In applications to logic, for example, we use inference systems to capture both the concepts of satisfiability and proof systems.

class Cslib.Logic.InferenceSystem (S : Type u_1) (α : Type u_2) : Type (max u_2 v)

The notation typeclass for inference systems. This enables the notation S⇓a, where S is a tag for the inference system and a : α is a derivable value.

• derivation (a : α) : Sort v

  S⇓a is a derivation of a, that is, a witness that a is derivable in the system S. The meaning of this notation is type-dependent.

opaque Cslib.Logic.InferenceSystem.Default : Type

Default tag for inference system instances. ⇓a is short for Default⇓a.

@[reducible, inline]

abbrev Cslib.Logic.HasInferenceSystem (α : Type u_1) : Type (max u_1 u_2)

Class for types (α) that have a canonical inference system.

Equations

• Cslib.Logic.HasInferenceSystem = Cslib.Logic.InferenceSystem Cslib.Logic.InferenceSystem.Default

def Cslib.Logic.InferenceSystem.«term_⇓_» : Lean.TrailingParserDescr

S⇓a is a derivation of a, that is, a witness that a is derivable in the system S. The meaning of this notation is type-dependent.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.InferenceSystem.rwConclusion {S : Type u_1} {α : Type u_2} [InferenceSystem S α] {Γ Δ : α} (h : Γ = Δ) (p : derivation S Γ) : derivation S Δ

Rewrites the conclusion of a proof into an equal one.

Equations

• Cslib.Logic.InferenceSystem.rwConclusion h p = h ▸ p

def Cslib.Logic.InferenceSystem.DerivableIn {α : Type u_1} (S : Type u_2) [InferenceSystem S α] (a : α) : Prop

a is derivable in S if it is the conclusion of some derivation.

Equations

• Cslib.Logic.InferenceSystem.DerivableIn S a = Nonempty (Cslib.Logic.InferenceSystem.derivation S a)

@[reducible, inline]

abbrev Cslib.Logic.InferenceSystem.Derivable {α : Type u_1} [InferenceSystem Default α] (a : α) : Prop

a : α is derivable in the default inference system for α.

Equations

• Cslib.Logic.InferenceSystem.Derivable = Cslib.Logic.InferenceSystem.DerivableIn Cslib.Logic.InferenceSystem.Default

theorem Cslib.Logic.InferenceSystem.DerivableIn.fromDerivation {S : Type u_1} {α : Type u_2} [InferenceSystem S α] {a : α} (d : derivation S a) : DerivableIn S a

Shows derivability from a derivation.

@[instance_reducible]

instance Cslib.Logic.InferenceSystem.instCoeDerivationDerivableIn {S : Type u_1} {α : Type u_2} [InferenceSystem S α] {a : α} : Coe (derivation S a) (DerivableIn S a)

Equations

• Cslib.Logic.InferenceSystem.instCoeDerivationDerivableIn = { coe := ⋯ }

noncomputable def Cslib.Logic.InferenceSystem.DerivableIn.toDerivation {S : Type u_1} {α : Type u_2} [InferenceSystem S α] {a : α} (d : DerivableIn S a) : derivation S a

Extracts (noncomputably) a derivation from the fact that a conclusion is derivable.

Equations

• d.toDerivation = Classical.choice d

@[instance_reducible]

noncomputable instance Cslib.Logic.InferenceSystem.instCoeDerivableInDerivation {S : Type u_1} {α : Type u_2} [InferenceSystem S α] {a : α} : Coe (DerivableIn S a) (derivation S a)

Equations

• Cslib.Logic.InferenceSystem.instCoeDerivableInDerivation = { coe := Cslib.Logic.InferenceSystem.DerivableIn.toDerivation }

def Cslib.Logic.InferenceSystem.«term⇓_» : Lean.ParserDescr

S⇓a is a derivation of a, that is, a witness that a is derivable in the system S. The meaning of this notation is type-dependent.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.InferenceSystem.delabInferenceSystem : Lean.PrettyPrinter.Delaborator.Delab

Delaborator that hides InferenceSystem.Default in uses of the ⇓a notation.

Equations

• One or more equations did not get rendered due to their size.