class Cslib.Logic.InferenceSystem (α : Type u) : Type (max u v)

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

• derivation (s : α) : Sort v

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

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

⇓a is a derivation of a, that is, a witness that a is derivable. 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 {α : Type u_1} [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : derivation Γ) : derivation Δ

Rewrites the conclusion of a proof into an equal one.

Equations

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

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

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

Equations

• Cslib.Logic.InferenceSystem.Derivable a = Nonempty (Cslib.Logic.InferenceSystem.derivation a)

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

Shows derivability from a derivation.

@[implicit_reducible]

instance Cslib.Logic.InferenceSystem.instCoeDerivationDerivable {α : Type u_1} [InferenceSystem α] {a : α} : Coe (derivation a) (Derivable a)

Equations

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

noncomputable def Cslib.Logic.InferenceSystem.Derivable.toDerivation {α : Type u_1} [InferenceSystem α] {a : α} (d : Derivable a) : derivation 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.instCoeDerivableDerivation {α : Type u_1} [InferenceSystem α] {a : α} : Coe (Derivable a) (derivation a)

Equations

• Cslib.Logic.InferenceSystem.instCoeDerivableDerivation = { coe := Cslib.Logic.InferenceSystem.Derivable.toDerivation }