Documentation

Mathling.Lambek.ProductFree.Decidable

def Mathling.Lambek.ProductFree.splits {α : Type u_1} :

List α → List (List α × List α)

Equations

One or more equations did not get rendered due to their size.
Mathling.Lambek.ProductFree.splits [] = [([], [])]

Instances For

theorem Mathling.Lambek.ProductFree.splits_list_degree {α✝ : Type u_1} {Γ : List α✝} {X : List α✝ × List α✝} (h : X ∈ splits Γ) :

X.fst ++ X.snd = Γ

def Mathling.Lambek.ProductFree.picks {α : Type u_1} :

List α → List (List α × α × List α)

Equations

One or more equations did not get rendered due to their size.
Mathling.Lambek.ProductFree.picks [] = []

Instances For

theorem Mathling.Lambek.ProductFree.picks_list_degree {α✝ : Type u_1} {Γ : List α✝} {X : List α✝ × α✝ × List α✝} (h : X ∈ picks Γ) :

X.fst ++ [X.snd.fst] ++ X.snd.snd = Γ

theorem Mathling.Lambek.ProductFree.splits_mem {α : Type u_1} (Γ Δ : List α) :

(Γ, Δ) ∈ splits (Γ ++ Δ)

theorem Mathling.Lambek.ProductFree.picks_mem {α : Type u_1} (Γ Δ : List α) (a : α) :

(Γ, a, Δ) ∈ picks (Γ ++ [a] ++ Δ)

inductive Mathling.Lambek.ProductFree.Cand :

rdiv (L : List Tp) (B A : Tp) (Δ Λ : List Tp) : Cand
ldiv (Γ Δ : List Tp) (A B : Tp) (Λ : List Tp) : Cand

Instances For

def Mathling.Lambek.ProductFree.candidates (Γ : List Tp) :

Equations

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

Instances For

theorem Mathling.Lambek.ProductFree.candidates_list_degree {Γ : List Tp} {c : Cand} (h : c ∈ candidates Γ) :

match c, h with | Cand.rdiv L B A Δ Λ, h => L ++ [B ⧸ A] ++ Δ ++ Λ = Γ | Cand.ldiv Γ₁ Δ A B R, h => Γ₁ ++ Δ ++ [A ⧹ B] ++ R = Γ

theorem Mathling.Lambek.ProductFree.candidates_rdiv_mem (Γ Δ Λ : List Tp) (A B : Tp) :

Cand.rdiv Γ B A Δ Λ ∈ candidates (Γ ++ [B ⧸ A] ++ Δ ++ Λ)

theorem Mathling.Lambek.ProductFree.candidates_ldiv_mem (Γ₁ Δ R : List Tp) (A B : Tp) :

Cand.ldiv Γ₁ Δ A B R ∈ candidates (Γ₁ ++ Δ ++ [A ⧹ B] ++ R)

@[irreducible]

def Mathling.Lambek.ProductFree.prove1 (Γ : List Tp) (A : Tp) :

Equations

One or more equations did not get rendered due to their size.
Mathling.Lambek.ProductFree.prove1 Γ (A' ⧹ B) = (decide (Γ ≠ []) && Mathling.Lambek.ProductFree.prove1 ([A'] ++ Γ) B)
Mathling.Lambek.ProductFree.prove1 Γ (B ⧸ A') = (decide (Γ ≠ []) && Mathling.Lambek.ProductFree.prove1 (Γ ++ [A']) B)

Instances For

def Mathling.Lambek.ProductFree.proveAux :

ℕ → List Tp → Tp → Bool

Equations

One or more equations did not get rendered due to their size.
Mathling.Lambek.ProductFree.proveAux 0 x✝¹ x✝ = false
Mathling.Lambek.ProductFree.proveAux n.succ x✝ (A' ⧹ B) = (decide (x✝ ≠ []) && Mathling.Lambek.ProductFree.proveAux n ([A'] ++ x✝) B)
Mathling.Lambek.ProductFree.proveAux n.succ x✝ (B ⧸ A') = (decide (x✝ ≠ []) && Mathling.Lambek.ProductFree.proveAux n (x✝ ++ [A']) B)

Instances For

def Mathling.Lambek.ProductFree.prove2 (Γ : List Tp) (A : Tp) :

Equations

Mathling.Lambek.ProductFree.prove2 Γ A = Mathling.Lambek.ProductFree.proveAux (Mathling.Lambek.ProductFree.list_degree Γ + Mathling.Lambek.ProductFree.tp_degree A + 1) Γ A

Instances For

theorem Mathling.Lambek.ProductFree.proveAux_mono {n : ℕ} {Γ : List Tp} {A : Tp} (h : proveAux n Γ A = true) :

proveAux (n + 1) Γ A = true

theorem Mathling.Lambek.ProductFree.proveAux_mono_le {Γ : List Tp} {A : Tp} {n m : ℕ} (h : n ≤ m) (hp : proveAux n Γ A = true) :

proveAux m Γ A = true

theorem Mathling.Lambek.ProductFree.proveAux_sound {n : ℕ} {Γ : List Tp} {A : Tp} (h : proveAux n Γ A = true) :

prove1 Γ A = true

theorem Mathling.Lambek.ProductFree.proveAux_complete {Γ : List Tp} {A : Tp} (h : prove1 Γ A = true) :

prove2 Γ A = true

theorem Mathling.Lambek.ProductFree.prove1_iff_prove2 {Γ : List Tp} {A : Tp} :

prove1 Γ A = true ↔ prove2 Γ A = true

theorem Mathling.Lambek.ProductFree.prove1_sound {Γ : List Tp} {A : Tp} (h : prove1 Γ A = true) :

Γ ⇒ A

theorem Mathling.Lambek.ProductFree.prove1_comple {Γ : List Tp} {A : Tp} (h : Γ ⇒ A) :

prove1 Γ A = true

theorem Mathling.Lambek.ProductFree.prove1_iff_sequent {Γ : List Tp} {A : Tp} :

prove1 Γ A = true ↔ Γ ⇒ A

theorem Mathling.Lambek.ProductFree.prove2_iff_sequent {Γ : List Tp} {A : Tp} :

prove2 Γ A = true ↔ Γ ⇒ A

instance Mathling.Lambek.ProductFree.instDecidableSequent {Γ : List Tp} {A : Tp} :

Decidable (Γ ⇒ A)

Equations

Mathling.Lambek.ProductFree.instDecidableSequent = decidable_of_iff (Mathling.Lambek.ProductFree.prove2 Γ A = true) ⋯