helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.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-ARITHMETICS/add_props".
  16
  17 include "add_gen.ma".
  18
  19 theorem add_O_1: \forall q. add O q q.
  20  intros. elim q; clear q; auto.
  21 qed.
  22
  23 theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
  24  intros 2. elim q; clear q;
  25  [ lapply add_gen_O_2 to H as H0. clear H.
  26    rewrite > H0. clear H0. clear p
  27  | lapply add_gen_S_2 to H1 as H0. clear H1.
  28    decompose H0.
  29    rewrite > H2. clear H2. clear r
  30  ]; auto.
  31 qed.
  32
  33 theorem add_sym: \forall p,q,r. add p q r \to add q p r.
  34  intros 2. elim q; clear q;
  35  [ lapply add_gen_O_2 to H as H0. clear H.
  36    rewrite > H0. clear H0. clear p
  37  | lapply add_gen_S_2 to H1 as H0. clear H1.
  38    decompose H0.
  39    rewrite > H2. clear H2. clear r
  40  ]; auto.
  41 qed.
  42
  43 theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r.
  44  intros.
  45  lapply add_gen_S_2 to H as H0. clear H.
  46  decompose H0.
  47  rewrite > H1. clear H1. clear r.
  48  auto.
  49 qed.
  50
  51
  52 theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r.
  53  intros.
  54  lapply add_gen_S_1 to H as H0. clear H.
  55  decompose H0.
  56  rewrite > H1. clear H1. clear r.
  57  auto.
  58 qed.
  59
  60 theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to
  61                      \forall q2,r2. add r1 q2 r2 \to
  62                      \exists q. add q1 q2 q \land add p q r2.
  63  intros 2; elim q1; clear q1; intros;
  64  [ lapply add_gen_O_2 to H as H0. clear H.
  65    rewrite > H0. clear H0. clear p
  66  | lapply add_gen_S_2 to H1 as H0. clear H1.
  67    decompose H0.
  68    rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
  69    lapply add_gen_S_1 to H2 as H0. clear H2.
  70    decompose H0.
  71    rewrite > H2. clear H2. clear r2.
  72    lapply H to H4, H3 as H0. clear H. clear H4. clear H3.
  73    decompose H0.
  74  ]; apply ex_intro; [| auto || auto ]. (**)
  75 qed.
  76
  77 theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
  78                      \forall p2,r2. add p2 r1 r2 \to
  79                      \exists p. add p1 p2 p \land add p q r2.
  80  intros 2; elim q; clear q; intros;
  81  [ lapply add_gen_O_2 to H as H0. clear H.
  82    rewrite > H0. clear H0. clear p1
  83  | lapply add_gen_S_2 to H1 as H0. clear H1.
  84    decompose H0.
  85    rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
  86    lapply add_gen_S_2 to H2 as H0. clear H2.
  87    decompose H0.
  88    rewrite > H2. clear H2. clear r2.
  89    lapply H to H4, H3 as H0. clear H. clear H4. clear H3.
  90    decompose H0.
  91  ]; apply ex_intro; [| auto || auto ]. (**)
  92 qed.
  93
  94 theorem add_conf: \forall p,q,r1. add p q r1 \to
  95                   \forall r2. add p q r2 \to r1 = r2.
  96  intros 2. elim q; clear q; intros;
  97  [ lapply add_gen_O_2 to H as H0. clear H.
  98    rewrite > H0 in H1. clear H0. clear p
  99  | lapply add_gen_S_2 to H1 as H0. clear H1.
 100    decompose H0.
 101    rewrite > H3. clear H3. clear r1.
 102    lapply add_gen_S_2 to H2 as H0. clear H2.
 103    decompose H0.
 104    rewrite > H2. clear H2. clear r2.
 105  ]; auto.
 106 qed.
 107
 108
 109
 110 theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
 111  intros 2. elim q; clear q; intros;
 112  [ lapply add_gen_O_2 to H as H0. clear H.
 113    rewrite > H0. clear H0. clear p
 114  | lapply add_gen_S_2 to H1 as H0. clear H1.
 115    decompose H0.
 116    lapply eq_gen_S_S to H2 as H0. clear H2.
 117    rewrite < H0 in H3. clear H0. clear a
 118  ]; auto.
 119 qed.
 120
 121 theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
 122  intros.
 123  lapply add_sym to H. clear H.
 124  auto.
 125 qed.