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/inv.ma".
  18
  19 theorem nplus_zero_1: \forall q. zero + q == q.
  20  intros. elim q; clear q; auto new timeout=100.
  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    subst
  28  | lapply linear nplus_gen_succ_2 to H1 as H0.
  29    decompose.
  30    subst
  31  ]; auto new timeout=100.
  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    subst
  38  | lapply linear nplus_gen_succ_2 to H1 as H0.
  39    decompose.
  40    subst
  41  ]; auto new timeout=100.
  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. subst. auto new timeout=100.
  49 qed.
  50
  51 theorem nplus_shift_succ_dx: \forall p,q,r.
  52                              ((succ p) + q == r) \to p + (succ q) == r.
  53  intros.
  54  lapply linear nplus_gen_succ_1 to H as H0.
  55  decompose. subst. auto new timeout=100.
  56 qed.
  57
  58 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
  59                        \forall q2,r2. (r1 + q2 == r2) \to
  60                        \exists q. (q1 + q2 == q) \land p + q == r2.
  61  intros 2; elim q1; clear q1; intros;
  62  [ lapply linear nplus_gen_zero_2 to H as H0.
  63    subst.
  64  | lapply linear nplus_gen_succ_2 to H1 as H0.
  65    decompose. subst.
  66    lapply linear nplus_gen_succ_1 to H2 as H0.
  67    decompose. subst.
  68    lapply linear H to H4, H3 as H0.
  69    decompose.
  70  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
  71 qed.
  72
  73 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
  74                        \forall p2,r2. (p2 + r1 == r2) \to
  75                        \exists p. (p1 + p2 == p) \land p + q == r2.
  76  intros 2; elim q; clear q; intros;
  77  [ lapply linear nplus_gen_zero_2 to H as H0.
  78    subst
  79  | lapply linear nplus_gen_succ_2 to H1 as H0.
  80    decompose. subst.
  81    lapply linear nplus_gen_succ_2 to H2 as H0.
  82    decompose. subst.
  83    lapply linear H to H4, H3 as H0.
  84    decompose.
  85  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
  86 qed.
  87
  88 theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
  89                     \forall r2. (p + q == r2) \to r1 = r2.
  90  intros 2. elim q; clear q; intros;
  91  [ lapply linear nplus_gen_zero_2 to H as H0.
  92    subst
  93  | lapply linear nplus_gen_succ_2 to H1 as H0.
  94    decompose. subst.
  95    lapply linear nplus_gen_succ_2 to H2 as H0.
  96    decompose. subst.
  97  ]; auto new timeout=100.
  98 qed.