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.