]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/RELATIONAL/NPlus/monoid.ma
Full specification of find. Added notation for If_Then_Else. Probably a delta
[helm.git] / matita / contribs / RELATIONAL / NPlus / monoid.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/RELATIONAL/NPlus/monoid".
16
17 include "NPlus/fun.ma".
18
19 (* Monoidal properties ******************************************************)
20
21 theorem nplus_zero_1: \forall q. zero + q == q.
22  intros. elim q; clear q; autobatch.
23 qed.
24
25 theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to 
26                       (succ p) + q == (succ r).
27  intros. elim H; clear H q r; autobatch.
28 qed.
29
30 theorem nplus_comm: \forall p, q, x. (p + q == x) \to
31                     \forall y. (q + p == y) \to x = y.
32  intros 4; elim H; clear H q x;
33  [ lapply linear nplus_inv_zero_1 to H1
34  | lapply linear nplus_inv_succ_1 to H3. decompose
35  ]; subst; autobatch.
36 qed.
37
38 theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r.
39  intros. elim H; clear H q r; autobatch.
40 qed.
41
42 theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to
43                    \forall p3, s1. (r1 + p3 == s1) \to
44                    \forall r3. (p2 + p3 == r3) \to 
45                    \forall s3. (p1 + r3 == s3) \to s1 = s3.
46  intros 4. elim H; clear H p2 r1;
47  [ lapply linear nplus_inv_zero_1 to H2. subst.
48    lapply nplus_mono to H1, H3. subst. autobatch
49  | lapply linear nplus_inv_succ_1 to H3. decompose. subst.
50    lapply linear nplus_inv_succ_1 to H4. decompose. subst.
51    lapply linear nplus_inv_succ_2 to H5. decompose. subst. autobatch
52  ].
53 qed.
54  
55 (* Corollaries of functional properties **************************************)
56
57 theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to
58                      \forall q2. (p + q2 == r) \to q1 = q2.
59  intros. autobatch.
60 qed.
61
62 (* Corollaries of nonoidal properties ***************************************)
63
64 theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to
65                       \forall p2, r2. (p2 + q == r2) \to
66                       \forall x. (p2 + r1 == x) \to 
67                       \forall y. (p1 + r2 == y) \to
68                       x = y.
69  intros 4. elim H; clear H q r1;
70  [ lapply linear nplus_inv_zero_2 to H1
71  | lapply linear nplus_inv_succ_2 to H3.
72    lapply linear nplus_inv_succ_2 to H4. decompose. subst.
73    lapply linear nplus_inv_succ_2 to H5. decompose
74  ]; subst; autobatch.
75 qed.
76
77 theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
78                           \forall p2,r2. (p2 + q == r2) \to
79                           \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
80  intros 4. elim H; clear H q r1;
81  [ lapply linear nplus_inv_zero_2 to H1. subst
82  | lapply linear nplus_inv_succ_2 to H3. decompose. subst.
83    lapply linear nplus_inv_succ_2 to H4. decompose. subst
84  ]; autobatch.
85 qed.
86
87 (*                      
88 theorem nplus_shift_succ_sx: \forall p,q,r. 
89                              (p + (succ q) == r) \to (succ p) + q == r.
90  intros.
91  lapply linear nplus_inv_succ_2 to H as H0.
92  decompose. subst. auto new timeout=100.
93 qed.
94
95 theorem nplus_shift_succ_dx: \forall p,q,r. 
96                              ((succ p) + q == r) \to p + (succ q) == r.
97  intros.
98  lapply linear nplus_inv_succ_1 to H as H0.
99  decompose. subst. auto new timeout=100.
100 qed.
101
102 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to 
103                        \forall q2,r2. (r1 + q2 == r2) \to
104                        \exists q. (q1 + q2 == q) \land p + q == r2.
105  intros 2; elim q1; clear q1; intros;
106  [ lapply linear nplus_inv_zero_2 to H as H0.
107    subst.
108  | lapply linear nplus_inv_succ_2 to H1 as H0.
109    decompose. subst.
110    lapply linear nplus_inv_succ_1 to H2 as H0.
111    decompose. subst.
112    lapply linear H to H4, H3 as H0.
113    decompose.
114  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
115 qed.
116
117 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to 
118                        \forall p2,r2. (p2 + r1 == r2) \to
119                        \exists p. (p1 + p2 == p) \land p + q == r2.
120  intros 2; elim q; clear q; intros;
121  [ lapply linear nplus_inv_zero_2 to H as H0.
122    subst
123  | lapply linear nplus_inv_succ_2 to H1 as H0.
124    decompose. subst.
125    lapply linear nplus_inv_succ_2 to H2 as H0.
126    decompose. subst.
127    lapply linear H to H4, H3 as H0.
128    decompose.
129  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
130 qed.
131 *)