Require Import ATBR.

Set Implicit Arguments.
Unset Strict Implicit.

Section Props1.

  Context `{KA: KleeneAlgebra}.

  Theorem SemiConfluence_is_WeakConfluence A:
    ∀ (a b : X A A), b × a# <== a# × b# ↔ b# × a# <== a# × b#.
  Proof.
    intros a b; split.
     apply wsemicomm_iter_left.
     intro H. rewrite <- H. kleene_reflexivity.
  Qed.

  Theorem SemiConfluence_is_ChurchRosser A:
    ∀ (a b : X A A), b × a# <== a# × b# ↔ (a+b)# <== a# × b#.
  Proof.
    intros a b; split; intro H.
     star_left_induction.
     semiring_normalize.
     rewrite H. kleene_reflexivity.

     rewrite <- H. kleene_reflexivity.
  Qed.

  Theorem WeakConfluence_is_ChurchRosser A:
    ∀ (a b : X A A), b# × a# <== a# × b# ↔ (a+b)# <== a# × b#.
  Proof.
    intros a b; split; intro H.
     star_left_induction.
     semiring_normalize.
     rewrite (a_leq_star_a b) at 2.
     rewrite H. kleene_reflexivity.

     rewrite <- H. kleene_reflexivity.
  Qed.

  Theorem BubbleSort A:
    ∀ (a b : X A A), b × a <== a × b → (a+b)# <== a# × b#.
  Proof.
    intros a b; intro H.
     star_left_induction.
     semiring_normalize.
     apply semicomm_iter_left, semicomm_iter_right in H.
     rewrite (a_leq_star_a b) at 2.
     rewrite H. kleene_reflexivity.
  Qed.

  Notation "a ^+" := (a × a#) (at level 15).

  Theorem WeakConfluence_is_ChurchRosser_plus A:
    ∀ (a b : X A A), b^+ × a# <== a# × b^+ + a^+ × b# ↔ (a+b)^+ <== a# × b^+ + a^+ × b#.
  Proof.
    intros a b; split; intro H.
     star_right_induction.
     rewrite (a_leq_star_a a) at 5.
     rewrite <- (star_make_right b) at 2.
     semiring_normalize.
     monoid_rewrite H.
     unfold leq. kleene_reflexivity.

     rewrite <- H. kleene_reflexivity.
  Qed.

  Lemma star_plus_one A: ∀ (a: X A A), a# == (a+1)#.
  Proof. intros. kleene_reflexivity. Qed.

  Lemma star_plus_star A: ∀ (a b: X A A), (a+b)# == (a#+b#)#.
  Proof. intros. kleene_reflexivity. Qed.

  Theorem Hindley_Rosen A: ∀ (a b : X A A),
    b×a <== a#*(b+1) → b#×a# <== a#×b#.
  Proof.
    intros.
    do 2 rewrite (star_plus_one b) at 1.
    apply semicomm_iter_left.
    rewrite <- (star_idem a) at 2.
    apply semicomm_iter_right.
    semiring_normalize.
    rewrite H. kleene_reflexivity.
  Qed.

  Theorem Hindley_Rosen_union A: ∀ (a b c : X A A),
    c#×a# <== a#×c# →
    c#×b# <== b#×c# →
    c#×(a+b)# <== (a+b)#×c#.
  Proof.
    intros a b c Ha Hb.
    do 2 rewrite (star_plus_star a b) at 1.
    apply semicomm_iter_right.
    semiring_normalize. auto with compat.
  Qed.

End Props1.

Section Props2.

  Context `{KA: ConverseKleeneAlgebra}.

  Theorem Hindley_Rosen_confluent_union A: ∀ (a b : X A A),
    a`#×a# <== a#×a`# →
    b`#×b# <== b#×b`# →
    a`#×b# <== b#×a`# →
    (a+b)`#×(a+b)# <== (a+b)#×(a+b)`#.
  Proof.
    intros a b Ha Hb Hab.
    do 2 rewrite conv_plus at 1.
    do 2 rewrite (star_plus_star (b`) (a`)) at 1.
    apply semicomm_iter_left. semiring_normalize.
    rewrite 2 Hindley_Rosen_union; trivial with algebra.
    switch. assumption.
  Qed.

End Props2.