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_fwd.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 linear add_gen_O_2 to H as H0.
  26    rewrite > H0. clear H0 p
  27  | lapply linear add_gen_S_2 to H1 as H0.
  28    decompose.
  29    rewrite > H2. clear H2 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 linear add_gen_O_2 to H as H0.
  36    rewrite > H0. clear H0 p
  37  | lapply linear add_gen_S_2 to H1 as H0.
  38    decompose.
  39    rewrite > H2. clear H2 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 linear add_gen_S_2 to H as H0.
  46  decompose.
  47  rewrite > H1. clear H1 r.
  48  auto.
  49 qed.
  50
  51 theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r.
  52  intros.
  53  lapply linear add_gen_S_1 to H as H0.
  54  decompose.
  55  rewrite > H1. clear H1 r.
  56  auto.
  57 qed.
  58
  59 theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to
  60                      \forall q2,r2. add r1 q2 r2 \to
  61                      \exists q. add q1 q2 q \land add p q r2.
  62  intros 2; elim q1; clear q1; intros;
  63  [ lapply linear add_gen_O_2 to H as H0.
  64    rewrite > H0. clear H0 p
  65  | lapply linear add_gen_S_2 to H1 as H0.
  66    decompose.
  67    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
  68    lapply linear add_gen_S_1 to H2 as H0.
  69    decompose.
  70    rewrite > H2. clear H2 r2.
  71    lapply linear H to H4, H3 as H0.
  72    decompose.
  73  ]; apply ex_intro; [| auto || auto ]. (**)
  74 qed.
  75
  76 theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
  77                      \forall p2,r2. add p2 r1 r2 \to
  78                      \exists p. add p1 p2 p \land add p q r2.
  79  intros 2; elim q; clear q; intros;
  80  [ lapply linear add_gen_O_2 to H as H0.
  81    rewrite > H0. clear H0 p1
  82  | lapply linear add_gen_S_2 to H1 as H0.
  83    decompose.
  84    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
  85    lapply linear add_gen_S_2 to H2 as H0.
  86    decompose.
  87    rewrite > H2. clear H2 r2.
  88    lapply linear H to H4, H3 as H0.
  89    decompose.
  90  ]; apply ex_intro; [| auto || auto ]. (**)
  91 qed.
  92
  93 theorem add_conf: \forall p,q,r1. add p q r1 \to
  94                   \forall r2. add p q r2 \to r1 = r2.
  95  intros 2. elim q; clear q; intros;
  96  [ lapply linear add_gen_O_2 to H as H0.
  97    rewrite > H0 in H1. clear H0 p
  98  | lapply linear add_gen_S_2 to H1 as H0.
  99    decompose.
 100    rewrite > H3. clear H3 r1.
 101    lapply linear add_gen_S_2 to H2 as H0.
 102    decompose.
 103    rewrite > H2. clear H2 r2.
 104  ]; auto.
 105 qed.