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.

@[implicit_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

@[implicit_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.