graph.v

Definition associative {A:Type} (op: A -> A -> A) :=
  forall x y z, op x (op y z) = op (op x y) z.

Definition commutative {A:Type} (op: A -> A -> A) :=
  forall x y, op x y = op y x.

Definition is_unit_left {A:Type} (op: A -> A -> A) one :=
  forall x, op one x = x.

Definition is_unit_right {A:Type} (op: A -> A -> A) one :=
  forall x, op x one = x.

Definition distributive {A:Type} (mul: A -> A -> A) (plus: A -> A -> A) :=
  forall x y z, mul x (plus y z) = plus (mul x y) (mul x z).


Class GraphAlgebra {A:Type} : Type :=
  {
    plus : A -> A -> A;
    plus_comm: commutative plus;
    plus_assoc: associative plus;
    mul: A -> A -> A;
    mul_assoc: associative mul;
    one: A;
    mul_unit_left: is_unit_left mul one;
    mul_unit_right: is_unit_right mul one;
    mul_plus_distr: distributive mul plus;
    decomposition: forall a b c, mul (mul a b) c = plus (plus (mul a b) (mul b c)) (mul a c);
  }.

Parameter A:Type.
Parameter G:@GraphAlgebra A.

  
Notation "x + y" := (plus x y).
Notation "x * y" := (mul x y).

Notation "1" := one.
Notation "2" := (1 + 1).
Notation "3" := (2+1).
Notation "4" := (2+2).

Check decomposition.

Require Import Coq.Setoids.Setoid.

Lemma double: forall a, a + a = a*2.
Proof.
  intro.
  replace (a+a) with (a*1 + a*1) by (now rewrite mul_unit_right). 
  now replace (a*1 + a*1) with (a*2) by (now rewrite mul_plus_distr).
Qed.

Lemma ident1: forall a, a = a*2 + 1.
Proof.
  intro.
  replace a with (1*a*1) at 1 by (rewrite mul_unit_left; now rewrite mul_unit_right).
  rewrite (decomposition 1 a 1).
  repeat rewrite mul_unit_right.
  rewrite mul_unit_left.
  now rewrite double.
Qed.

Lemma three_one: 3 = 1.
Proof.
  rewrite (ident1 1) at 4.
  now rewrite mul_unit_left.
Qed.

Lemma ident2: forall a, a*2 = a + 1.
Proof.
  intro.
  assert (H: forall b, a + b = (a *2 + 1) + b).
  intro. now rewrite (ident1 a) at 1.
  rewrite <- double.
  rewrite (H a).
  rewrite <- plus_assoc.
  replace (1+a) with (a+1) by (apply plus_comm).
  rewrite plus_assoc.
  replace a with (a*1) at 2 by (apply mul_unit_right).
  replace (a*2 + a*1) with (a*3) by (apply mul_plus_distr).
  rewrite three_one.
  now rewrite mul_unit_right.
Qed.

Lemma two_by_two: 2*2 = 4.
Proof.
  rewrite mul_plus_distr. now rewrite mul_unit_right.
Qed.

Lemma four_one: 4 = 1.
  pose (e:=ident2 2).
  rewrite two_by_two in e.
  rewrite e.
  apply three_one.
Qed.

Lemma two_unit: forall a, a = a + 2.
Proof.
  intro a.
  rewrite (ident1 a) at 1.
  rewrite (ident2 a).
  now rewrite plus_assoc.
Qed.

Theorem one_plus_unit: forall a, a = a + 1.
Proof.
  intro a.
  rewrite two_unit at 1.
  rewrite two_unit at 1.
  replace (a + 2 + 2) with (a + (2+2)) by (now rewrite plus_assoc).
  now rewrite four_one.
Qed.

Theorem plus_idempotent: forall a, a = a + a.
Proof.
  intro a.
  rewrite double.
  rewrite  ident2.
  now rewrite <- one_plus_unit.
Qed.

Formalization of the algebra described in "an algebra of graphs" blog post.