]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prove/provaIota.v
Minor bug fixes:
[helm.git] / helm / EXPORT / exportprove / prove / provaIota.v
1 Inductive bool : Set := true : bool | false : bool.
2 Inductive nat  : Set := O : nat | S : nat -> nat.
3
4 Fixpoint plus [n:nat] : nat -> nat :=
5   [m:nat]
6   Cases n of
7      O     => m
8    | (S n) => (S (plus n m))
9   end.
10
11 Fixpoint mult [n:nat] : nat -> nat :=
12   [m:nat]
13   Cases n of
14      O     => O
15    | (S n) => (plus m (mult n m))
16   end.
17
18 Fixpoint fact [n:nat] : nat  :=
19   Cases n of
20      O     => (S O)
21    | (S n) => (mult (S n) (fact n))
22   end.
23
24 Definition bnot :=
25  [b:bool]
26  Cases b of
27     true  => false
28   | false => true
29  end.
30
31 Fixpoint is_even [n:nat] : bool :=
32   Cases n of
33      O     => true
34    | (S n) => (bnot (bnot (is_odd n)))
35   end
36 with is_odd [n:nat] : bool :=
37   Cases n of
38      O     => false
39    | (S n) => (bnot (bnot (is_even n)))
40   end
41 .
42
43 Fixpoint idn [n:nat] : nat :=
44   Cases n of
45      O     => O
46    | (S n) => (S (idn n))
47   end.
48
49 Definition test1 := (is_even (S (S O))).
50 Definition test2 := (is_even (S (S (S O)))).
51 Definition test3 := (idn (idn (S O))).
52 Definition test4 := (is_odd (fact (S (S (O))))).
53 Definition test5 := (is_odd (fact (S (S (S (S (S (S O)))))))).