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