+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+
inductive True: Prop \def
I : True.
qed.
-definition plus : nat \to nat \to nat \def
-let rec plus (n,m) \def
+let rec plus n m \def
match n with
[ O \Rightarrow m
- | (S p) \Rightarrow S (plus p m) ]
-in
-plus.
+ | (S p) \Rightarrow S (plus p m) ].
theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
qed.
-definition times : nat \to nat \to nat \def
-let rec times (n,m) \def
+let rec times n m \def
match n with
[ O \Rightarrow O
- | (S p) \Rightarrow (plus m (times p m)) ]
-in
-times.
+ | (S p) \Rightarrow (plus m (times p m)) ].
theorem times_n_O: \forall n:nat. eq nat O (times n O).
intros.elim n.simplify.apply refl_equal.simplify.assumption.
simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
qed.
-definition minus : nat \to nat \to nat \def
-let rec minus (n,m) \def
- [\lambda n:nat.nat] match n with
+let rec minus n m \def
+ match n with
[ O \Rightarrow O
| (S p) \Rightarrow
- [\lambda n:nat.nat] match m with
+ match m with
[O \Rightarrow (S p)
- | (S q) \Rightarrow minus p q ]]
-in
-minus.
+ | (S q) \Rightarrow minus p q ]].
theorem nat_case :
\forall n:nat.\forall P:nat \to Prop.
apply le_S_n.assumption.
qed.
-definition leb : nat \to nat \to bool \def
-let rec leb (n,m) \def
- [\lambda n:nat.bool] match n with
+let rec leb n m \def
+ match n with
[ O \Rightarrow true
| (S p) \Rightarrow
- [\lambda n:nat.bool] match m with
+ match m with
[ O \Rightarrow false
- | (S q) \Rightarrow leb p q]]
-in leb.
+ | (S q) \Rightarrow leb p q]].
theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
intros.