helm/software/matita/nlibrary/nat/plus.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 include "nat/big_ops.ma".
  16 include "algebra/unital_magmas.ma".
  17 include "algebra/abelian_magmas.ma".
  18
  19 nlet rec plus (n:nat) (m:nat) on n : nat ≝
  20  match n with
  21   [ O ⇒ m
  22   | S n' ⇒ S (plus n' m) ].
  23
  24 ndefinition plus_magma_type: magma_type.
  25  napply mk_magma_type
  26   [ napply NAT
  27   | napply mk_binary_morphism
  28      [ napply plus
  29      | #a; #a'; #b; #b'; #Ha; #Hb; nrewrite < Ha; nrewrite < Hb; napply refl ]##]
  30 nqed.
  31
  32 ndefinition plus_abelian_magma_type: abelian_magma_type.
  33  napply mk_abelian_magma_type
  34   [ napply plus_magma_type
  35   | nnormalize; #x;
  36      (* nelim non va *) napply (nat_rect_CProp0 ??? x);
  37      ##[ #y; napply (nat_rect_CProp0 ??? y) [ napply refl | #n; #H; nnormalize; nrewrite < H; napply refl]
  38      ##| #n; #H; #y; nnormalize;
  39          (* rewrite qui non va *)
  40          napply (eq_rect_CProp0_r ????? (H y));
  41          napply (nat_rect_CProp0 ??? y)
  42           [ napply refl
  43           | #n0; #K; nnormalize in K; nnormalize;
  44             napply (eq_rect_CProp0 ????? K); napply refl] ##]
  45 nqed.
  46
  47 ndefinition plus_unital_magma_type: unital_magma_type.
  48  napply mk_unital_magma_type
  49   [ napply plus_magma_type
  50   | napply O
  51   | #x; napply refl
  52   | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
  53 nqed.
  54
  55 ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.