helm/software/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  [ auto depth = 4
  29  | clear H1. decompose. subst. auto 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. auto depth = 4.
  40 qed.
  41
  42 theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to
  43                           p = zero \land q = zero.
  44  intros. inversion H; clear H; intros; subst. autobatch.
  45 qed.
  46
  47 theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  48                           \exists s. p = succ s \land (s + q == r) \lor
  49                                      q = succ s \land p + s == r.
  50  intros. inversion H; clear H; intros; subst; auto depth = 4.
  51 qed.
  52
  53 (* Corollaries to inversion lemmas ******************************************)
  54
  55 theorem nplus_inv_succ_2_3: \forall p,q,r.
  56                             (p + (succ q) == (succ r)) \to p + q == r.
  57  intros.
  58  lapply linear nplus_inv_succ_2 to H. decompose. subst. autobatch.
  59 qed.
  60
  61 theorem nplus_inv_succ_1_3: \forall p,q,r.
  62                             ((succ p) + q == (succ r)) \to p + q == r.
  63  intros.
  64  lapply linear nplus_inv_succ_1 to H. decompose. subst. autobatch.
  65 qed.
  66
  67 theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  68  intros 2. elim q; clear q;
  69  [ lapply linear nplus_inv_zero_2 to H
  70  | lapply linear nplus_inv_succ_2_3 to H1
  71  ]; autobatch.
  72 qed.
  73
  74 theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  75  intros 1. elim p; clear p;
  76  [ lapply linear nplus_inv_zero_1 to H
  77  | lapply linear nplus_inv_succ_1_3 to H1.
  78  ]; autobatch.
  79 qed.