Inductively Defined Propositions

In the Logic chapter, we examined various ways of writing propositions, including conjunction, disjunction, and quantifiers. In this chapter, we add a new tool to the mix: inductive definitions.

Remember that we saw two ways to state that a number n is even: we can say (1) Evenb n = Bool.true or (2) (k => Equal n (Nat.double k)). Another possibility is to say that n is even if we can establish its parity based on the following rules:

  • Ev_0 Rule: The number 0 is even.
  • Ev_SS Rule: If n is even, then Nat.succ (Nat.succ n) is even.

To illustrate how this definition of parity works, let's imagine using it to show that 4 is even. By the Ev_SS rule, it suffices to show that 2 is even. This, in turn, is guaranteed again by the Ev_SS rule, provided we can show that 0 is even. But this last fact follows directly from the Ev_0 rule.

We will see many definitions like this throughout the rest of the course. For informal discussions, it is helpful to have a lightweight notation that makes reading and writing easier. Inference rules are one such notation:


$$ \frac{ }{Ev\ \ 0} \ \ ev_0 $$


$$ \frac{\ \ \ \ ev\ \ \ \ \ }{Ev\ \ (Nat.succ \ (Nat.succ \ n))} \ \ ev_SS $$


Each of the textual rules above is reformatted here as an inference rule; the intended reading is that if the premises above the line are all valid, then the conclusion below the line follows. For example, the ev_SS rule says that if n satisfies ev, then Nat.succ (Nat.succ n) also satisfies it. If a rule has no premises above the line, then its conclusion is valid unconditionally.

We can represent a proof using these rules by combining the applications of rules into a proof tree. Here is how we could transcribe the above proof that 4 is even:

$$ \frac{ }{Ev\ \ 0} \ \ ev_0 \ \ \ \ \frac{ }{Ev\ \ 2} \ \ ev_SS \ \ \ \ \frac{ }{Ev\ \ 4} \ \ ev_SS \ \ \ \ \frac{ }{Ev\ \ 6} \ \ ev_SS \ $$


Why call this a "tree" (instead of a "stack," for example)? Because, in general, inference rules can have multiple premises. We will see examples of this below.
Putting it all together, we can translate the definition of parity into a formal definition in Kind using a data declaration, where each constructor corresponds to an inference rule: 
type Ev ~ (n: Nat){
  ev_0 : Ev Nat.zero
  ev_ss <n : Nat> (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
}

This definition differs in a crucial aspect from previous uses of data: its result is not a Type but rather a function from Nat to Type – that is, a property of numbers. Note that we have seen other inductive definitions that result in functions, such as List, whose type is Type -> Type. What is new here is that, since the Nat argument of Ev is unnamed and appears to the right of the colon, it is allowed to take different values in the types of different constructors: Nat.zero in the type of ev_z and Nat.succ (Nat.succ n) in the type of ev_ss.

On the other hand, the definition of List globally names the parameter x, forcing the result of Nil and Cons to be the same (List x). If we had tried to omit the type n: Nat when defining ev_ss, we would have seen an error

type Wrong_ev ~ (n: Nat){
  wrong_ev_0 : Ev Nat.zero
  wrong_ev_ss (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
}

Com o seguinte retorno:

   - ERROR  Cannot find the definition 'n'.

      ┌──[ev.kind2:9:25]
      │
    8 │      wrong_ev_z : Ev Nat.zero
    9 │      wrong_ev_ss (pred: Ev n) : Ev (Nat.succ (Nat.succ n))
      │                            ┬                           ┬
      │                            │                           └Here!
      │                            └Here!
   10 │

("Parameter" here is jargon from Kind for an argument to the left of the colon in an inductive definition; "index" is used to refer to arguments to the right of the colon.)

We can think of the definition of Ev as defining a property of the Kind Ev: Nat -> Type, along with the theorems ev_z: Ev 0 and ev_ss <n : Nat> (pred: Ev n) : Ev (Nat.succ (Nat.succ n)). Such "constructor theorems" have the same status as proven theorems. In particular, we can apply rule names as functions to each other to prove Ev for specific numbers...

Ev_4 : Ev 4n
Ev_4 = Ev.ev_ss 2n (Ev.ev_ss 0n Ev.ev_z)

We can also prove theorems that have hypotheses involving Ev.

Ev_plus5 (n: Nat) : Ev n -> Ev (Nat.add 4n n)
Ev_plus5 n = x => Ev.ev_ss (Ev.ev_ss x)

More generally, we can show that any number multiplied by 2 is even.

Ev_double

Ev_double (n: Nat) : Ev (Nat.double n)
Ev_double n = ?