helm/software/matita/tests/letrecand.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/tests/letrecand".
  16
  17 include "nat/nat.ma".
  18
  19 let rec pari n : Prop :=
  20  match n with
  21   [ O ⇒ True
  22   | S n ⇒ dispari n
  23   ]
  24 and dispari n : Prop :=
  25  match n with
  26   [ O => False
  27   | S n => pari n
  28   ].
  29
  30 definition pari2 ≝
  31 let rec pari n : Prop :=
  32  match n with
  33   [ O ⇒ True
  34   | S n ⇒ dispari n
  35   ]
  36 and dispari n : Prop :=
  37  match n with
  38   [ O => False
  39   | S n => pari n
  40   ]
  41 in pari.
  42
  43 definition dispari2 ≝
  44 let rec pari n : Prop :=
  45  match n with
  46   [ O ⇒ True
  47   | S n ⇒ dispari n
  48   ]
  49 and dispari n : Prop :=
  50  match n with
  51   [ O => False
  52   | S n => pari n
  53   ]
  54 in dispari.
  55
  56 lemma test_pari: pari (S (S O)).
  57 simplify.
  58 constructor 1.
  59 qed.
  60
  61 lemma test_pari2: pari2 (S (S O)).
  62 simplify.
  63 constructor 1.
  64 qed.
  65
  66 lemma test_dispari: dispari (S O).
  67 simplify.
  68 constructor 1.
  69 qed.
  70
  71 lemma test_dispari2: dispari2 (S O).
  72 simplify.
  73 constructor 1.
  74 qed.