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 (* primitive generation lemmas proved by elimination and inversion *)
  20
  21 theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r.
  22  intros. elim H; clear H q r; intros;
  23  [ reflexivity
  24  | clear H1. auto new timeout=30
  25  ].
  26 qed.
  27
  28 theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to
  29                           \exists s. r = (succ s) \land p + q == s.
  30  intros. elim H; clear H q r; intros;
  31  [
  32  | clear H1.
  33    decompose.
  34    subst.
  35  ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**)
  36 qed.
  37
  38 theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  39  intros. inversion H; clear H; intros;
  40  [ auto new timeout=30
  41  | clear H H1.
  42    destruct H2.
  43  ].
  44 qed.
  45
  46 theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to
  47                           \exists s. r = (succ s) \land p + q == s.
  48  intros. inversion H; clear H; intros;
  49  [ destruct H.
  50  | clear H1 H3 r.
  51    destruct H2; clear H2.
  52    subst.
  53    apply ex_intro; [| auto new timeout=30 ] (**)
  54  ].
  55 qed.
  56
  57 theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to
  58                           p = zero \land q = zero.
  59  intros. inversion H; clear H; intros;
  60  [ subst. auto new timeout=30
  61  | clear H H1.
  62    destruct H3.
  63  ].
  64 qed.
  65
  66 theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  67                           \exists s. p = succ s \land (s + q == r) \lor
  68                                      q = succ s \land p + s == r.
  69  intros. inversion H; clear H; intros;
  70  [ subst.
  71  | clear H1.
  72    destruct H3. clear H3.
  73    subst.
  74  ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**)
  75 qed.
  76 (*
  77 (* alternative proofs invoking nplus_gen_2 *)
  78
  79 variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to
  80                               p = zero \land q = zero.
  81  intros 2. elim q; clear q; intros;
  82  [ lapply linear nplus_gen_zero_2 to H as H0.
  83    subst. auto new timeout=30
  84  | clear H.
  85    lapply linear nplus_gen_succ_2 to H1 as H0.
  86    decompose.
  87    lapply linear eq_gen_zero_succ to H1 as H0. apply H0
  88  ].
  89 qed.
  90
  91 variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
  92                               \exists s. p = succ s \land (s + q == r) \lor
  93                                          q = succ s \land p + s == r.
  94  intros 2. elim q; clear q; intros;
  95  [ lapply linear nplus_gen_zero_2 to H as H0.
  96    subst
  97  | clear H.
  98    lapply linear nplus_gen_succ_2 to H1 as H0.
  99    decompose.
 100    lapply linear eq_gen_succ_succ to H1 as H0.
 101    subst
 102  ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**)
 103 qed.
 104 *)
 105 (* other simplification lemmas *)
 106
 107 theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
 108  intros 2. elim q; clear q; intros;
 109  [ lapply linear nplus_gen_zero_2 to H as H0.
 110    subst
 111  | lapply linear nplus_gen_succ_2 to H1 as H0.
 112    decompose.
 113    destruct H2. clear H2.
 114    subst
 115  ]; auto new timeout=30.
 116 qed.
 117
 118 theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
 119  intros 1. elim p; clear p; intros;
 120  [ lapply linear nplus_gen_zero_1 to H as H0.
 121    subst
 122  | lapply linear nplus_gen_succ_1 to H1 as H0.
 123    decompose.
 124    destruct H2. clear H2.
 125    subst
 126  ]; auto new timeout=30.
 127 qed.