helm/software/matita/contribs/RELATIONAL/NPlus/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/NPlus/props".
  16
  17 include "NPlus/fwd.ma".
  18
  19 theorem nplus_zero_1: \forall q. zero + q == q.
  20  intros. elim q; clear q; auto.
  21 qed.
  22
  23 theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
  24                        (succ p) + q == (succ r).
  25  intros 2. elim q; clear q;
  26  [ lapply linear nplus_gen_zero_2 to H as H0.
  27    rewrite > H0. clear H0 p
  28  | lapply linear nplus_gen_succ_2 to H1 as H0.
  29    decompose.
  30    rewrite > H2. clear H2 r
  31  ]; auto.
  32 qed.
  33
  34 theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
  35  intros 2. elim q; clear q;
  36  [ lapply linear nplus_gen_zero_2 to H as H0.
  37    rewrite > H0. clear H0 p
  38  | lapply linear nplus_gen_succ_2 to H1 as H0.
  39    decompose.
  40    rewrite > H2. clear H2 r
  41  ]; auto.
  42 qed.
  43
  44 theorem nplus_shift_succ_sx: \forall p,q,r.
  45                               (p + (succ q) == r) \to (succ p) + q == r.
  46  intros.
  47  lapply linear nplus_gen_succ_2 to H as H0.
  48  decompose.
  49  rewrite > H1. clear H1 r.
  50  auto.
  51 qed.
  52
  53 theorem nplus_shift_succ_dx: \forall p,q,r.
  54                               ((succ p) + q == r) \to p + (succ q) == r.
  55  intros.
  56  lapply linear nplus_gen_succ_1 to H as H0.
  57  decompose.
  58  rewrite > H1. clear H1 r.
  59  auto.
  60 qed.
  61
  62 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
  63                         \forall q2,r2. (r1 + q2 == r2) \to
  64                         \exists q. (q1 + q2 == q) \land p + q == r2.
  65  intros 2; elim q1; clear q1; intros;
  66  [ lapply linear nplus_gen_zero_2 to H as H0.
  67    rewrite > H0. clear H0 p
  68  | lapply linear nplus_gen_succ_2 to H1 as H0.
  69    decompose.
  70    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
  71    lapply linear nplus_gen_succ_1 to H2 as H0.
  72    decompose.
  73    rewrite > H2. clear H2 r2.
  74    lapply linear H to H4, H3 as H0.
  75    decompose.
  76  ]; apply ex_intro; [| auto || auto ]. (**)
  77 qed.
  78
  79 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
  80                         \forall p2,r2. (p2 + r1 == r2) \to
  81                         \exists p. (p1 + p2 == p) \land p + q == r2.
  82  intros 2; elim q; clear q; intros;
  83  [ lapply linear nplus_gen_zero_2 to H as H0.
  84    rewrite > H0. clear H0 p1
  85  | lapply linear nplus_gen_succ_2 to H1 as H0.
  86    decompose.
  87    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
  88    lapply linear nplus_gen_succ_2 to H2 as H0.
  89    decompose.
  90    rewrite > H2. clear H2 r2.
  91    lapply linear H to H4, H3 as H0.
  92    decompose.
  93  ]; apply ex_intro; [| auto || auto ]. (**)
  94 qed.
  95
  96 theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
  97                      \forall r2. (p + q == r2) \to r1 = r2.
  98  intros 2. elim q; clear q; intros;
  99  [ lapply linear nplus_gen_zero_2 to H as H0.
 100    rewrite > H0 in H1. clear H0 p
 101  | lapply linear nplus_gen_succ_2 to H1 as H0.
 102    decompose.
 103    rewrite > H3. clear H3 r1.
 104    lapply linear nplus_gen_succ_2 to H2 as H0.
 105    decompose.
 106    rewrite > H2. clear H2 r2.
 107  ]; auto.
 108 qed.