Library RelationAlgebra.level

level: tuples of Booleans identifying a point in the algebraic hierarchy

Require Import common.

a level specifies which relation algebra operations are considered

the interpretation in the model of binary relations is given on the right-hand side.

Record level := mk_level {
has_cup: bool;

set theoretic union

has_bot: bool;

empty relation

has_cap: bool;

set theoretic intersection

has_top: bool;

full relation

has_str: bool;

reflexive transitive closure

has_cnv: bool;

converse, or transpose

has_neg: bool;

Boolean negation

has_div: bool

residuals, or factors

}.
Declare Scope level_scope.
Bind Scope level_scope with level.
Delimit Scope level_scope with level.

dual level, for symmetry arguments related to lattices

Definition dual l := mk_level
  (has_cap l)
  (has_top l)
  (has_cup l)
  (has_bot l)
  (has_str l)
  (has_cnv l)
  (has_neg l)
  (has_div l).

Level constraints

lower k k', or k ≪ k', denotes the fact that there are less operations/axioms at level k than at level k'

Class lower (k k': level) := mk_lower:
  let 'mk_level a b c d e f g h := k in
  let 'mk_level a' b' c' d' e' f' g' h' := k' in
  is_true (a<<<a'&&& b<<<b' &&& c<<<c' &&& d<<<d'
           &&& e<<<e' &&& f<<<f' &&& g<<<g' &&& h <<< h').

Notation ≪ : \ll (company coq) or MUCH LESS-THAN

Declare Scope ra_scope.
Infix " ≪ " := lower (at level 79): ra_scope.
Arguments lower _ _: simpl never.

Local Open Scope ra_scope.

alternative specifiaction of h ≪ k

Lemma lower_spec h k: h ≪ k ↔
  (has_cup h → has_cup k ) ∧
  (has_bot h → has_bot k ) ∧
  (has_cap h → has_cap k ) ∧
  (has_top h → has_top k ) ∧
  (has_str h → has_str k ) ∧
  (has_cnv h → has_cnv k ) ∧
  (has_neg h → has_neg k ) ∧
  (has_div h → has_div k ).
Proof.
  destruct h; destruct k. unfold lower.
  rewrite !landb_spec, !le_bool_spec. reflexivity.
Qed.

≪ is a preorder

#[export] Instance lower_refl: Reflexive lower.
Proof. intro. setoid_rewrite lower_spec. tauto. Qed.

#[export] Instance lower_trans: Transitive lower.
Proof. intros h k l. setoid_rewrite lower_spec. tauto. Qed.

Merging levels

merging two levels: taking the union of their supported operations

Definition merge h k := mk_level
  (has_cup h ||| has_cup k)
  (has_bot h ||| has_bot k)
  (has_cap h ||| has_cap k)
  (has_top h ||| has_top k)
  (has_str h ||| has_str k)
  (has_cnv h ||| has_cnv k)
  (has_neg h ||| has_neg k)
  (has_div h ||| has_div k).
Infix "+" := merge: level_scope.
Arguments merge _ _: simpl never.

merge is a supremum for the ≪ preorder

Lemma merge_spec h k l: h +k ≪ l ↔ h ≪ l ∧ k ≪ l.
Proof. setoid_rewrite lower_spec. setoid_rewrite lorb_spec. tauto. Qed.

Lemma lower_xmerge h k l: l ≪ h ∨ l ≪ k → l ≪ (h + k ).
Proof.
assert (C:= merge_spec h k (h+k)).
intros [E|E]; (eapply lower_trans; [eassumption|]); apply C, lower_refl.
Qed.

Lemma lower_mergex h k l: h ≪ l → k ≪ l → h +k ≪ l.
Proof. rewrite merge_spec. tauto. Qed.

#[export] Instance merge_lower: Proper (lower ==> lower ==> lower) merge.
Proof. intros h k H h' k' H'. apply lower_mergex; apply lower_xmerge; auto. Qed.

Tactics for level constraints resolution

simple but efficient tactic, this is the one used by default, we give it as a hint for maximally inserted arguments (typeclasses resolution)

Ltac solve_lower := solve
  [ exact eq_refl
  | eassumption
  | repeat
    match goal with
      | H: ?h ≪ ?l , H': ?k ≪ ?l |- _ ≪ ?l ⇒

        apply (lower_mergex h k l H) in H'; clear H
      | H: ?k ≪ ?l |- ?h ≪ _ ⇒

        apply (lower_trans h k l eq_refl H)
    end ] || fail "could not prove this entailment".
#[export] Hint Extern 0 (_ ≪ _) ⇒ solve_lower: typeclass_instances.

heavier and more complete tactic, which we use in a selfdom way

Ltac solve_lower' := solve [
  (repeat
    match goal with
      H: _ + _ ≪ _ |- _ ⇒ apply merge_spec in H as [? ?]
    end);
  (repeat apply lower_mergex);
  auto 100 using lower_xmerge, lower_refl ] || fail "could not prove this entailment".

tactic used to discriminate unsatisfiable level constraint

Ltac discriminate_levels := solve [
  intros; repeat discriminate ||
    match goal with
      | H: _ + _ ≪ _ |- _ ⇒ apply merge_spec in H as [? ?]
    end ].

Concrete levels

Section levels.
Notation "1" := true.
Notation "0" := false.

atoms

Definition MIN := mk_level 0 0 0 0 0 0 0 0.
Definition CUP := mk_level 1 0 0 0 0 0 0 0.
Definition BOT := mk_level 0 1 0 0 0 0 0 0.
Definition CAP := mk_level 0 0 1 0 0 0 0 0.
Definition TOP := mk_level 0 0 0 1 0 0 0 0.
Definition STR := mk_level 0 0 0 0 1 0 0 0.
Definition CNV := mk_level 0 0 0 0 0 1 0 0.
Definition NEG := mk_level 0 0 0 0 0 0 1 0.
Definition DIV := mk_level 0 0 0 0 0 0 0 1.
Local Open Scope level_scope.

points of particular interest (i.e., corresponding to standard mathematical structures)

Definition SL := CUP.
Definition DL := Eval compute in CUP +CAP.
Definition BSL := Eval compute in SL +BOT.
Definition BDL := Eval compute in DL +BOT +TOP.
Definition BL := Eval compute in BDL +NEG.
Definition KA := Eval compute in SL +STR.
Definition AA := Eval compute in DL +STR.
Definition AL := Eval compute in CAP +CNV.
Definition DAL := Eval compute in DL +CNV.
Definition BKA := Eval compute in KA +BOT.
Definition CKA := Eval compute in KA +CNV.
End levels.