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:

Inductivesyntax-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.