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