Definition of ToSet and basic API

This file defines the ToSet class and its API needed for the inclusion tactic.

Implimentation Notes

• Inclusion.IntervalBool is nearly identical to Lean.LBool but with a seperate API and documentation which is catered to the needs of the inclusion tactic.

class Inclusion.ToSet (Iα : Type u_1) (α : outParam (Type u_2)) : Type (max u_1 u_2)

A ToSet Iα α instance provides a way of interpreting elements of Iα as sets of α, through a function toSet : Iα → Set α. In its use in the inclusion tactic, Iα will be a type with good computational properties (such as Interval Dyadic) and α will be some type that appears in the user's expression, such as ℝ.

• toSet : Iα → Set α

  The mapping of elements of Iα to sets in α.

@[instance_reducible]

instance Inclusion.instMembershipOfToSet {Iα : Type u_1} {α : Type u_2} [ToSet Iα α] : Membership α Iα

Equations

• Inclusion.instMembershipOfToSet = { mem := fun (s : Iα) (a : α) => Inclusion.ToSet.toSet s a }

theorem Inclusion.ToSet.mem_def {Iα : Type u_1} {α : Type u_2} [ToSet Iα α] (a : α) (s : Iα) : a ∈ s ↔ a ∈ toSet s

theorem Inclusion.ToSet.mem_of_eq_of_mem {Iα : Type u_1} {α : Type u_2} [ToSet Iα α] {x y : α} {s : Iα} (hxy : x = y) (hy : y ∈ s) : x ∈ s

theorem Inclusion.ToSet.mem_of_mem_of_eq {Iα : Type u_1} {α : Type u_2} [ToSet Iα α] {x y : α} {s : Iα} (hxy : x = y) (hx : x ∈ s) : y ∈ s

class Inclusion.Univ (Iα : Type u_1) (α : Type u_2) [ToSet Iα α] : Type u_1

A Univ Iα α instance is a specification of an element univ : Iα such that every element of α belongs to univ. This is useful for assigning a container to inclusion variables that have no inclusion hypotheses.

• univ : Iα

  A (computational) representative of the universal set.

• mem_univ (x : α) : x ∈ univ α

  Every element of α belongs to univ.

class Inclusion.Refine (Iα : Type u_1) (α : Type u_2) [ToSet Iα α] : Type u_1

A Refine Iα α instance is a specification of a (computable) function refine : Iα → Iα → Iα such that for any s t : Iα, s ∩ t ⊆ refine s t as sets of α. This is useful for merging multiple inclusion hypotheses of a single inclusion variable.

• refine : Iα → Iα → Iα

  A (computable) function to refine two inclusion hypotheses.

• mem_refine {x : α} {s t : Iα} (hs : x ∈ s) (ht : x ∈ t) : x ∈ refine α s t

  If x ∈ s and x ∈ t then x ∈ refine s t.

class Inclusion.Coarsen (Iα : Type u_1) (α : Type u_2) [ToSet Iα α] : Type u_1

A Coarsen Iα α instance is a specification of a (computable) function coarsen : Iα → Iα → Iα such that for any s t : Iα, s ∪ t ⊆ coarsen s t. This is useful for applying an inclusion function to a cover of the input and then merging the results.

• coarsen : Iα → Iα → Iα

  A represented set containing both input sets.

• mem_coarsen_left {x : α} {s t : Iα} (hx : x ∈ s) : x ∈ coarsen α s t

  If x ∈ s then x ∈ coarsen s t.

• mem_coarsen_right {x : α} {s t : Iα} (hx : x ∈ t) : x ∈ coarsen α s t

  If x ∈ t then x ∈ coarsen s t.

structure Inclusion.Cover (Iα : Type u_1) (α : Type u_2) [ToSet Iα α] : Type (max (u + 1) u_1)

A Cover Iα α specifies a function coverMap to compute a "refined" inclusion of F s for s : Iα and an inclusion function F : Iα → Iβ, by computing F on each element of a cover of s and then using coarsen to merge the results. Schematically

coverMap s F = fold coarsen (map F (cover s))

where cover : Iα → Array Iα would specify the underlying cover, but the coverMap formulation allows this function to be implemented more efficiently for kernel reduction.

• coverMap {Iβ β : Type u} [ToSet Iβ β] [Coarsen Iβ β] (s : Iα) (F : Iα → Iβ) : Iβ

  Compute an inclusion for F s using a cover of s.

• mem_coverMap {Iβ β : Type u} [ToSet Iβ β] [Coarsen Iβ β] {s : Iα} {F : Iα → Iβ} {x : α} {y : β} (hx : x ∈ s) (hy : ∀ (t : Iα), x ∈ t → y ∈ F t) : y ∈ self.coverMap s F

  If x ∈ s and ∀ t, x ∈ t → y ∈ F t then y ∈ coverMap s F.

inductive Inclusion.IntervalBool : Type

