Library ATBR.Converse

Properties and tactics about algebraic structures with converse.

In particular,

converse_down pushes converses down to leaves
switch add converses on both sides of an (in)equation, and pushes converses down to leaves

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

Section ISR.

  Context `{CISR: ConverseIdemSemiRing}.

  Lemma conv_compat' A B (x y: X A B): x` == y` -> x == y.

  Hint Rewrite conv_dot conv_plus conv_invol: converse_down.

  Ltac switch :=
    match goal with
      | |- _ ` == _ ` => apply conv_compat
      | |- _ == _ => apply conv_compat'
    end; autorewrite with converse_down.

  Lemma conv_one A: one A` == 1.
  Hint Rewrite conv_one: converse_down.

  Lemma conv_zero A B: zero B A` == 0.
  Hint Rewrite conv_zero: converse_down.

  Instance CISR_ISR: IdemSemiRing G.

  Global Instance conv_incr A B:
  Proper ((leq A B) ==> (leq B A)) (conv A B).

  Lemma conv_incr' A B (x y: X A B): x` <== y` -> x <== y.

End ISR.

the push converses down to leaves

Ltac converse_down :=
  repeat (
    rewrite conv_invol ||
    rewrite conv_dot ||
    rewrite conv_plus
  );
  repeat (
    rewrite conv_one ||
    rewrite conv_zero
  ).

add converses on both sides, and push converses down to leaves

Ltac switch :=
  match goal with
    | |- _ ` == _ ` => apply conv_compat
    | |- _ == _ => apply conv_compat'
    | |- _ ` <== _ ` => apply conv_incr
    | |- _ <== _ => apply conv_incr'
  end; converse_down.

Section KA.

  Context `{KA: ConverseKleeneAlgebra}.

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

  Lemma conv_star A (a: X A A): a# ` == a` #.

  Global Instance CKA_KA: KleeneAlgebra G.

End KA.

override, to take conv_star into account

Ltac converse_down ::=
  repeat (
    rewrite conv_invol ||
    rewrite conv_star ||
    rewrite conv_dot ||
    rewrite conv_plus
  );
  repeat (
    rewrite conv_one ||
    rewrite conv_zero
  ).