Documentation

ISAR.Kernel

inductive ISAR.SK :

S : SK
K : SK
I : SK
app : SK → SK → SK

Instances For

@[implicit_reducible]

instance ISAR.instDecidableEqSK :

Equations

ISAR.instDecidableEqSK = ISAR.instDecidableEqSK.decEq

def ISAR.instDecidableEqSK.decEq (x✝ x✝¹ : SK) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
ISAR.instDecidableEqSK.decEq ISAR.SK.S ISAR.SK.S = isTrue ⋯
ISAR.instDecidableEqSK.decEq ISAR.SK.S ISAR.SK.K = isFalse ISAR.instDecidableEqSK.decEq._proof_1
ISAR.instDecidableEqSK.decEq ISAR.SK.S ISAR.SK.I = isFalse ISAR.instDecidableEqSK.decEq._proof_2
ISAR.instDecidableEqSK.decEq ISAR.SK.S (a · a_1) = isFalse ⋯
ISAR.instDecidableEqSK.decEq ISAR.SK.K ISAR.SK.S = isFalse ISAR.instDecidableEqSK.decEq._proof_4
ISAR.instDecidableEqSK.decEq ISAR.SK.K ISAR.SK.K = isTrue ⋯
ISAR.instDecidableEqSK.decEq ISAR.SK.K ISAR.SK.I = isFalse ISAR.instDecidableEqSK.decEq._proof_5
ISAR.instDecidableEqSK.decEq ISAR.SK.K (a · a_1) = isFalse ⋯
ISAR.instDecidableEqSK.decEq ISAR.SK.I ISAR.SK.S = isFalse ISAR.instDecidableEqSK.decEq._proof_7
ISAR.instDecidableEqSK.decEq ISAR.SK.I ISAR.SK.K = isFalse ISAR.instDecidableEqSK.decEq._proof_8
ISAR.instDecidableEqSK.decEq ISAR.SK.I ISAR.SK.I = isTrue ⋯
ISAR.instDecidableEqSK.decEq ISAR.SK.I (a · a_1) = isFalse ⋯
ISAR.instDecidableEqSK.decEq (a · a_1) ISAR.SK.S = isFalse ⋯
ISAR.instDecidableEqSK.decEq (a · a_1) ISAR.SK.K = isFalse ⋯
ISAR.instDecidableEqSK.decEq (a · a_1) ISAR.SK.I = isFalse ⋯

Instances For

def ISAR.instReprSK.repr :

SK → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
ISAR.instReprSK.repr ISAR.SK.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.SK.S")).group prec✝
ISAR.instReprSK.repr ISAR.SK.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.SK.K")).group prec✝
ISAR.instReprSK.repr ISAR.SK.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.SK.I")).group prec✝

Instances For

@[implicit_reducible]

instance ISAR.instReprSK :

Equations

ISAR.instReprSK = { reprPrec := ISAR.instReprSK.repr }

def ISAR.SK.«term_·_» :

Lean.TrailingParserDescr

Equations

ISAR.SK.«term_·_» = Lean.ParserDescr.trailingNode `ISAR.SK.«term_·_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " · ") (Lean.ParserDescr.cat `term 71))

Instances For

inductive ISAR.ITerm :

var : Nat → ITerm
norm : ITerm
konst : ITerm
dup : ITerm
swap : ITerm
comp : ITerm
sₛ : ITerm
app : ITerm → ITerm → ITerm

Instances For

def ISAR.instDecidableEqITerm.decEq (x✝ x✝¹ : ITerm) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[implicit_reducible]

instance ISAR.instDecidableEqITerm :

DecidableEq ITerm

Equations

ISAR.instDecidableEqITerm = ISAR.instDecidableEqITerm.decEq

@[implicit_reducible]

instance ISAR.instReprITerm :

Equations

ISAR.instReprITerm = { reprPrec := ISAR.instReprITerm.repr }

def ISAR.instReprITerm.repr :

