Datatype Rules

Datatype rules may seem a bit difficult to understand at first sight. Here are a few examples intended to make them clearer.

Datatypes used

The rules will be applied to the following datatypes:

Directions:

direction ::=
    north
  | east
  | south
  | west

Let us have a function

$\operatorname{move} \in \Z \cprod \Z \cprod \operatorname{direction} \tfun \Z \cprod \Z$

first two arguments are a start position, third is a direction, result is the end position.

Lists:

list(T) ::=
    nil
  | cons( head : T, tail : list(T) )

Let us have a predicate

$\operatorname{member}(T, list(T))$

meaning that the first argument is a member of the list.

Trees:

tree(T) ::=
  empty
| node( left : tree(T), value : T, right : tree(T) )

Let us have a function

$\operatorname{height} \in \operatorname{Tree} \tfun \N$

defining the height of a tree

Distinct Case

The rule states

$\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }$

Distinct Case on directions

Starting from goal

$\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y$

we can free variables x,y,d then apply Distinct Case on d:

The resulting proof step is

$\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y  \qquad  d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad  d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad  d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{  \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }$

further simplifications depend on the existence of rules about move and the various directions.

Distinct Case on lists

Starting from goal

$\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)$

we can free variable l then apply Distinct Case on it:

$\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)  \qquad  l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{  \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }$

The left antecedent shows that the case of the nil list has been forgotten when writing the theorem. The right antecedent looks as hard to prove as the initial goal (but see the induction application).

Distinct Case on trees

Starting from goal

$\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)$

we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

$\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t)  \qquad  t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }$

the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.

Induction

The rule states

$\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }$

The only difference with Distinct Case resides in the $\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})$ hypotheses for inductive parameters.

Induction on directions

Starting from goal

$\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y$

we can free variables x,y,d then apply Induction on d:

The resulting proof step is

$\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y  \qquad  d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad  d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad  d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{  \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }$

As we can see, it is exactly the same proof step as for Distinct Case: the reason is that the direction constructors contain no parameters, a fortiori no inductive parameters, so there are no additional hypotheses.

Induction on lists

Starting from goal

$\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)$

we can free variable l then apply Induction on it:

$\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)  \qquad  l=\operatorname{cons}(head0, tail1) \;,\; \exists x \qdot \operatorname{member}(x,tail1) \land (\forall y \qdot \operatorname{member}(y,tail1) \limp y \leq x) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{  \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }$

The left antecedent shows the same problem as Distinct for nil list. The benefit of the Induction is in the right antecedent with the additional hypothesis that the predicate stands for tail1. Next step will be to make eh on l, free the x in the tail1 hypothesis, then use it to instantiate the x in the goal with $\operatorname{max}(\operatorname{head0}, x_{\operatorname{tail1}})$. In this proof, application of Distinct Case does not allow to complete the proof (at least not so easily), whereas Induction does.

Induction on trees

Starting from goal

$\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)$

we can free variables l,v,r,t then apply IMP_R and then Induction on t:

$\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty})  \qquad  t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;,\;\; \operatorname{height}(\operatorname{left0}) < \operatorname{height}(t) \;,\;\; \operatorname{height}(\operatorname{right2}) < \operatorname{height}(t) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }$

the left antecedent will then be proved using the contradiction in hypotheses. In the right one, additional induction hypotheses do not provide much help: in this situation, using Distinct Case and properties about height is sufficient to discharge the proof.