Require Export AAC.

Module Peano.
  Require Import Arith NArith Max.
  Program Instance aac_plus : @Op_AC nat eq plus 0 := @Build_Op_AC nat (@eq nat) plus 0 _ plus_0_l plus_assoc plus_comm.

  Program Instance aac_mult : Op_AC eq mult 1 := Build_Op_AC _ _ _ mult_assoc mult_comm.
  Definition default_a := AC_A aac_plus. Existing Instance default_a.
End Peano.

Module Z.
  Require Import ZArith.
  Open Scope Z_scope.
  Program Instance aac_plus : Op_AC eq Zplus 0 := Build_Op_AC _ _ _ Zplus_assoc Zplus_comm.
  Program Instance aac_mult : Op_AC eq Zmult 1 := Build_Op_AC _ _ Zmult_1_l Zmult_assoc Zmult_comm.
  Definition default_a := AC_A aac_plus. Existing Instance default_a.
End Z.

Module Q.
  Require Import QArith.
  Program Instance aac_plus : Op_AC Qeq Qplus 0 := Build_Op_AC _ _ Qplus_0_l Qplus_assoc Qplus_comm.
  Program Instance aac_mult : Op_AC Qeq Qmult 1 := Build_Op_AC _ _ Qmult_1_l Qmult_assoc Qmult_comm.
  Definition default_a := AC_A aac_plus. Existing Instance default_a.
End Q.

Module Prop_ops.
  Program Instance aac_or : Op_AC iff or False. Solve All Obligations using tauto.

  Program Instance aac_and : Op_AC iff and True. Solve All Obligations using tauto.

  Definition default_a := AC_A aac_and. Existing Instance default_a.

  Program Instance aac_not_compat : Proper (iff ==> iff) not.
  Solve All Obligations using firstorder.
End Prop_ops.

Module Bool.
  Program Instance aac_orb : Op_AC eq orb false.
  Solve All Obligations using firstorder.

  Program Instance aac_andb : Op_AC eq andb true.
  Solve All Obligations using firstorder.

  Definition default_a := AC_A aac_andb. Existing Instance default_a.

  Instance negb_compat : Proper (eq ==> eq) negb.
  Proof. intros [|] [|]; auto. Qed.
End Bool.

Module Relations.
  Require Import Relations.
  Section defs.
    Variable T : Type.
    Variables R S: relation T.
    Definition inter : relation T := fun x y => R x y /\ S x y.
    Definition compo : relation T := fun x y => exists z : T, R x z /\ S z y.
    Definition negr : relation T := fun x y => ~ R x y.

    Definition bot : relation T := fun _ _ => False.
    Definition top : relation T := fun _ _ => True.
  End defs.

  Program Instance aac_union T : Op_AC (same_relation T) (union T) (bot T).
  Solve All Obligations using compute; [tauto || intuition].

  Program Instance aac_inter T : Op_AC (same_relation T) (inter T) (top T).
  Solve All Obligations using compute; firstorder.

  Program Instance aac_compo T : Op_A (same_relation T) (compo T) eq.
  Solve All Obligations using compute; firstorder.
  Solve All Obligations using compute; firstorder subst; trivial.

  Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T).
  Proof. compute. firstorder. Qed.

  Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T).
  Proof. compute. firstorder. Qed.

  Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T).
  Proof.
    intros R S H x y Hxy. induction Hxy.
      constructor 1. apply H. assumption.
      econstructor 2; eauto 3.
  Qed.
  Instance clos_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_trans T).
  Proof. intros R S H; split; apply clos_trans_incr, H. Qed.

  Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T).
  Proof.
    intros R S H x y Hxy. induction Hxy.
      constructor 1. apply H. assumption.
      constructor 2.
      econstructor 3; eauto 3.
  Qed.
  Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T).
  Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed.

End Relations.

Module All.
  Export Peano.
  Export Z.
  Export Prop_ops.
  Export Bool.
  Export Relations.
End All.