An IntervalBool represents the result of a Prop inclusion and is either true (if the proposition is computed true), false (if the proposition is computed false), or undetermined (if the computation is indeterminate).

• true : IntervalBool
• false : IntervalBool
• undetermined : IntervalBool

def Inclusion.IntervalBool.toPropSet : IntervalBool → Set Prop

The mapping from IntervalBool to Set Prop which identifies each option (true, false, undetermined) with its set of possible outcomes ({True}, {False}, {True, False} respectively).

Equations

• Inclusion.IntervalBool.true.toPropSet = {True}
• Inclusion.IntervalBool.false.toPropSet = {False}
• Inclusion.IntervalBool.undetermined.toPropSet = {True, False}

@[instance_reducible]

instance Inclusion.instToSetIntervalBoolProp : ToSet IntervalBool Prop

Equations

• Inclusion.instToSetIntervalBoolProp = { toSet := Inclusion.IntervalBool.toPropSet }

@[simp]

theorem Inclusion.IntervalBool.mem_true_iff {p : Prop} : p ∈ true ↔ p

@[simp]

theorem Inclusion.IntervalBool.mem_false_iff {p : Prop} : p ∈ false ↔ ¬p

theorem Inclusion.IntervalBool.mem_true {p : Prop} (hp : p) : p ∈ true

theorem Inclusion.IntervalBool.mem_false {p : Prop} (hp : ¬p) : p ∈ false

@[simp]

theorem Inclusion.IntervalBool.mem_undetermined (p : Prop) : p ∈ undetermined

def Inclusion.IntervalBool.not : IntervalBool → IntervalBool

Negation of an IntervalBool value.

Equations

• Inclusion.IntervalBool.true.not = Inclusion.IntervalBool.false
• Inclusion.IntervalBool.false.not = Inclusion.IntervalBool.true
• Inclusion.IntervalBool.undetermined.not = Inclusion.IntervalBool.undetermined

theorem Inclusion.IntervalBool.not_mem {p : Prop} {a : IntervalBool} (hp : p ∈ a) : (¬p) ∈ a.not

@[macro_inline]

def Inclusion.IntervalBool.and : IntervalBool → IntervalBool → IntervalBool

Conjunction of two IntervalBool values.

Equations

• Inclusion.IntervalBool.true.and Inclusion.IntervalBool.true = Inclusion.IntervalBool.true
• Inclusion.IntervalBool.false.and x✝ = Inclusion.IntervalBool.false
• x✝.and Inclusion.IntervalBool.false = Inclusion.IntervalBool.false
• x✝¹.and x✝ = Inclusion.IntervalBool.undetermined

theorem Inclusion.IntervalBool.and_mem {p q : Prop} {a b : IntervalBool} (hp : p ∈ a) (hq : q ∈ b) : (p ∧ q) ∈ a.and b

@[macro_inline]

def Inclusion.IntervalBool.or : IntervalBool → IntervalBool → IntervalBool

Disjunction of two IntervalBool values.

Equations

• Inclusion.IntervalBool.true.or x✝ = Inclusion.IntervalBool.true
• x✝.or Inclusion.IntervalBool.true = Inclusion.IntervalBool.true
• Inclusion.IntervalBool.false.or Inclusion.IntervalBool.false = Inclusion.IntervalBool.false
• x✝¹.or x✝ = Inclusion.IntervalBool.undetermined

theorem Inclusion.IntervalBool.or_mem {p q : Prop} {a b : IntervalBool} (hp : p ∈ a) (hq : q ∈ b) : (p ∨ q) ∈ a.or b

theorem Inclusion.true_of_mem_intervalBool_true {p : Prop} (hp : p ∈ IntervalBool.true) : p

theorem Inclusion.true_of_mem_intervalBool_eq_true {p : Prop} {b : IntervalBool} (hp : p ∈ b) (hb : b = IntervalBool.true) : p

def Inclusion.IntervalBool.isTrue : IntervalBool → Bool

Return true exactly when the input is IntervalBool.true.

Equations

• Inclusion.IntervalBool.true.isTrue = true
• Inclusion.IntervalBool.false.isTrue = false
• Inclusion.IntervalBool.undetermined.isTrue = false

theorem Inclusion.IntervalBool.eq_true_of_isTrue_eq_true {b : IntervalBool} (h : b.isTrue = Bool.true) : b = true

@[macro_inline]

def Inclusion.IntervalBool.union : IntervalBool → IntervalBool → IntervalBool

Union of two IntervalBools.

Equations

• Inclusion.IntervalBool.true.union Inclusion.IntervalBool.true = Inclusion.IntervalBool.true
• Inclusion.IntervalBool.false.union Inclusion.IntervalBool.false = Inclusion.IntervalBool.false
• x✝¹.union x✝ = Inclusion.IntervalBool.undetermined

@[instance_reducible]

instance Inclusion.instCoarsenIntervalBoolProp : Coarsen IntervalBool Prop

Equations

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