Last updated on Friday, January 10, 2025

Proof of `InOrderTraversalMirror`

Points: 40 points
Topics: Computer-checked proofs, Pattern matching
Files to submit: src/main/scala/proof/InOrderMirrorProof.scala

In this exercise, your task is to write the inductive case of a computer-checked proof.

The first section defines the datatypes and axioms available to you, the second is a refresher on proof syntax and instructions to evaluate theorems, and the last section presents the graded question, the inductive case of InOrderTraversalMirror.

Datatypes and Axioms

Consider the following definition of binary trees:

sealed trait BinaryTree[+T]
case object Empty extends BinaryTree[Nothing]
case class Node[T](left: BinaryTree[T], x: T, right: BinaryTree[T]) extends BinaryTree[T]

and the usual definition of Scala lists:

sealed trait List[+T]
case object Nil extends List[Nothing]
case class Cons[T](head: T, tail: List[T]) extends List[T]

We use the infix notation x :: xs for Cons(x, xs).

All lemmas in this exercise hold for all types T and all x: T, xs, ys, zs: List[T], tree: BinaryTree[T], left: BinaryTree[T], right: BinaryTree[T].

On BinaryTree[T] we define functions inorder[T]: BinaryTree[T] => List[T] and mirror[T]: BinaryTree[T] => BinaryTree[T] specified by the following axioms:

object InOrder:
  val EmptyCase = Axiom:
    Empty.inOrder === Nil
  val NodeCase = Axiom:
    Node(left, x, right).inOrder ===
    left.inOrder ++ ((x :: Nil) ++ right.inOrder)

object Mirror:
  val EmptyCase = Axiom:
    Empty.mirror === Empty
  val NodeCase = Axiom:
    Node(left, x, right).mirror ===
    Node(right.mirror, x, left.mirror)

src/main/scala/proof/InOrderMirrorAxioms.scala

In addition, the binary function append on lists, noted as the infix operator ++, and the function reverse, given by the following Axioms:

object Reverse:
  val NilCase = Axiom:
    Nil.reverse === Nil
  val ConsCase = Axiom:
    (x :: xs).reverse === xs.reverse ++ (x :: Nil)
  val AppendCase = Axiom:
    (xs ++ ys).reverse === ys.reverse ++ xs.reverse
  val SingleCase = Axiom:
    (x :: Nil).reverse === x :: Nil

object Append:
  val NilCase = Axiom:
    (Nil ++ xs) === xs
  val ConsCase = Axiom:
    (x :: xs) ++ ys === x :: (xs ++ ys)
  val Associativity = Axiom:
    (xs ++ ys) ++ zs === xs ++ (ys ++ zs)

src/main/scala/proof/InOrderMirrorAxioms.scala

Refresher on Theorem Syntax

The syntax of a theorem involves the Theorem constructor, accepting a statement (possibly with assumptions), and a proof of the given statement.

The proof is a series of equalities and justifications, of the form x === y ==< Rule. As examples:

Without assumptions:

// example of a theorem applying two rules successively
val multipleRuleApplication = Theorem((Nil ++ Nil).map(f) === Nil):
  (Nil ++ Nil).map(f)
    === Nil.map(f)  ==< Append.NilCase
    === Nil         ==< Map.NilCase

src/main/scala/proof/MapSingleFlatten.scala

With assumptions:

// a formula to use as an assumption
val assumption = xs ++ Nil === Nil ++ xs

// example of a theorem using an assumption
// the assumption is automatically taken from the theorem statement
val usingAssumption = Theorem(assumption ==> (xs ++ Nil === xs)):
  xs ++ Nil
    === Nil ++ xs ==< assumption // if assumption is not in the statement, this will fail
    === xs        ==< Append.NilCase

src/main/scala/proof/MapSingleFlatten.scala

These examples were discussed in the list-proofs exercise. They can be found through Moodle.

The basic examples are also present in the file src/main/scala/proof/MapSingleFlatten.scala. These are available strictly for a refresher on proof syntax, and will not be considered for grading.

If you face issues with operators, e.g. operator ++ is not defined on Formula[T], put your whole terms inside parentheses. When in doubt, more parentheses are better. Also, some of the provided axioms allow you to manipulate parentheses.

Running and Testing Instructions

The proofs are checked automatically on running runMain proof.runTheorems in sbt or using run and selecting proof.runTheorems. You can use ~runMain proof.runTheorems to re-run the theorems on file modification for quick feedback.

Running the theorems will identify incorrect steps and report the line number. A correctly checked theorem will report Proved Theorem:

[info] running (fork) proof.runTheorems
[info] Proved Theorem EmptyCase: (Empty.mirror.inOrder === Empty.inOrder.reverse)

Since the proofs are checked by the system when running the theorems, the tests simply verify that the theorem and axiom statements have not been altered. The proofs may be additionally checked manually by teaching staff. The tests and printed information are for your feedback.

InOrderTraversalMirror

You need to prove the property InorderTraversalMirror:

tree.mirror.inOrder === tree.inOrder.reverse

The proof is done by induction, and is in two parts, EmptyCase, for tree being Empty, and NodeCase, for tree being Node(left, x, right) for some trees left and right, and x : T as above.

Base Case (example)

The base case is provided as an example of manipulating trees:

val EmptyCase = Theorem(EmptyCaseStatement):
  Empty.mirror.inOrder
    === Empty.inOrder         ==< Mirror.EmptyCase
    === Nil                   ==< InOrder.EmptyCase
    === Nil.reverse           ==< Reverse.NilCase
    === Empty.inOrder.reverse ==< InOrder.EmptyCase

src/main/scala/proof/InOrderMirrorProof.scala

Inductive case

Complete the proof of the inductive case, the theorem NodeCase, using the provided axioms and the inductive hypotheses IHLeft and IHRight:

val NodeCase = Theorem(NodeCaseStatement):
  Node(left, x, right).inOrder.reverse
  ???