# 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
empty relation
set theoretic intersection
full relation
reflexive transitive closure
converse, or transpose
Boolean negation
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.