Marked types for the monotonicity calculus

This file defines the type system of the [IMT17] monotonicity calculus: simple types over a set of base types, with each arrow marked as monotone (+), antitone (−), or unmarked (·).

Main declarations

• Marking: the three markings — a commutative monoid under valence composition (+ the identity, · absorbing), and a join-semilattice with · on top.
• Ty: marked simple types, with the subtyping order — contravariant in domains, covariant in codomains and markings — decidable over a DecidableEq base.
• Ty.sup?: the partial join of compatible types.
• Ty.unmark: erasure of the markings along the codomain spine.

References

• [IMT17] — Definitions 3.1–3.3.

Markings

inductive NaturalLogic.Marking : Type

A monotonicity marking: pos (+, monotone), neg (−, antitone), or unmarked (·, no information) ([IMT17] Definition 3.1).

• pos : Marking
• neg : Marking
• unmarked : Marking

@[instance_reducible]

instance NaturalLogic.instDecidableEqMarking : DecidableEq Marking

Equations

• NaturalLogic.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NaturalLogic.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• NaturalLogic.instReprMarking.repr NaturalLogic.Marking.pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NaturalLogic.Marking.pos")).group prec✝
• NaturalLogic.instReprMarking.repr NaturalLogic.Marking.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NaturalLogic.Marking.neg")).group prec✝

@[instance_reducible]

instance NaturalLogic.instReprMarking : Repr Marking

Equations

• NaturalLogic.instReprMarking = { reprPrec := NaturalLogic.instReprMarking.repr }

def NaturalLogic.Marking.comp : Marking → Marking → Marking

Valence composition: signs multiply, · absorbs.

Equations

• NaturalLogic.Marking.pos.comp x✝ = x✝
• x✝.comp NaturalLogic.Marking.pos = x✝
• NaturalLogic.Marking.neg.comp NaturalLogic.Marking.neg = NaturalLogic.Marking.pos
• x✝¹.comp x✝ = NaturalLogic.Marking.unmarked

@[instance_reducible]

instance NaturalLogic.Marking.instMul : Mul Marking

Equations

• NaturalLogic.Marking.instMul = { mul := NaturalLogic.Marking.comp }

@[instance_reducible]

instance NaturalLogic.Marking.instOne : One Marking

Equations

• NaturalLogic.Marking.instOne = { one := NaturalLogic.Marking.pos }

@[instance_reducible]

instance NaturalLogic.Marking.instCommMonoid : CommMonoid Marking

Equations

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

def NaturalLogic.Marking.le : Marking → Marking → Prop

The information order: + ⊑ · and − ⊑ ·.

Equations

• x✝.le NaturalLogic.Marking.unmarked = True
• NaturalLogic.Marking.pos.le NaturalLogic.Marking.pos = True
• NaturalLogic.Marking.neg.le NaturalLogic.Marking.neg = True
• x✝¹.le x✝ = False

@[instance_reducible]

instance NaturalLogic.Marking.instDecidableRelLe : DecidableRel le

Equations

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

@[instance_reducible]

instance NaturalLogic.Marking.instLE : LE Marking

Equations

• NaturalLogic.Marking.instLE = { le := NaturalLogic.Marking.le }

@[instance_reducible]

instance NaturalLogic.Marking.decidableLE (a b : Marking) : Decidable (a ≤ b)

Equations

• a.decidableLE b = a.instDecidableRelLe b

@[instance_reducible]

instance NaturalLogic.Marking.instSemilatticeSup : SemilatticeSup Marking

Equations

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

@[instance_reducible]

instance NaturalLogic.Marking.instOrderTop : OrderTop Marking

Equations

• NaturalLogic.Marking.instOrderTop = { top := NaturalLogic.Marking.unmarked, le_top := NaturalLogic.Marking.instOrderTop._proof_1 }

Marked types

inductive NaturalLogic.Ty (B : Type u_1) : Type u_1

Simple types over base types B, with marked arrows ([IMT17] Definition 3.1): arr σ m τ is the type of m-behaved functions from σ to τ.

• base {B : Type u_1} : B → Ty B
• arr {B : Type u_1} : Ty B → Marking → Ty B → Ty B

