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
  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    rewrite > H1. clear H1 n2
  36  ]; apply ex_intro; [| auto || auto ]. (**)
  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
  42  | clear H H1.
  43    lapply eq_gen_zero_succ to H2 as H0. apply H0
  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. apply H0
  51  | clear H1 H3 r.
  52    lapply linear eq_gen_succ_succ to H2 as H0.
  53    rewrite > H0. clear H0 q.
  54    apply ex_intro; [| auto ] (**)
  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  [ rewrite < H1. clear H1 p.
  62    auto
  63  | clear H H1.
  64    lapply eq_gen_zero_succ to H3 as H0. apply H0
  65  ].
  66 qed.
  67
  68 theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  69                            \exists s. p = succ s \land (s + q == r) \lor
  70                                       q = succ s \land (p + s == r).
  71  intros. inversion H; clear H; intros;
  72  [ rewrite < H1. clear H1 p
  73  | clear H1.
  74    lapply linear eq_gen_succ_succ to H3 as H0.
  75    rewrite > H0. clear H0 r.
  76  ]; apply ex_intro; [| auto || auto ] (**)
  77 qed.
  78 (*
  79 (* alternative proofs invoking nplus_gen_2 *)
  80
  81 variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to
  82                                p = zero \land q = zero.
  83  intros 2. elim q; clear q; intros;
  84  [ lapply linear nplus_gen_zero_2 to H as H0.
  85    rewrite > H0. clear H0 p.
  86    auto
  87  | clear H.
  88    lapply linear nplus_gen_succ_2 to H1 as H0.
  89    decompose.
  90    lapply linear eq_gen_zero_succ to H1 as H0. apply H0
  91  ].
  92 qed.
  93
  94 variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
  95                                \exists s. p = succ s \land (s + q == r) \lor
  96                                           q = succ s \land (p + s == r).
  97  intros 2. elim q; clear q; intros;
  98  [ lapply linear nplus_gen_zero_2 to H as H0.
  99    rewrite > H0. clear H0 p
 100  | clear H.
 101    lapply linear nplus_gen_succ_2 to H1 as H0.
 102    decompose.
 103    lapply linear eq_gen_succ_succ to H1 as H0.
 104    rewrite > H0. clear H0 r.
 105  ]; apply ex_intro; [| auto || auto ]. (**)
 106 qed.
 107 *)
 108 (* other simplification lemmas *)
 109
 110 theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
 111  intros 2. elim q; clear q; intros;
 112  [ lapply linear nplus_gen_zero_2 to H as H0.
 113    rewrite > H0. clear H0 p
 114  | lapply linear nplus_gen_succ_2 to H1 as H0.
 115    decompose.
 116    lapply linear eq_gen_succ_succ to H2 as H0.
 117    rewrite < H0 in H3. clear H0 a
 118  ]; auto.
 119 qed.
 120
 121 theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
 122  intros 1. elim p; clear p; intros;
 123  [ lapply linear nplus_gen_zero_1 to H as H0.
 124    rewrite > H0. clear H0 q
 125  | lapply linear nplus_gen_succ_1 to H1 as H0.
 126    decompose.
 127    lapply linear eq_gen_succ_succ to H2 as H0.
 128    rewrite < H0 in H3. clear H0 a
 129  ]; auto.
 130 qed.