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
they take both two arguments. They are the smallest predicates verifying
the given properties. The identifier
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
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
x left) and
P (S x0) (S y0) with three
Less x0 y0,
x = S x0 and
y = S y0.
The general syntax is:
You will remark that you can give a special syntax to your predicate.
-ce means to claim the elimination rule.
-cc means to claim the case reasonning.
-ci means to claim the introduction rule specific to