matita/contribs/RELATIONAL/NPlus/monoid.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
  16
  17 include "NPlus/fun.ma".
  18
  19 (* Monoidal properties ******************************************************)
  20
  21 theorem nplus_zero_1: \forall q. zero + q == q.
  22  intros. elim q; clear q; autobatch.
  23 qed.
  24
  25 theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to
  26                       (succ p) + q == (succ r).
  27  intros. elim H; clear H q r; autobatch.
  28 qed.
  29
  30 theorem nplus_comm: \forall p, q, x. (p + q == x) \to
  31                     \forall y. (q + p == y) \to x = y.
  32  intros 4; elim H; clear H q x;
  33  [ lapply linear nplus_inv_zero_1 to H1
  34  | lapply linear nplus_inv_succ_1 to H3. decompose
  35  ]; destruct; autobatch.
  36 qed.
  37
  38 theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r.
  39  intros. elim H; clear H q r; autobatch.
  40 qed.
  41
  42 theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to
  43                    \forall p3, s1. (r1 + p3 == s1) \to
  44                    \forall r3. (p2 + p3 == r3) \to
  45                    \forall s3. (p1 + r3 == s3) \to s1 = s3.
  46  intros 4. elim H; clear H p2 r1;
  47  [ lapply linear nplus_inv_zero_1 to H2. destruct.
  48    lapply nplus_mono to H1, H3. destruct. autobatch
  49  | lapply linear nplus_inv_succ_1 to H3. decompose. destruct.
  50    lapply linear nplus_inv_succ_1 to H4. decompose. destruct.
  51    lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch
  52  ].
  53 qed.
  54
  55 (* Corollaries of functional properties **************************************)
  56
  57 theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to
  58                      \forall q2. (p + q2 == r) \to q1 = q2.
  59  intros. autobatch.
  60 qed.
  61
  62 (* Corollaries of nonoidal properties ***************************************)
  63
  64 theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to
  65                       \forall p2, r2. (p2 + q == r2) \to
  66                       \forall x. (p2 + r1 == x) \to
  67                       \forall y. (p1 + r2 == y) \to
  68                       x = y.
  69  intros 4. elim H; clear H q r1;
  70  [ lapply linear nplus_inv_zero_2 to H1
  71  | lapply linear nplus_inv_succ_2 to H3.
  72    lapply linear nplus_inv_succ_2 to H4. decompose. destruct.
  73    lapply linear nplus_inv_succ_2 to H5. decompose
  74  ]; destruct; autobatch.
  75 qed.
  76
  77 theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
  78                           \forall p2,r2. (p2 + q == r2) \to
  79                           \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
  80  intros 4. elim H; clear H q r1;
  81  [ lapply linear nplus_inv_zero_2 to H1. destruct
  82  | lapply linear nplus_inv_succ_2 to H3. decompose. destruct.
  83    lapply linear nplus_inv_succ_2 to H4. decompose. destruct
  84  ]; autobatch.
  85 qed.
  86
  87 (*
  88 theorem nplus_shift_succ_sx: \forall p,q,r.
  89                              (p + (succ q) == r) \to (succ p) + q == r.
  90  intros.
  91  lapply linear nplus_inv_succ_2 to H as H0.
  92  decompose. destruct. auto new timeout=100.
  93 qed.
  94
  95 theorem nplus_shift_succ_dx: \forall p,q,r.
  96                              ((succ p) + q == r) \to p + (succ q) == r.
  97  intros.
  98  lapply linear nplus_inv_succ_1 to H as H0.
  99  decompose. destruct. auto new timeout=100.
 100 qed.
 101
 102 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
 103                        \forall q2,r2. (r1 + q2 == r2) \to
 104                        \exists q. (q1 + q2 == q) \land p + q == r2.
 105  intros 2; elim q1; clear q1; intros;
 106  [ lapply linear nplus_inv_zero_2 to H as H0.
 107    destruct.
 108  | lapply linear nplus_inv_succ_2 to H1 as H0.
 109    decompose. destruct.
 110    lapply linear nplus_inv_succ_1 to H2 as H0.
 111    decompose. destruct.
 112    lapply linear H to H4, H3 as H0.
 113    decompose.
 114  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
 115 qed.
 116
 117 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
 118                        \forall p2,r2. (p2 + r1 == r2) \to
 119                        \exists p. (p1 + p2 == p) \land p + q == r2.
 120  intros 2; elim q; clear q; intros;
 121  [ lapply linear nplus_inv_zero_2 to H as H0.
 122    destruct
 123  | lapply linear nplus_inv_succ_2 to H1 as H0.
 124    decompose. destruct.
 125    lapply linear nplus_inv_succ_2 to H2 as H0.
 126    decompose. destruct.
 127    lapply linear H to H4, H3 as H0.
 128    decompose.
 129  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
 130 qed.
 131 *)