matita/contribs/RELATIONAL/NPlus/inv.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/inv".
  16
  17 include "NPlus/defs.ma".
  18
  19 (* Inversion lemmas *********************************************************)
  20
  21 theorem nplus_inv_zero_1: \forall q,r. (zero + q == r) \to q = r.
  22  intros. elim H; clear H q r; autobatch.
  23 qed.
  24
  25 theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to
  26                           \exists s. r = (succ s) \land p + q == s.
  27  intros. elim H; clear H q r; intros;
  28  [ autobatch depth = 4
  29  | clear H1. decompose. subst. autobatch depth = 4
  30  ]
  31 qed.
  32
  33 theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r.
  34  intros. inversion H; clear H; intros; subst. autobatch.
  35 qed.
  36
  37 theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to
  38                           \exists s. r = (succ s) \land p + q == s.
  39  intros. inversion H; clear H; intros; subst.
  40  autobatch depth = 4.
  41 qed.
  42
  43 theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to
  44                           p = zero \land q = zero.
  45  intros. inversion H; clear H; intros; subst. autobatch.
  46 qed.
  47
  48 theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  49                           \exists s. p = succ s \land (s + q == r) \lor
  50                                      q = succ s \land p + s == r.
  51  intros. inversion H; clear H; intros; subst;
  52  autobatch depth = 4.
  53 qed.
  54
  55 (* Corollaries to inversion lemmas ******************************************)
  56
  57 theorem nplus_inv_succ_2_3: \forall p,q,r.
  58                             (p + (succ q) == (succ r)) \to p + q == r.
  59  intros.
  60  lapply linear nplus_inv_succ_2 to H. decompose. subst. autobatch.
  61 qed.
  62
  63 theorem nplus_inv_succ_1_3: \forall p,q,r.
  64                             ((succ p) + q == (succ r)) \to p + q == r.
  65  intros.
  66  lapply linear nplus_inv_succ_1 to H. decompose. subst. autobatch.
  67 qed.
  68
  69 theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  70  intros 2. elim q; clear q;
  71  [ lapply linear nplus_inv_zero_2 to H
  72  | lapply linear nplus_inv_succ_2_3 to H1
  73  ]; autobatch.
  74 qed.
  75
  76 theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  77  intros 1. elim p; clear p;
  78  [ lapply linear nplus_inv_zero_1 to H
  79  | lapply linear nplus_inv_succ_1_3 to H1.
  80  ]; autobatch.
  81 qed.