]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/paramodulation/irratsqrt2.ma
...
[helm.git] / helm / software / matita / tests / paramodulation / irratsqrt2.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 include "nat/times.ma".
18 include "nat/minus.ma".
19
20 theorem prova :
21   \forall n,m:nat.
22   \forall P:nat \to Prop.
23   \forall H:P (S (S O)).
24   \forall H:P (S (S (S O))).
25   \forall H1: \forall x.P x \to O = x.
26    O = S (S (S (S (S O)))).
27    intros.
28    autobatch.
29  qed.
30  
31 theorem example2:
32 \forall x: nat. (x+S O)*(x-S O) = x*x - S O.
33 intro;
34 apply (nat_case x);
35  [ autobatch timeout = 1.|intro.autobatch timeout = 1.]
36 qed.
37
38 theorem irratsqrt2_byhand:
39   \forall A:Set.
40   \forall m:A \to A \to A.
41   \forall divides: A \to A \to Prop.
42   \forall o,a,b,two:A.
43   \forall H1:\forall x.m o x = x.
44   \forall H1:\forall x.m x o = x.
45   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
46   \forall H1:\forall x.m x o = x.
47   \forall H2:\forall x,y.m x y = m y x.
48   \forall H3:\forall x,y,z. m x y = m x z \to y = z. 
49   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
50   \forall H4:\forall x,y.(divides x y \to (\exists z.m x z = y)). 
51   \forall H4:\forall x,y,z.m x z = y \to divides x y.
52   \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y.
53   \forall H5:m a a = m two (m b b).
54   \forall H6:\forall x.divides x a \to divides x b \to x = o.
55   two = o.
56   intros.
57   cut (divides two a);
58     [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
59     |elim (H6 ? ? Hcut).
60      cut (divides two b);
61        [ apply (H10 ? Hcut Hcut1).
62        | elim (H8 b b);[assumption.|assumption|
63          apply (H7 ? ? (m a1 a1));
64          apply (H5 two ? ?);rewrite < H9.
65          rewrite < H11.rewrite < H2.
66          apply eq_f.rewrite > H2.rewrite > H4.reflexivity.
67          ]
68          ]
69          ]
70 qed.
71          
72 theorem irratsqrt2_byhand':
73   \forall A:Set.
74   \forall m,f:A \to A \to A.
75   \forall divides: A \to A \to Prop.
76   \forall o,a,b,two:A.
77   \forall H1:\forall x.m o x = x.
78   \forall H1:\forall x.m x o = x.
79   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
80   \forall H1:\forall x.m x o = x.
81   \forall H2:\forall x,y.m x y = m y x.
82   \forall H3:\forall x,y,z. m x y = m x z \to y = z. 
83   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
84   \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). 
85   \forall H4:\forall x,y,z.m x z = y \to divides x y.
86   \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y.
87   \forall H5:m a a = m two (m b b).
88   \forall H6:\forall x.divides x a \to divides x b \to x = o.
89   two = o.
90   intros.
91   cut (divides two a);
92     [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
93     |(*elim (H6 ? ? Hcut). *)
94      cut (divides two b);
95        [ apply (H10 ? Hcut Hcut1).
96        | elim (H8 b b);[assumption.|assumption|
97        
98          apply (H7 ? ? (m (f two a) (f two a)));
99          apply (H5 two ? ?);
100          rewrite < H9.
101          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
102          rewrite < H2.apply eq_f.
103          rewrite < H4 in \vdash (? ? ? %).
104          rewrite > H2.reflexivity.
105          ]
106          ]
107          ]
108 qed.  
109      
110 theorem irratsqrt2:
111   \forall A:Set.
112   \forall m,f:A \to A \to A.
113   \forall divides: A \to A \to Prop.
114   \forall o,a,b,two:A.
115   \forall H1:\forall x.m o x = x.
116   \forall H1:\forall x.m x o = x.
117   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
118   \forall H1:\forall x.m x o = x.
119   \forall H2:\forall x,y.m x y = m y x.
120   \forall H3:\forall x,y,z. m x y = m x z \to y = z. 
121   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
122   \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). 
123   \forall H4:\forall x,y,z.m x z = y \to divides x y.
124   \forall H4:\forall x.divides two (m x x) \to divides two x.
125   \forall H5:m a a = m two (m b b).
126   \forall H6:\forall x.divides x a \to divides x b \to x = o.
127   two = o.
128 intros.
129 autobatch depth = 5 timeout = 180.
130 qed.
131
132 (* time: 146s *)
133
134  
135 (* intermediate attempts 
136
137   cut (divides two a);[|
138     (* apply H8;apply (H7 two (m a a) (m b b));symmetry;assumption. *)
139     autobatch depth = 4 width = 3 use_paramod = false. ]
140   (*autobatch depth = 5.*)
141   
142   apply H10;
143   [ assumption.
144   |(*autobatch depth = 4.*) apply H8;   
145          (*autobatch.*)
146          apply (H7 ? ? (m (f two a) (f two a)));
147          apply (H5 two ? ?);
148          cut ((\lambda x:A.m x (m two ?)=m x (m b b))?);
149          [|||simplify;
150          autobatch paramodulation.
151          (*autobatch new.*)
152          rewrite < H9.
153          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
154          rewrite < H2.apply eq_f.
155          rewrite < H4 in \vdash (? ? ? %).
156          rewrite > H2.reflexivity.
157   ]
158          
159 qed.
160 *)