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; auto.
  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;
  35  [ auto.
  36  | clear H H1. destruct H2.
  37  ].
  38 qed.
  39
  40 theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to
  41                           \exists s. r = (succ s) \land p + q == s.
  42  intros. inversion H; clear H; intros;
  43  [ destruct H.
  44  | clear H1 H3 r. destruct H2; clear H2. subst. auto depth = 4.
  45  ].
  46 qed.
  47
  48 theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to
  49                           p = zero \land q = zero.
  50  intros. inversion H; clear H; intros;
  51  [ subst. auto
  52  | clear H H1. destruct H3.
  53  ].
  54 qed.
  55
  56 theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  57                           \exists s. p = succ s \land (s + q == r) \lor
  58                                      q = succ s \land p + s == r.
  59  intros. inversion H; clear H; intros;
  60  [ subst
  61  | clear H1. destruct H3. clear H3. subst.
  62  ]; auto depth = 4.
  63 qed.
  64
  65 (* Corollaries to inversion lemmas ******************************************)
  66
  67 theorem nplus_inv_succ_2_3: \forall p,q,r.
  68                             (p + (succ q) == (succ r)) \to p + q == r.
  69  intros.
  70  lapply linear nplus_inv_succ_2 to H. decompose. subst.
  71  destruct H1. clear H1. subst. auto.
  72 qed.
  73
  74 theorem nplus_inv_succ_1_3: \forall p,q,r.
  75                             ((succ p) + q == (succ r)) \to p + q == r.
  76  intros.
  77  lapply linear nplus_inv_succ_1 to H. decompose. subst.
  78  destruct H1. clear H1. subst. auto.
  79 qed.
  80
  81 theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  82  intros 2. elim q; clear q;
  83  [ lapply linear nplus_inv_zero_2 to H
  84  | lapply linear nplus_inv_succ_2_3 to H1
  85  ]; auto.
  86 qed.
  87
  88 theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  89  intros 1. elim p; clear p;
  90  [ lapply linear nplus_inv_zero_1 to H
  91  | lapply linear nplus_inv_succ_1_3 to H1.
  92  ]; auto.
  93 qed.