Library ATBR.KleeneAlgebra

Simple properties about Kleene algebras

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.

Section Props0.

Context `{KA: KleeneAlgebra}.

other induction schemes

  Lemma star_destruct_right_old A B: forall (a: X A A) (b c: X B A), b+c*a <== c -> b*a# <== c.

  Lemma star_destruct_left_old A B: forall (a: X A A) (b c: X A B), b+a*c <== c -> a#*b <== c.

  Lemma star_destruct_right_one A: forall (a c: X A A), 1+c*a <== c -> a# <== c.

  Lemma star_destruct_left_one A: forall (a c: X A A), 1+a*c <== c -> a# <== c.

End Props0.

simple tactics to run an induction without having to remember which scheme to use

Ltac star_left_induction :=
  first [ apply star_destruct_left |
          apply star_destruct_left_old |
          apply star_destruct_left_one ].

Ltac star_right_induction :=
  first [ apply star_destruct_right |
          apply star_destruct_right_old |
          apply star_destruct_right_one ].

simple properties

Section Props1.

  Context `{KA: KleeneAlgebra}.
  Variable A: T.

  Global Instance star_incr:
  Proper ((leq A A ) ==> (leq A A )) (star A).

  Global Instance star_compat: Proper ((equal A A ) ==> (equal A A )) (star A).

  Lemma one_leq_star_a (a: X A A): 1 <== a#.

  Lemma a_leq_star_a (a: X A A): a <== a#.

  Lemma star_mon_is_one (a: X A A): a <== 1 -> a# == 1.

  Lemma star_one: (1#: X A A ) == 1.

  Lemma star_zero: (0#: X A A ) == 1.

  Lemma star_a_a_leq_star_a (a: X A A): a#*a <== a#.

  Lemma a_star_a_leq_star_a_a (a: X A A): a*a# <== a#*a.

  Lemma star_make_right (a:X A A): 1+a*a# == a#.

End Props1.

hints

Hint Extern 1 (equal _ _ _ _) => apply star_compat; instantiate: compat algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_make_left: algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_make_right: algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_one: algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_zero: algebra.
Hint Extern 0 (leq _ _ _ _) => apply a_leq_star_a: algebra.
Hint Extern 0 (leq _ _ _ _) => apply one_leq_star_a: algebra.

Hint Rewrite @star_zero @star_one using ti_auto : simpl.
Hint Rewrite @star_mon_is_one using ti_auto : simpl.

dual Kleene algebra

more properties

Section Props2.
  Context `{KA: KleeneAlgebra}.
  Variable A: T.

  Lemma star_trans (a: X A A): a#*a# == a#.

  Lemma star_idem (a: X A A): a## == a#.

  Lemma a_star_a_leq_star_a: forall (a: X A A), a*a# <== a#.
  Lemma star_distr (a b: X A A): (a + b)# == a# * (b*a#)#.

  Lemma semicomm_iter_right B (a: X A A) (b: X B B) (c: X B A): c*a <== b*c -> c*a# <== b#*c.

  Lemma wsemicomm_iter_right (a b : X A A): a*b <== b#*a -> a*b# <== b#*a.

End Props2.

Hint Extern 1 (leq _ _ _ _) => apply star_incr: compat algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_idem: algebra.
Hint Extern 0 (equal _ _ _ _) => apply star_trans: algebra.

more properties, by duality

Section Props3.
  Context `{KA: KleeneAlgebra}.

  Lemma semicomm_iter_left: forall A B (a: X A A) (b: X B B) (c: X A B), a*c <== c*b -> a#*c <== c*b#.
  Lemma wsemicomm_iter_left: forall A (b a : X A A), a*b <== b*a# -> a#*b <== b*a#.
  Lemma comm_iter_left A B (x : X A B) a b: a * x == x * b -> a# * x == x * b# .

  Lemma move_star A (a: X A A): a#*a == a*a#.

  Lemma move_star2 A B (a: X A B) (b: X B A): (a*b)#*a == a*(b*a)#.

End Props3.

Section Props4.
  Context `{KA: KleeneAlgebra}.

  Lemma comm_iter_right: forall B A (x : X A B) a b, x * a == b * x -> x * a# == b# * x .
End Props4.