Next: Inductive data-types. Up: Inductive predicates and data-types. Previous: Inductive predicates and data-types.   Contents

Inductive predicates.

We will first start with some examples:

```Use nat.

Inductive Less x y =
zero : /\x Less N0 x
| succ : /\x,y (Less x y -> Less (S x) (S y))
.

Inductive Less2 x y =
zero : Less2 x x
| succ : /\y (Less2 x y -> Less2 x (S y))
.
```

This example shows two possible definitions for the predicate less or equal on natural numbers.

The name of the predicates will be `Less` and `Less2` and they take both two arguments. They are the smallest predicates verifying the given properties. The identifier `zero` and `succ` are just given to generate good names for the produced lemmas.

These lemmas, generated and proved by , are:

```zero.Less = /\x Less N0 x : theorem
succ.Less = /\x,y (Less x y -> Less (S x) (S y)) : theorem
```

Which are both added as introduction rules for that predicate with `zero` and `succ` as abbreviation (this means you can type `intro zero` or `intro succ` to specify which rule to use when guesses wrong).

```rec.Less =
/\X/\x,y
(/\x0 X N0 x0 ->
/\x0,y0 (Less x0 y0 -> X x0 y0 -> X (S x0) (S y0)) ->
Less x y -> X x y) : theorem

case.Less =
/\X/\x,y
((x = N0 -> X N0 y) ->
/\x0,y0 (Less x0 y0 -> x = S x0 -> y = S y0 -> X (S x0) (S y0)) ->
Less x y -> X x y) : theorem
```

The first one: `rec.less` is an induction principle (not very useful ?). It is added as an elimination rule. The second one is to reason by cases. It is added as an invertible left rule: If you want to prove `P x y` with an hypothesis `H := Less x y`, the command `left H` will ask you to prove `P N0 y` with the hypothesis `x = N0` (there may be other occurrences of `x` left) and `P (S x0) (S y0)` with three hypothesis: `Less x0 y0`, `x = S x0` and `y = S y0`.

The general syntax is:

 `Inductive` syntax `-ce` `-cc` = alpha-ident `-ci` : expr `|` alpha-ident `-ci` : expr

You will remark that you can give a special syntax to your predicate. The option `-ce` means to claim the elimination rule. The option `-cc` means to claim the case reasonning. The option `-ci` means to claim the introduction rule specific to that property.

Next: Inductive data-types. Up: Inductive predicates and data-types. Previous: Inductive predicates and data-types.   Contents
Christophe Raffalli 2005-03-02