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