Доказательство структурной индукции на объединении IntSet

Question

Предположим, у вас есть следующее определение:

abstract class IntSet {
  def incl(x: Int): IntSet    
  def contains(x: Int): Boolean    
  def union(other: IntSet): IntSet
}

case class NonEmpty(elem: Int, left: IntSet, right: IntSet) extends IntSet {
  def incl(x: Int) =
    if (x < elem) NonEmpty(elem, left incl x, right)
    else if (x > elem) NonEmpty(elem, left, right incl x)
    else this

  def contains(x: Int) =
    if (x < elem) left contains x
    else if (x > elem) right contains x
    else true

  def union(other: IntSet) = (left union (right union other)) incl elem
}

object Empty extends IntSet {
  def incl(x: Int) = NonEmpty(x, Empty, Empty)    
  def contains(x: Int) = false    
  def union(other: IntSet) = other
}

и следующее предложение должно быть доказано:

(xs union ys) contains x = xs contains x || ys contains x

Отсюда я выводю два базовых случая. xs = пусто, а ys = пусто. Это второй базовый случай, когда я застрял по следующим причинам:

// substituting ys = Empty
 (xs union Empty) contains x = xs contains x || Empty contains x
// RHS:
 xs contains x || false
 xs contains x
// LHS:
 ((left union (right union Empty)) incl elem) contains x // By definition of NonEmpty.union

Как я могу уменьшить LHS, чтобы хз содержит х? Должен ли я сделать еще одну гипотезу индукции для xs union Empty = xs, и если да, то как это можно использовать в выражении?

Answer 1

Чтобы доказать:

(xs union ys) contains x = xs contains x || ys contains x

Дано:

1. Определения выше
2. Empty contains x = false
3. (s incl x) contains x = true
4. (s incl y) contains x = s contains x ; if x != y

Шаг индукции и структурное доказательство с использованием только xs, а не ys, пожалуйста, обратитесь к исходной проблеме

---

Случай I:

if xs = Empty

Левая сторона:
(Empty union ys) contains x
= ys contains x => Definition of Empty union other

Правая сторона:
Empty contains x || ys contains x
= false || ys contains x => Definition of Empty contains x
= ys contains x => Truth table of OR ( false OR true = true, false OR false = false)

Левая сторона = правая сторона, следовательно, шаг индукции доказан, утверждение верно для всех поддеревьев

---

Случай II:
if (xs is NonEmpty(z, l, r) and z = x)

Левая сторона:
(NonEmpty(x, l, r) union ys) contains x
= ((l union(r union ys)) incl x) contains x => From definition of union on NonEmpty
= true => from (3) above (s incl x) contains x = true

Правая сторона:
xs contains x || ys contains x
= NonEmpty(x, l, r) contains x || ys contains x => From definition of xs
= true || ys contains x => From definition of contains on NonEmpty
= true => Truth table of OR (true OR false = true, true OR true = true)

Левая сторона = правая сторона

---

Случай III:
if ( xs is NonEmpty(z, l, r) and z < x )

Левая сторона:
(NonEmpty(z, l, r) union ys) contains x
= (l union(r union ys) incl z) contains x => From definition of union
= (l union(r union ys)) contains x => From (4) above (s incl x) contains y = s contains y; if x != y
= (l contains x || (r union ys) contains x) => From induction step, the statement is true for all subtrees
= (l contains x || r contains x || ys contains x) => From induction step, the statement is true for all subtrees
= r contains x || ys contains x => since z < x, definition of contains (l contains x) returns false

Правая сторона:
(if z < x)
NonEmpty(z, l, r) contains x || ys contains x
= r contains x || ys contains x => definition of contains,

Левая сторона = Правая сторона,

---

Дело if ( xs is NonEmpty(z, l, r) and z > x ) аналогично случаю III выше. Следовательно, доказано