]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/fguidi.ma
removed a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow...
[helm.git] / helm / software / 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 set "baseuri" "cic:/matita/tests/fguidi/".
16 include "legacy/coq.ma".
17
18 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
20 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
21 alias id "le" = "cic:/matita/fguidi/le.ind#xpointer(1/1)".
22 alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
23 alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". 
24 alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
25 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
26 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
27
28 alias symbol "and" (instance 0) = "Coq's logical and".
29 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
30 alias symbol "exists" (instance 0) = "Coq's exists".
31
32 definition is_S: nat \to Prop \def
33    \lambda n. match n with 
34       [ O     \Rightarrow False
35       | (S n) \Rightarrow True
36       ].
37
38 definition pred: nat \to nat \def
39    \lambda n. match n with
40       [ O     \Rightarrow O
41       | (S n) \Rightarrow n
42       ]. 
43
44 theorem eq_gen_S_O: \forall x. (S x = O) \to \forall P:Prop. P.
45 intros. apply False_ind. cut (is_S O). auto paramodulation. elim H. exact I.
46 qed.
47
48 theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O).
49 intros. auto.
50 qed.
51
52 theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n. 
53 intros. cut ((pred (S m)) = (pred (S n))). 
54 assumption. elim H. auto paramodulation.
55 qed.
56
57 theorem eq_gen_S_S_cc: \forall m,n. m = n \to (S m) = (S n).
58 intros. elim H. auto paramodulation.
59 qed.
60
61 inductive le: nat \to nat \to Prop \def
62      le_zero: \forall n. (le O n)
63    | le_succ: \forall m, n. (le m n) \to (le (S m) (S n)).
64
65 theorem le_refl: \forall x. (le x x).
66 intros. elim x. auto paramodulation. auto paramodulation.
67 qed.
68
69 theorem le_gen_x_O_aux: \forall x, y. (le x y) \to (y =O) \to 
70                         (x = O).
71 intros 3. elim H. auto paramodulation. apply eq_gen_S_O. exact n1. auto paramodulation.
72 qed.
73
74 theorem le_gen_x_O: \forall x. (le x O) \to (x = O).
75 intros. apply le_gen_x_O_aux. exact O. auto paramodulation. auto paramodulation.
76 qed.
77
78 theorem le_gen_x_O_cc: \forall x. (x = O) \to (le x O).
79 intros. elim H. auto paramodulation.
80 qed.
81
82 theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to 
83                         (\exists n. x = (S n) \land (le m n)).
84 intros 4. elim H. 
85 apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
86 cut (n = m). elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto. (* paramodulation non trova la prova *)
87 qed.
88
89 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 
90                     (\exists n. x = (S n) \land (le m n)).
91 intros. apply le_gen_S_x_aux. exact (S m). auto paramodulation. auto paramodulation.
92 qed.
93
94 theorem le_gen_S_x_cc: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to
95                        (le (S m) x).
96 intros. elim H. elim H1. cut ((S x1) = x). elim Hcut. auto paramodulation. elim H2. auto paramodulation.
97 qed.
98
99 theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n).
100 intros.
101 lapply le_gen_S_x to H using H0. elim H0. elim H1. 
102 lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
103 qed.
104
105 theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
106 intros. auto paramodulation.
107 qed.
108
109 (*
110 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
111 intros 1. elim x; clear H. clear x. 
112 auto paramodulation.
113 fwd H1 [H]. decompose H.
114 *)