ITerm → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
ISAR.instReprITerm.repr ISAR.ITerm.norm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.norm")).group prec✝
ISAR.instReprITerm.repr ISAR.ITerm.konst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.konst")).group prec✝
ISAR.instReprITerm.repr ISAR.ITerm.dup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.dup")).group prec✝
ISAR.instReprITerm.repr ISAR.ITerm.swap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.swap")).group prec✝
ISAR.instReprITerm.repr ISAR.ITerm.comp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.comp")).group prec✝
ISAR.instReprITerm.repr ISAR.ITerm.sₛ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.ITerm.sₛ")).group prec✝

Instances For

def ISAR.ITerm.«term_·_» :

Lean.TrailingParserDescr

Equations

ISAR.ITerm.«term_·_» = Lean.ParserDescr.trailingNode `ISAR.ITerm.«term_·_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " · ") (Lean.ParserDescr.cat `term 71))

Instances For

inductive ISAR.SKStep :

SK → SK → Prop

Iβ (x : SK) : SKStep (SK.I · x) x
Kβ (x y : SK) : SKStep (SK.K · x · y) x
Sβ (x y z : SK) : SKStep (SK.S · x · y · z) (x · z · (y · z))
appL {f f' x : SK} : SKStep f f' → SKStep (f · x) (f' · x)
appR {f x x' : SK} : SKStep x x' → SKStep (f · x) (f · x')

Instances For

inductive ISAR.IStep :

ITerm → ITerm → Prop

normβ (x : ITerm) : IStep (ITerm.norm · x) x
konstβ (x y : ITerm) : IStep (ITerm.konst · x · y) x
compβ (f g x : ITerm) : IStep (ITerm.comp · f · g · x) (f · (g · x))
sβ (x y z : ITerm) : IStep (ITerm.sₛ · x · y · z) (x · z · (y · z))
appL {f f' x : ITerm} : IStep f f' → IStep (f · x) (f' · x)
appR {f x x' : ITerm} : IStep x x' → IStep (f · x) (f · x')

Instances For

@[reducible, inline]

abbrev ISAR.SKRed (a : SK) :

Equations

ISAR.SKRed = Relation.ReflTransGen ISAR.SKStep

Instances For

@[reducible, inline]

abbrev ISAR.IRed (a : ITerm) :

Equations

ISAR.IRed = Relation.ReflTransGen ISAR.IStep

Instances For

def ISAR.NormalSK (t : SK) :

Equations

ISAR.NormalSK t = ∀ (u : ISAR.SK), ¬ISAR.SKStep t u

Instances For

def ISAR.NormalI (t : ITerm) :

Equations

ISAR.NormalI t = ∀ (u : ISAR.ITerm), ¬ISAR.IStep t u

Instances For

def ISAR.encode :

Equations

ISAR.encode ISAR.SK.S = ISAR.ITerm.sₛ
ISAR.encode ISAR.SK.K = ISAR.ITerm.konst
ISAR.encode ISAR.SK.I = ISAR.ITerm.norm
ISAR.encode (a · a_1) = ISAR.encode a · ISAR.encode a_1

Instances For

theorem ISAR.encode_I (x : ITerm) :

IRed (encode SK.I · x) x

theorem ISAR.encode_K (x y : ITerm) :

IRed (encode SK.K · x · y) x

theorem ISAR.encode_S (x y z : ITerm) :

IRed (encode SK.S · x · y · z) (x · z · (y · z))

theorem ISAR.IRed_app_left {f f' x : ITerm} :

IRed f f' → IRed (f · x) (f' · x)

theorem ISAR.IRed_app_right {f x x' : ITerm} :

IRed x x' → IRed (f · x) (f · x')

theorem ISAR.IRed_app {f f' x x' : ITerm} (hf : IRed f f') (hx : IRed x x') :

IRed (f · x) (f' · x')

theorem ISAR.simulate_step {t u : SK} :

SKStep t u → IRed (encode t) (encode u)

theorem ISAR.simulate_red {t u : SK} :

SKRed t u → IRed (encode t) (encode u)

inductive ISAR.ISKTerm :

Identifies ISAR terms that belong to the pure SKI fragment.

norm : ISKTerm ITerm.norm
konst : ISKTerm ITerm.konst
sₛ : ISKTerm ITerm.sₛ
app {f x : ITerm} : ISKTerm f → ISKTerm x → ISKTerm (f · x)

Instances For

theorem ISAR.encode_is_ISKTerm (t : SK) :

ISKTerm (encode t)

Any term produced by encode belongs to the ISK fragment.

inductive ISAR.ParStep :

ITerm → ITerm → Prop

var (n : Nat) : ParStep (ITerm.var n) (ITerm.var n)
norm : ParStep ITerm.norm ITerm.norm
konst : ParStep ITerm.konst ITerm.konst
dup : ParStep ITerm.dup ITerm.dup
swap : ParStep ITerm.swap ITerm.swap
comp : ParStep ITerm.comp ITerm.comp
sₛ : ParStep ITerm.sₛ ITerm.sₛ
app {f f' x x' : ITerm} : ParStep f f' → ParStep x x' → ParStep (f · x) (f' · x')
norm_red {x x' : ITerm} : ParStep x x' → ParStep (ITerm.norm · x) x'
konst_red {x x' y y' : ITerm} : ParStep x x' → ParStep y y' → ParStep (ITerm.konst · x · y) x'
comp_red {f f' g g' x x' : ITerm} : ParStep f f' → ParStep g g' → ParStep x x' → ParStep (ITerm.comp · f · g · x) (f' · (g' · x'))
s_red {x x' y y' z z' : ITerm} : ParStep x x' → ParStep y y' → ParStep z z' → ParStep (ITerm.sₛ · x · y · z) (x' · z' · (y' · z'))

Instances For

ITerm → ITerm

Equations

ISAR.cd (ISAR.ITerm.var n) = ISAR.ITerm.var n
ISAR.cd ISAR.ITerm.norm = ISAR.ITerm.norm
ISAR.cd ISAR.ITerm.konst = ISAR.ITerm.konst
ISAR.cd ISAR.ITerm.dup = ISAR.ITerm.dup
ISAR.cd ISAR.ITerm.swap = ISAR.ITerm.swap
ISAR.cd ISAR.ITerm.comp = ISAR.ITerm.comp
ISAR.cd ISAR.ITerm.sₛ = ISAR.ITerm.sₛ
ISAR.cd (ISAR.ITerm.norm · x_1) = ISAR.cd x_1
ISAR.cd (ISAR.ITerm.konst · x_1 · a) = ISAR.cd x_1
ISAR.cd (ISAR.ITerm.comp · f · g · x_1) = ISAR.cd f · (ISAR.cd g · ISAR.cd x_1)
ISAR.cd (ISAR.ITerm.sₛ · x_1 · y · z) = ISAR.cd x_1 · ISAR.cd z · (ISAR.cd y · ISAR.cd z)
ISAR.cd (f · x_1) = ISAR.cd f · ISAR.cd x_1

Instances For

theorem ISAR.ParStep.refl (t : ITerm) :

theorem ISAR.ParStep_cd (t : ITerm) {u : ITerm} :

ParStep t u → ParStep u (cd t)

theorem ISAR.ParStep_diamond {t u₁ u₂ : ITerm} (h₁ : ParStep t u₁) (h₂ : ParStep t u₂) :

∃ (v : ITerm ), ParStep u₁ v ∧ ParStep u₂ v

theorem ISAR.IStep_to_ParStep {t u : ITerm} (h : IStep t u) :

theorem ISAR.ParStep_to_IRed {t u : ITerm} (h : ParStep t u) :

IRed t u

theorem ISAR.ParStep_commute_ParTransGen {t u₁ u₂ : ITerm} (h₁ : ParStep t u₁) (h₂ : Relation.ReflTransGen ParStep t u₂) :

∃ (v : ITerm ), Relation.ReflTransGen ParStep u₁ v ∧ ParStep u₂ v

theorem ISAR.ParTransGen_diamond {t u₁ u₂ : ITerm} (h₁ : Relation.ReflTransGen ParStep t u₁) (h₂ : Relation.ReflTransGen ParStep t u₂) :

∃ (v : ITerm ), Relation.ReflTransGen ParStep u₁ v ∧ Relation.ReflTransGen ParStep u₂ v

theorem ISAR.IRed_to_ParTransGen {t u : ITerm} (h : IRed t u) :

Relation.ReflTransGen ParStep t u

theorem ISAR.ParTransGen_to_IRed {t u : ITerm} (h : Relation.ReflTransGen ParStep t u) :

IRed t u

theorem ISAR.IRed_confluence {t u₁ u₂ : ITerm} (h₁ : IRed t u₁) (h₂ : IRed t u₂) :

∃ (v : ITerm ), IRed u₁ v ∧ IRed u₂ v

theorem ISAR.ISKTerm_preserved {t u : ITerm} (ht : ISKTerm t) (h : IStep t u) :

theorem ISAR.ISKTerm_IRed_preserved {t u : ITerm} (ht : ISKTerm t) (h : IRed t u) :

theorem ISAR.isar_fragment_confluence {t u₁ u₂ : ITerm} (ht : ISKTerm t) (r₁ : IRed t u₁) (r₂ : IRed t u₂) :

∃ (v : ITerm ), IRed u₁ v ∧ IRed u₂ v ∧ ISKTerm v

The operational semantics restricted to the ISK fragment is confluent.

theorem ISAR.IRed_normal_eq {n v : ITerm} (hn : NormalI n) (h : IRed n v) :

n = v

theorem ISAR.isar_fragment_unique_normal_forms {t n₁ n₂ : ITerm} (ht : ISKTerm t) (r₁ : IRed t n₁) (hn₁ : NormalI n₁) (r₂ : IRed t n₂) (hn₂ : NormalI n₂) :

n₁ = n₂

An encoded term in the ISK fragment has at most one normal form.

def ISAR.derived_s :

Equations

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

Instances For

inductive ISAR.IStepBasis :

ITerm → ITerm → Prop

normβ (x : ITerm) : IStepBasis (ITerm.norm · x) x
konstβ (x y : ITerm) : IStepBasis (ITerm.konst · x · y) x
compβ (f g x : ITerm) : IStepBasis (ITerm.comp · f · g · x) (f · (g · x))
dupβ (f x : ITerm) : IStepBasis (ITerm.dup · f · x) (f · x · x)
swapβ (f x y : ITerm) : IStepBasis (ITerm.swap · f · x · y) (f · y · x)
appL {f f' x : ITerm} : IStepBasis f f' → IStepBasis (f · x) (f' · x)
appR {f x x' : ITerm} : IStepBasis x x' → IStepBasis (f · x) (f · x')

Instances For

@[reducible, inline]

abbrev ISAR.IRedBasis (a : ITerm) :

Equations

ISAR.IRedBasis = Relation.ReflTransGen ISAR.IStepBasis

Instances For

theorem ISAR.IRedBasis_app_left {f f' x : ITerm} :

IRedBasis f f' → IRedBasis (f · x) (f' · x)

theorem ISAR.IRedBasis_app_right {f x x' : ITerm} :

IRedBasis x x' → IRedBasis (f · x) (f · x')

theorem ISAR.IRedBasis_app {f f' x x' : ITerm} (hf : IRedBasis f f') (hx : IRedBasis x x') :

IRedBasis (f · x) (f' · x')

theorem ISAR.derived_s_beta (x y z : ITerm) :

IRedBasis (derived_s · x · y · z) (x · z · (y · z))

theorem ISAR.translate_preserves_step {t u : ITerm} (h : IStep t u) :

IRedBasis (translate_to_basis t) (translate_to_basis u)

inductive ISAR.NoS :

var (n : Nat) : NoS (ITerm.var n)
norm : NoS ITerm.norm
konst : NoS ITerm.konst
dup : NoS ITerm.dup
swap : NoS ITerm.swap
comp : NoS ITerm.comp
app {f x : ITerm} : NoS f → NoS x → NoS (f · x)

Instances For

theorem ISAR.derived_s_NoS :

theorem ISAR.translate_NoS (t : ITerm) :

NoS (translate_to_basis t)

theorem ISAR.IStepBasis_preserves_NoS {t u : ITerm} (h : IStepBasis t u) (ht : NoS t) :

theorem ISAR.IRedBasis_preserves_NoS {t u : ITerm} (h : IRedBasis t u) (ht : NoS t) :