matita/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
  16
  17 include "NPlus/defs.ma".
  18
  19 (* Inversion lemmas *********************************************************)
  20
  21 theorem nplus_inv_zero_1: ∀q,r. zero ⊕ q ≍ r → q = r.
  22  intros. elim H; clear H q r; autobatch.
  23 qed.
  24
  25 theorem nplus_inv_succ_1: ∀p,q,r. succ p ⊕ q ≍ r →
  26                           ∃s. r = succ s ∧ p ⊕ q ≍ s.
  27  intros. elim H; clear H q r; intros;
  28  [ autobatch depth = 3
  29  | clear H1; decompose; destruct; autobatch depth = 4
  30  ]
  31 qed.
  32
  33 theorem nplus_inv_zero_2: ∀p,r. p ⊕ zero ≍ r → p = r.
  34  intros; inversion H; clear H; intros; destruct; autobatch.
  35 qed.
  36
  37 theorem nplus_inv_succ_2: ∀p,q,r. p ⊕ succ q ≍ r →
  38                           ∃s. r = succ s ∧ p ⊕ q ≍ s.
  39  intros; inversion H; clear H; intros; destruct.
  40  autobatch depth = 3.
  41 qed.
  42
  43 theorem nplus_inv_zero_3: ∀p,q. p ⊕ q ≍ zero →
  44                           p = zero ∧ q = zero.
  45  intros; inversion H; clear H; intros; destruct; autobatch.
  46 qed.
  47
  48 theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r →
  49                              ∃s. p = succ s ∧ s ⊕ q ≍ r ∨
  50                                q = succ s ∧ p ⊕ s ≍ r.
  51  intros; inversion H; clear H; intros; destruct;
  52  autobatch depth = 4.
  53 qed.
  54
  55 (* Corollaries to inversion lemmas ******************************************)
  56
  57 theorem nplus_inv_succ_2_3: ∀p,q,r.
  58                             p ⊕ succ q ≍ succ r → p ⊕ q ≍ r.
  59  intros;
  60  lapply linear nplus_inv_succ_2 to H; decompose; destruct; autobatch.
  61 qed.
  62
  63 theorem nplus_inv_succ_1_3: ∀p,q,r.
  64                             succ p ⊕ q ≍ succ r → p ⊕ q ≍ r.
  65  intros;
  66  lapply linear nplus_inv_succ_1 to H; decompose; destruct; autobatch.
  67 qed.
  68
  69 theorem nplus_inv_eq_2_3: ∀p,q. p ⊕ q ≍ q → 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: ∀p,q. p ⊕ q ≍ p → 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.