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

• The three markings are the signs 1 (+), -1 (−) and 0 (·), composing under valence composition as signs multiply; they are compared by information (MarkingLE), a join-semilattice with · on top (markingSup), not by the order of SignType.
• 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

A monotonicity marking ([IMT17] Definition 3.1) is a sign: 1 (+, monotone), -1 (−, antitone) or 0 (·, no information), composing as signs multiply.

def NaturalLogic.MarkingLE (m m' : SignType) : Prop

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

Equations

• NaturalLogic.MarkingLE m m' = (m = m' ∨ m' = 0)

@[instance_reducible]

instance NaturalLogic.instDecidableRelSignTypeMarkingLE : DecidableRel MarkingLE

Equations

• NaturalLogic.instDecidableRelSignTypeMarkingLE x✝¹ x✝ = { decide := decide (x✝¹ = x✝) || decide (x✝ = 0), reflects_decide := ⋯ }

theorem NaturalLogic.MarkingLE.refl (m : SignType) : MarkingLE m m

theorem NaturalLogic.MarkingLE.trans {a b c : SignType} (h₁ : MarkingLE a b) (h₂ : MarkingLE b c) : MarkingLE a c

theorem NaturalLogic.MarkingLE.antisymm {a b : SignType} (h₁ : MarkingLE a b) (h₂ : MarkingLE b a) : a = b

theorem NaturalLogic.markingLE_zero (m : SignType) : MarkingLE m 0

def NaturalLogic.markingSup (m m' : SignType) : SignType

The join in the information order: a marking with itself, · otherwise.

Equations

• NaturalLogic.markingSup m m' = if m = m' then m else 0

@[simp]

theorem NaturalLogic.markingSup_self (m : SignType) : markingSup m m = m

theorem NaturalLogic.markingLE_markingSup_left (m m' : SignType) : MarkingLE m (markingSup m m')

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 → SignType → 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' : SignType} : σ'.LE σ → τ.LE τ' → MarkingLE 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 : SignType} : ¬base b ≤ σ.arr m τ

@[simp]

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

@[simp]

theorem NaturalLogic.Ty.arr_le_arr {B : Type u_1} {σ σ' τ τ' : Ty B} {m m' : SignType} : σ.arr m τ ≤ σ'.arr m' τ' ↔ σ' ≤ σ ∧ τ ≤ τ' ∧ MarkingLE 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 (NaturalLogic.markingSup 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 0 τ.unmark

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

Every type embeds into its marking erasure.