]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/algebra/bool.ma
ground: some arithmetical properties added
[helm.git] / matita / matita / nlibrary / algebra / bool.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
17 inductive eq (A: Type[1]) (a: A) : A → CProp[0] ≝
18  refl: eq A a a. 
19
20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
21  
22 lemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a = b → P b.
23 #A; #a; #P; #p; #b; #E; cases E; assumption;
24 qed.
25
26 lemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
27 #A; #a; #P; #p; #b; #E; cases E in p; //;
28 qed. 
29
30 lemma csc : 
31  (∀x,y,z.(x∨(y∨z)) = ((x∨y)∨z)) →
32  (∀x,y,z.(x∧(y∧z)) = ((x∧y)∧z)) →
33  (∀x,y.(x∨y) = (y∨x)) →
34  (∀x,y.(x∧y) = (y∧x)) →
35  (∀x,y,z.(x∧(y∨z)) = ((x∧y)∨(x∧z))) →
36  (∀x.(x∨False) = (x)) →
37  (∀x.(x∧True) = (x)) →
38  (∀x.(x∧False) = (False)) →
39  (∀x.(x∨x) = (x)) →
40  (∀x.(x∧x) = (x)) →
41  (∀x,y.(x∧(x∨y)) = (x)) →
42  (∀x,y.(x∨(x∧y)) = (x)) →
43  (∀x,y,z.(x∨(y∧z)) = ((x∨y)∧(x∨z))) →
44  (∀x.(x∨True) = (True)) →
45  (∀x.(x∧¬x) = (False)) →
46  (∀x.(x∨¬x) = (True)) →
47  ∀a,b.((a ∧ ¬b) ∨ b) = (a ∨ b).
48 #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10; #H11; #H12;
49 #H13; #H14; #H15; #H16; #a; #b;
50 letin proof ≝ (
51 let clause_11: ∀x24. eq CProp[0] (And x24 True) x24
52  ≝ λx24. H7 x24 in
53  let clause_2: ∀x2. eq CProp[0] (Or x2 (Not x2)) True
54   ≝ λx2. H16 x2 in
55   let clause_5:
56    ∀x8.
57     ∀x9.
58      ∀x10.
59       eq CProp[0] (Or x8 (And x9 x10)) (And (Or x8 x9) (Or x8 x10))
60    ≝ λx8. λx9. λx10. H13 x8 x9 x10
61    in
62    let clause_15:
63     ∀x35.
64      ∀x36. eq CProp[0] (Or x35 x36) (Or x36 x35)
65     ≝ λx35. λx36. H3 x35 x36 in
66     let clause_194: eq CProp[0] (Or a b) (Or a b)
67      ≝ refl ?? in
68      let clause_193: eq CProp[0] (And (Or a b) True) (Or a b)
69       ≝ eq_ind_r_CProp0 CProp[0] (Or a b)
70             (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_194
71             (And (Or a b) True) (clause_11 (Or a b)) in
72       let clause_192: eq CProp[0] (And (Or a b) (Or b (Not b))) (Or a b)
73        ≝ eq_ind_r_CProp0 CProp[0] True
74              (λx:CProp[0]. eq CProp[0] (And (Or a b) x) (Or a b)) clause_193
75              (Or b (Not b)) (clause_2 b) in
76        let clause_191: eq CProp[0] (And (Or b a) (Or b (Not b))) (Or a b)
77         ≝ eq_ind_r_CProp0 CProp[0] (Or a b)
78               (λx:CProp[0]. eq CProp[0] (And x (Or b (Not b))) (Or a b))
79               clause_192 (Or b a) (clause_15 b a) in
80         let clause_190: eq CProp[0] (Or b (And a (Not b))) (Or a b)
81          ≝ eq_ind_r_CProp0 CProp[0] (And (Or b a) (Or b (Not b)))
82                (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_191
83                (Or b (And a (Not b))) (clause_5 b a (Not b)) in
84          let clause_1: eq CProp[0] (Or (And a (Not b)) b) (Or a b)
85           ≝ eq_ind_r_CProp0 CProp[0] (Or b (And a (Not b)))
86                 (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_190
87                 (Or (And a (Not b)) b) (clause_15 (And a (Not b)) b) in
88           clause_1);
89 apply proof;
90 qed.