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