]> matita.cs.unibo.it Git - helm.git/blob - matita/library_auto/auto/nat/times.ma
debian package for matita
[helm.git] / matita / library_auto / auto / nat / times.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 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/library_auto/nat/times".
16
17 include "auto/nat/plus.ma".
18
19 let rec times n m \def 
20  match n with 
21  [ O \Rightarrow O
22  | (S p) \Rightarrow m+(times p m) ].
23
24 (*CSC: the URI must disappear: there is a bug now *)
25 interpretation "natural times" 'times x y = (cic:/matita/library_auto/nat/times/times.con x y).
26
27 theorem times_n_O: \forall n:nat. O = n*O.
28 intros.elim n
29 [ auto
30   (*simplify.
31   reflexivity.*)
32 | simplify.  (* qui auto non funziona: Uncaught exception: Invalid_argument ("List.map2")*)
33   assumption.
34 ]
35 qed.
36
37 theorem times_n_Sm : 
38 \forall n,m:nat. n+(n*m) = n*(S m).
39 intros.elim n
40 [ auto.
41   (*simplify.reflexivity.*)
42 | simplify.
43   auto
44   (*apply eq_f.
45   rewrite < H.
46   transitivity ((n1+m)+n1*m)
47  [ symmetry.                    
48    apply assoc_plus.            
49  | transitivity ((m+n1)+n1*m)
50    [ apply eq_f2.
51      apply sym_plus.
52      reflexivity.
53    | apply assoc_plus.
54    ]
55  ]*)
56 ]
57 qed.
58
59 (* NOTA:
60    se non avessi semplificato con auto tutto il secondo ramo della tattica
61    elim n, avrei comunque potuto risolvere direttamente con auto entrambi
62    i rami generati dalla prima applicazione della tattica transitivity
63    (precisamente transitivity ((n1+m)+n1*m)
64  *)
65
66 theorem times_n_SO : \forall n:nat. n = n * S O.
67 intros.
68 rewrite < times_n_Sm.
69 auto paramodulation. (*termina la dim anche solo con auto*)
70 (*rewrite < times_n_O.
71 rewrite < plus_n_O.
72 reflexivity.*)
73 qed.
74
75 theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
76 intros.
77 simplify.
78 auto paramodulation. (* termina la dim anche solo con auto*)
79 (*rewrite < plus_n_O.
80 reflexivity.*)
81 qed.
82
83 theorem symmetric_times : symmetric nat times. 
84 unfold symmetric.
85 intros.elim x
86 [ auto
87   (*simplify.apply times_n_O.*)
88 | simplify.
89   auto
90   (*rewrite > H.apply times_n_Sm.*)
91 ]
92 qed.
93
94 variant sym_times : \forall n,m:nat. n*m = m*n \def
95 symmetric_times.
96
97 theorem distributive_times_plus : distributive nat times plus.
98 unfold distributive.
99 intros.elim x;simplify
100 [ reflexivity.
101 | auto
102   (*rewrite > H.
103   rewrite > assoc_plus.
104   rewrite > assoc_plus.
105   apply eq_f.
106   rewrite < assoc_plus. 
107   rewrite < (sym_plus ? z).
108   rewrite > assoc_plus.
109   reflexivity.*)
110 ]
111 qed.
112
113 variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
114 \def distributive_times_plus.
115
116 theorem associative_times: associative nat times.
117 unfold associative.intros.
118 elim x;simplify
119 [ apply refl_eq
120 | auto
121   (*rewrite < sym_times.
122   rewrite > distr_times_plus.
123   rewrite < sym_times.
124   rewrite < (sym_times (times n y) z).
125   rewrite < H.
126   apply refl_eq.*)
127 ]
128 qed.
129
130 variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
131 associative_times.