Section RewriteDemo.

Hypothesis A:Set.
Hypothesis unit:A.
Hypothesis mul:A -> A -> A.

Infix "&" := mul (at level 40).

Definition e:= unit:A.

(* Axioms for a monoid *)

Hypothesis unitl: (forall x:A, e & x = x).
Hypothesis unitr: (forall x:A, x & e = x).
Hypothesis assoc: (forall x y z:A, (x & y) & z = x & (y & z)).

Hint Rewrite unitl unitr assoc: monoid_rules.

Theorem semigr_eq1: 
(forall x y:A,  (x & y) & (e & x) = x & (y & x)).
intros.
autorewrite with monoid_rules.
trivial.
Qed.

(* Extend with group axioms *)

Hypothesis iv: A -> A.

Hypothesis invl: (forall x:A, (iv x) & x = e).
Hypothesis invr: (forall x:A, x & (iv x) = e).

Hint Rewrite unitl unitr assoc invl invr: group_rules.


Theorem inv_inv:
(forall y:A, (iv (iv y)) = y).
intros.
autorewrite with group_rules.

(* Did not work. Try by hand. *)

rewrite <- unitr.
rewrite <- invr with (x:= (iv y)).
rewrite <- assoc.
rewrite invr.  (* default direction of rewrite is -> *)
rewrite unitl.
trivial.
Qed.

(* Exercise Prove  (a1) - (a4)  as theorems *)
Hypothesis a1: (forall x y:A, (iv x) & (x & y) = y).
Hypothesis a2: (iv e) = e.
Hypothesis a3: (forall x y:A, y & ((iv y) & x) = x).
Hypothesis a4: (forall x y:A, (iv (x & y)) = (iv y) & (iv x)).

(* The following set of rewrite rules form a complete
TRS for the equational theory of groups. See 
J W Klop: Term rewriting systems in Handbook of Logic
in Computer Science, vol 2, p 49. *)

Hint Rewrite unitl unitr assoc invl invr inv_inv 
a1 a2 a3 a4: extended_group_rules.

Theorem grpthm1 : (forall x y z :A,
x & (iv (y & (z &  x))) & y & z = e).
intros.
autorewrite with extended_group_rules.
trivial.
Qed.