Algebra

Alge.v

From Coq Require Export Bool.
From Coq Require Export PeanoNat.
From Coq Require Export Peano_dec.
From Coq Require Export List.

Module MyGroup.

  Section ClassDefns.

  Class Magma (G : Type) (plus : G -> G -> G) : Type :=
    { G_is_nonemtpy : G
    }
  .

  Class Semigroup (G : Type) (plus : G -> G -> G) `(is_magma : Magma G plus) : Type :=
    { has_associativity :
      forall a : G, forall b : G, forall c : G, plus a (plus b c) = plus (plus a b) c
    }
  .

  Class Monoid (G : Type) (plus : G -> G -> G) `(is_semigroup : Semigroup G plus) : Type :=
    { has_identity :
      { zero : G | forall a : G, plus zero a = a /\ plus a zero = a }
    }
  .

  Lemma zero_is_the_unique_identity (G : Type) (plus : G -> G -> G) `{is_monoid : Monoid G plus} :
    { zero : G | forall zero' : G, zero = zero' <-> forall a : G, plus zero' a = a /\ plus a zero' = a }.
  Proof.
    destruct is_monoid.
    destruct has_identity0 as [zero H].
    exists zero.
    intros zero'.
    constructor.
    - intro.
      subst.
      apply H.
    - intro.
      assert (plus zero zero' = zero).
        apply H0.
      assert (plus zero zero' = zero').
        apply H.
      rewrite <- H1.
      apply H2.
  Qed.

  Definition e {G : Type} {plus : G -> G -> G} `{is_monoid : Monoid G plus} : G :=
    proj1_sig (zero_is_the_unique_identity G plus)
  .

  Class Group (G : Type) (plus : G -> G -> G) `(is_monoid : Monoid G plus) : Type :=
    { has_inverse :
      forall a : G,
      { neg_a : G | plus neg_a a = e /\ plus a neg_a = e }
    }
  .

  Lemma neg_a_is_the_unique_inverse_of_a (G : Type) (plus : G -> G -> G) `{is_group : Group G plus} :
    forall a : G, { neg_a : G | forall neg_a' : G, neg_a = neg_a' <-> plus neg_a' a = e /\ plus a neg_a' = e }.
  Proof.
    destruct is_group.
    intros a.
    destruct (has_inverse0 a) as [neg_a H].
    exists neg_a.
    intros neg_a'.
    constructor.
    - intros.
      subst.
      apply H.
    - intros.
      destruct H.
      destruct H0.
      assert (plus neg_a e = neg_a).
        apply (proj2_sig (zero_is_the_unique_identity G plus)).
        reflexivity.
      assert (plus e neg_a' = neg_a').
        apply (proj2_sig (zero_is_the_unique_identity G plus)).
        reflexivity.
      rewrite <- H3.
      rewrite <- H4.
      cut (plus neg_a (plus a neg_a') = plus (plus neg_a a) neg_a').
        rewrite H.
        rewrite H2.
        tauto.
      apply has_associativity.
  Qed.

  Definition inv (G : Type) (plus : G -> G -> G) `{is_group : Group G plus} : G -> G :=
    fun a : G => proj1_sig (neg_a_is_the_unique_inverse_of_a G plus a)
  .

  Definition IsSubgroupOf (H : Type) (plus_H : H -> H -> H) (G : Type) (plus_G : G -> G -> G) `{G_is_group : Group G plus_G} : Type :=
    { monomorphism : H -> G | (forall x1 : H, forall x2 : H, monomorphism x1 = monomorphism x2 -> x1 = x2) /\ (forall x1 : H, forall x2: H, monomorphism (plus_H x1 x2) = plus_G (monomorphism x1) (monomorphism x2)) }
  .

  Lemma induce_subgroup_identity (H : Type) (plus_H : H -> H -> H) (G : Type) (plus_G : G -> G -> G) `{G_is_group : Group G plus_G} :
    IsSubgroupOf H plus_H G plus_G ->
    { zero_H : H | forall a : H, plus_H zero_H a = a /\ plus_H a zero_H = a }.
  Proof.
    admit.
  Qed.

  End ClassDefns.  

End MyGroup.

algebra.py

# algebra.py

def getAllPermutations(lst):
    def go(n):
        nonlocal lst
        res = []
        if n == 0:
            res += [lst[0:]]
        else:
            for i in range(n):
                lst[i], lst[n - 1] = lst[n - 1], lst[i]
                res += go(n - 1)
                lst[i], lst[n - 1] = lst[n - 1], lst[i]
        return res
    return go(len(lst))

def printAllPermutations(sz):
    transpositions = []
    lst = list(range(1, sz + 1))
    print("*", "Finding all permutations of", lst)
    def show_product_of_transpositions():
        nonlocal transpositions
        res = ""
        cnt = 0
        for (i, j) in transpositions:
            res = ("(" + str(i) + " " + str(j) + ")") + res
            cnt += 1
        if res == "":
            return "1", 1
        else:
            return res, - 2 * (cnt % 2) + 1
    def go(n):
        nonlocal transpositions, lst
        cnt_odd, cnt_even = 0, 0    
        if n == 0:
            prod, sgn = show_product_of_transpositions()
            print(">>>", lst, "=", prod, "where", "sgn", "=", sgn)
            if sgn < 0:
                cnt_odd  += 1
            elif sgn > 0:
                cnt_even += 1
        else:
            for i in reversed(range(n)):
                if i < n - 1:
                    transpositions = transpositions + [(lst[i], lst[n - 1]) if lst[i] < lst[n - 1] else (lst[n - 1], lst[i])]
                    lst[i], lst[n - 1] = lst[n - 1], lst[i]
                cnt_odd_1, cnt_even_1 = go(n - 1)
                cnt_odd  += cnt_odd_1
                cnt_even += cnt_even_1
                if i < n - 1:
                    transpositions.pop(-1)
                    lst[i], lst[n - 1] = lst[n - 1], lst[i]
        return cnt_odd, cnt_even
    cnt_odd, cnt_even = go(sz)
    print("-->", "cnt_odd ", "=", cnt_odd )
    print("-->", "cnt_even", "=", cnt_even)
    return None

if __name__ == '__main__':
    printAllPermutations(4)