Library additions.Monoid_instances

Some useful instances of Monoid classes

File

Require Export Monoid_def.
Require Import RelationClasses Morphisms.

Require Import ZArith PArith.
Require Import Arith.
Require Import NArith.
Require Import Ring63.

Open Scope Z_scope.

Multiplicative monoid on Z

#[ global ] Instance Z_mult_op : Mult_op Z := Z.mul.

#[ global ] Instance ZMult : Monoid Z_mult_op 1.
#[ global ] Instance ZMult_Abelian : Abelian_Monoid ZMult.

Multiplicative monoid on nat

#[ global ] Instance nat_mult_op : Mult_op nat | 5 := Nat.mul.

#[ global ] Instance Natmult : Monoid nat_mult_op 1%nat | 5.

Additive monoid on nat

The following monoid is useful for proving the correctness of complex exponentiation algorithms. In effect, the -th "power" of is equal to . See Sect.

#[ global ] Instance nat_plus_op : Mult_op nat | 12 := Nat.add.

#[ global ] Instance Natplus : Monoid nat_plus_op 0%nat | 12.

Open Scope N_scope.

#[ global ] Instance N_mult_op : Mult_op N | 5 := N.mul.

#[ global ] Instance NMult : Monoid N_mult_op 1 | 5.

Check NMult : EMonoid N.mul 1%N eq.

#[ global ] Instance N_plus_op : Mult_op N | 12 := N.add.

#[ global ] Instance NPlus : Monoid N_plus_op 0 | 12.

Multiplicative Monoid on positive

#[ global ] Instance P_mult_op : Mult_op positive | 5 := Pos.mul .

#[ global ] Instance PMult : Monoid P_mult_op xH | 5.

Import Uint63.
Open Scope int63_scope.

Multiplicative monoid on 63-bits integers

Cyclic numeric types are good candidates for testing exponentiations with big exponents, since the size of data is bounded.

The type int63 is defined in Standard Library in Module Coq.Numbers.Cyclic.Int63.Uint63.

#[ global ] Instance int63_mult_op : Mult_op int := mul.

#[ global ] Instance Int63mult : Monoid int63_mult_op 1.

Module Bad.

  Fixpoint int63_from_nat (n:nat) :int :=
    match n with
    | O ⇒ 1
    | S p ⇒ 1 + int63_from_nat p
    end.

  Coercion int63_from_nat : nat >-> int.

  Fixpoint fact (n:nat) : int := match n with
                             O ⇒ 1
                           | S p ⇒ n × fact p
                           end.

End Bad.

Close Scope int63_scope.

Monoid of 2x2 matrices

Let be some type, provided with a ring structure. We define the multiplication of -matrices, the coefficients of which have type .

Section M2_def.
Variables (A:Type)
           (zero one : A)
           (plus mult : A → A → A).

Notation "0" := zero.
Notation "1" := one.
Notation "x + y" := (plus x y).
Notation "x * y " := (mult x y).

Variable rt : semi_ring_theory zero one plus mult (@eq A).
Add Ring Aring : rt.

Structure M2 : Type := {c00 : A; c01 : A;
                        c10 : A; c11 : A}.

Definition Id2 : M2 := Build_M2 1 0 0 1.

Definition M2_mult (m m':M2) : M2 :=
Build_M2 (c00 m × c00 m' + c01 m × c10 m')
          (c00 m × c01 m' + c01 m × c11 m')
          (c10 m × c00 m' + c11 m × c10 m')
          (c10 m × c01 m' + c11 m × c11 m').

Lemma M2_eq_intros : ∀ a b c d a' b' c' d',
  a =a' → b =b' → c =c' → d =d' →
   Build_M2 a b c d = Build_M2 a' b' c' d'.

#[global] Instance M2_op : Mult_op M2 := M2_mult.

#[global] Instance M2_Monoid : Monoid M2_op Id2.

End M2_def.

Arguments M2_Monoid {A zero one plus mult} rt.
Arguments Build_M2 {A} _ _ _ _.

Matrices over N

Definition M2N := M2_Monoid Nth.

Integers modulo m

The following instance of EMonoid describes the set of integers modulo , where is some integer greater or equal than . For simplicity's sake, we represent such values using the type N, and consider "equivalence modulo " instead of equality.

Section Nmodulo.
  Variable m : N.
  Hypothesis m_gt_1 : 1 < m.

  Remark m_neq_0 : m ≠ 0.

  #[local] Hint Resolve m_neq_0 : chains.

  Definition mult_mod (x y : N) := (x × y ) mod m.
  Definition mod_eq (x y: N) := x mod m = y mod m.

  Instance mod_equiv : Equiv N := mod_eq.

  Instance mod_op : Mult_op N := mult_mod.

  Instance mod_Equiv : Equivalence mod_equiv.

  #[global] Instance mult_mod_proper :
    Proper (mod_equiv ==> mod_equiv ==> mod_equiv) mod_op.

  #[local] Open Scope M_scope.

  Lemma mult_mod_associative : ∀ x y z,
      x × (y × z ) = x × y × z.

  Lemma one_mod_neutral_l : ∀ x, 1 × x == x.
  Lemma one_mod_neutral_r : ∀ x, x × 1 == x.

  #[global] Instance Nmod_Monoid : EMonoid mod_op 1 mod_equiv.

End Nmodulo.

Section S256.

  Let mod256 := mod_op 256.

  #[local] Existing Instance mod256 | 1.

End S256.

Close Scope N_scope.
Close Scope positive_scope.