]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/fguidi.ma
init_copy init_match
[helm.git] / matita / matita / tests / fguidi.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 include "logic/connectives.ma".
16 include "nat/nat.ma".
17
18 theorem eq_S_S: \forall m,n. m = n \to (S m) = (S n).
19 intros; destruct; autobatch.
20 qed.
21
22 inductive le: nat \to nat \to Prop \def
23      le_zero: \forall n. (le O n)
24    | le_succ: \forall m, n. (le m n) \to (le (S m) (S n)).
25
26 theorem le_refl: \forall x. (le x x).
27 intros; elim x; clear x; autobatch.
28 qed.
29
30 theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to (x = O).
31 intros 3; elim H; clear H x y;
32 [ autobatch
33 | destruct
34 ]
35 qed.
36
37 theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
38 intros; lapply linear le_gen_x_O_aux to H;
39 [ destruct; autobatch
40 | autobatch
41 ].
42 qed.
43
44 theorem le_x_O: \forall x. (x = O) \to (le x O).
45 intros; destruct; autobatch.
46 qed.
47
48 theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to 
49                         (\exists n. x = (S n) \land (le m n)).
50 intros 4; elim H; clear H x y;
51 [ destruct
52 | destruct; autobatch
53 ].
54 qed.
55
56 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 
57                     (\exists n. x = (S n) \land (le m n)).
58 intros; lapply le_gen_S_x_aux to H; autobatch.
59 qed.
60
61 theorem le_S_x: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to
62                 (le (S m) x).
63 intros; decompose; destruct; autobatch.
64 qed.
65
66 theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n).
67 intros.
68 lapply linear le_gen_S_x to H as H0; decompose; destruct; autobatch.
69 qed.
70
71 theorem le_S_S: \forall m,n. (le m n) \to (le (S m) (S n)).
72 intros; autobatch.
73 qed.
74
75 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
76 intros 3. elim H; clear H x y;
77 [ autobatch
78 | lapply linear le_gen_S_x to H3; decompose; destruct; autobatch.
79 ].
80 qed.