def NaturalLogic.instDecidableEqTy.decEq {B✝ : Type u_1} [DecidableEq B✝] (x✝ x✝¹ : Ty B✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• NaturalLogic.instDecidableEqTy.decEq (NaturalLogic.Ty.base a) (NaturalLogic.Ty.base b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• NaturalLogic.instDecidableEqTy.decEq (NaturalLogic.Ty.base a) (a_1.arr a_2 a_3) = isFalse ⋯
• NaturalLogic.instDecidableEqTy.decEq (a.arr a_1 a_2) (NaturalLogic.Ty.base a_3) = isFalse ⋯

@[instance_reducible]

instance NaturalLogic.instDecidableEqTy {B✝ : Type u_1} [DecidableEq B✝] : DecidableEq (Ty B✝)

Equations

• NaturalLogic.instDecidableEqTy = NaturalLogic.instDecidableEqTy.decEq

inductive NaturalLogic.Ty.LE {B : Type u_1} : Ty B → Ty B → Prop

The subtyping order ([IMT17] Definition 3.2): contravariant in domains, covariant in codomains and markings, so that every +- or −-typed function can also be considered ·-typed.

• base {B : Type u_1} (b : B) : (Ty.base b).LE (Ty.base b)
• arr {B : Type u_1} {σ σ' τ τ' : Ty B} {m m' : Marking} : σ'.LE σ → τ.LE τ' → m ≤ m' → (σ.arr m τ).LE (σ'.arr m' τ')

@[instance_reducible]

instance NaturalLogic.Ty.instLE {B : Type u_1} : LE (Ty B)

Equations

• NaturalLogic.Ty.instLE = { le := NaturalLogic.Ty.LE }

theorem NaturalLogic.Ty.LE.refl {B : Type u_1} (σ : Ty B) : σ.LE σ

theorem NaturalLogic.Ty.LE.trans {B : Type u_1} {σ τ μ : Ty B} : σ.LE τ → τ.LE μ → σ.LE μ

theorem NaturalLogic.Ty.LE.antisymm {B : Type u_1} {σ τ : Ty B} : σ.LE τ → τ.LE σ → σ = τ

@[instance_reducible]

instance NaturalLogic.Ty.instPartialOrder {B : Type u_1} : PartialOrder (Ty B)

Equations

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

@[simp]

theorem NaturalLogic.Ty.base_le_base {B : Type u_1} {b b' : B} : base b ≤ base b' ↔ b = b'

@[simp]

theorem NaturalLogic.Ty.not_base_le_arr {B : Type u_1} {b : B} {σ τ : Ty B} {m : Marking} : ¬base b ≤ σ.arr m τ

@[simp]

theorem NaturalLogic.Ty.not_arr_le_base {B : Type u_1} {b : B} {σ τ : Ty B} {m : Marking} : ¬σ.arr m τ ≤ base b

@[simp]

theorem NaturalLogic.Ty.arr_le_arr {B : Type u_1} {σ σ' τ τ' : Ty B} {m m' : Marking} : σ.arr m τ ≤ σ'.arr m' τ' ↔ σ' ≤ σ ∧ τ ≤ τ' ∧ m ≤ m'

@[irreducible]

instance NaturalLogic.Ty.decidableLE {B : Type u_1} [DecidableEq B] (σ τ : Ty B) : Decidable (σ ≤ τ)

Equations

• One or more equations did not get rendered due to their size.
• (NaturalLogic.Ty.base a).decidableLE (NaturalLogic.Ty.base b) = if h : a = b then isTrue ⋯ else isFalse ⋯
• (NaturalLogic.Ty.base a).decidableLE (a_1.arr a_2 a_3) = isFalse ⋯
• (a.arr a_1 a_2).decidableLE (NaturalLogic.Ty.base a_3) = isFalse ⋯

Compatibility join and marking erasure

def NaturalLogic.Ty.sup? {B : Type u_1} [DecidableEq B] : Ty B → Ty B → Option (Ty B)

The partial join of compatible types ([IMT17] Definition 3.3): defined when the two types share their unmarked skeleton and their domains exactly, joining the markings along the codomain spine.

Equations

• (NaturalLogic.Ty.base b).sup? (NaturalLogic.Ty.base b') = if b = b' then some (NaturalLogic.Ty.base b) else none
• (σ.arr m τ).sup? (σ'.arr m' τ') = if σ = σ' then Option.map (σ.arr (m ⊔ m')) (τ.sup? τ') else none
• x✝¹.sup? x✝ = none

@[simp]

theorem NaturalLogic.Ty.sup?_self {B : Type u_1} [DecidableEq B] (σ : Ty B) : σ.sup? σ = some σ

theorem NaturalLogic.Ty.le_of_mem_sup?_left {B : Type u_1} [DecidableEq B] {σ τ μ : Ty B} : σ.sup? τ = some μ → σ ≤ μ

Both compatible types lie below their join.

def NaturalLogic.Ty.unmark {B : Type u_1} : Ty B → Ty B

Erase the markings along the codomain spine ([IMT17] Definition 3.3, their σ̂).

Equations

• (NaturalLogic.Ty.base b).unmark = NaturalLogic.Ty.base b
• (σ.arr a τ).unmark = σ.arr NaturalLogic.Marking.unmarked τ.unmark

theorem NaturalLogic.Ty.le_unmark {B : Type u_1} (σ : Ty B) : σ ≤ σ.unmark

Every type embeds into its marking erasure.