Library RelationAlgebra.lattice

lattice: from preorders to Boolean lattices

We define here all structures ranging from preorders to Boolean lattice (e.g., sup-semilattices, inf-semilattices with bottom element, bounded lattices, etc...).

Require Export common level.

Declare Scope ra_terms.
Delimit Scope ra_terms with ra.
Open Scope ra_scope.
Open Scope ra_terms.

Lattice operations

The following class packages all operations that can possibly come with a preorder: a supremum, a bottom element, a negation, etc... We use dummy values when working in structures lacking some operations.

We use a "Class" rather than a "Structure" just to make the first argument of all the corresponding projections implicit. Instances of this class will be declared as Canonical structures rather than typeclasses instances, so that this first argument will actually be inferred by unification. (except in the abstract and unconstrained case, where typeclass resolution will be called since unification will keep the hole unconstrained)

Universe L.

Class ops := mk_ops {
car: Type@{L};

carrier

leq: relation car;

preorder

weq: relation car;

underlying equality

cup: car → car → car;

supremum

cap: car → car → car;

infimum

neg: car → car;

Boolean negation

bot: car;

bottom element

top: car

top element

}.
Arguments car : clear implicits.
Coercion car : ops >-> Sortclass.
Bind Scope ra_terms with car.

Hints for simpl

Arguments weq {ops} (x y)%ra / : simpl nomatch.
Arguments leq {ops} (x y)%ra / : simpl nomatch.
Arguments cup {ops} (x y)%ra / : simpl nomatch.
Arguments cap {ops} (x y)%ra / : simpl nomatch.
Arguments neg {ops} (x)%ra / : simpl nomatch.
Arguments bot {ops} / : simpl nomatch.
Arguments top {ops} / : simpl nomatch.

Notations

≦ : \leqq (company coq) or LESS THAN OVER EQUAL TO (was '<==')

≡ : \equiv (company coq) or IDENTIAL TO (was '==')

⊔ : \sqcup (company coq) or SQUARE CUP (was '\cup')

⊓ : \sqcap (company coq) or SQUARE CAP (was '\cap')

Infix "≦" := leq (at level 79): ra_scope.
Infix "≡" := weq (at level 79): ra_scope.
Infix "⊔" := cup (left associativity, at level 50): ra_terms.
Infix "⊓" := cap (left associativity, at level 40): ra_terms.
Notation "! x" := (neg x) (right associativity, at level 20, format "! x"): ra_terms.

Lattice laws (axioms)

laws l X provides the laws corresponding to the various operations of X, provided these operations belong to the level l. For instance, the specification of the supremum (cup) is available only if the level contains CUP.

Note that leq is always require to be a preorder, and weq is always required to be the kernel of that preorder.

Also note that some axioms (leq_bx_, leq_x_t_) are present unless some operations are present in l. They end with an underscore, they are actually derivable from the other axioms when the additional operations belong to l. They are reformulated without the escaping disjunction below, under the same name but without the ending underscore (see leq_bx, leq_x_t below).

The field name cupcap_ also ends with an underscore, this is because it's statement is an inequality, for which the converse inequality is derivable. It is thus later reformulated as an equality (see lemma cupcap below).

Unlike for operations (ops), laws are actually inferred by typeclass resolution.

Class laws (l: level) (X: ops) := {
  leq_PreOrder:> PreOrder leq;
  weq_spec : ∀ x y , x ≡ y ↔ x ≦ y ∧ y ≦ x;
  cup_spec {Hl:CUP ≪ l}: ∀ x y z, x ⊔ y ≦ z ↔ x ≦ z ∧ y ≦ z;
  cap_spec {Hl:CAP ≪ l}: ∀ x y z, z ≦ x ⊓ y ↔ z ≦ x ∧ z ≦ y;
  leq_bx_ {Hl:BOT ≪ l}: NEG +CAP ≪ l ∨ ∀ x, bot ≦ x;
  leq_xt_ {Hl:TOP ≪ l}: NEG +CUP ≪ l ∨ ∀ x, x ≦ top;
  cupcap_ {Hl:DL ≪ l}: ∀ x y z, (x ⊔ y ) ⊓ (x ⊔ z ) ≦ x ⊔ (y ⊓ z );
  capneg {Hl:NEG +CAP +BOT ≪ l}: ∀ x, x ⊓ !x ≡ bot;
  cupneg {Hl:NEG +CUP +TOP ≪ l}: ∀ x, x ⊔ !x ≡ top
}.

Properties of the preorder (≦) and it kernel (≡)

Lemma antisym `{laws}: ∀ x y, x ≦ y → y ≦ x → x ≡ y.
Proof. intros. apply weq_spec; split; assumption. Qed.

Lemma from_below `{laws}: ∀ x y, (∀ z, z ≦ x ↔ z ≦ y ) → x ≡ y.
Proof. intros x y E. apply antisym; apply E; reflexivity. Qed.

Lemma from_above `{laws}: ∀ x y, (∀ z, x ≦ z ↔ y ≦ z ) → x ≡ y.
Proof. intros x y E. apply antisym; apply E; reflexivity. Qed.

Trivial hints

#[export] Hint Extern 0 (_ ≦ _) ⇒ reflexivity : core.
#[export] Hint Extern 0 (_ ≡ _) ⇒ reflexivity : core.

Instances to be used by the setoid_rewrite machinery

#[export] Instance weq_Equivalence `{laws}: Equivalence weq.
Proof.
  constructor.
   intro. now rewrite weq_spec.
   intros ? ?. rewrite 2weq_spec. tauto.
   intros x y z. rewrite 3weq_spec. intuition; etransitivity; eassumption.
Qed.

#[export] Instance weq_rel {ops} : RewriteRelation (@weq ops) := {}.

#[export] Instance weq_leq `{laws}: subrelation weq leq.
Proof. intros x y E. apply weq_spec in E as [? ?]. assumption. Qed.

#[export] Instance weq_geq `{laws}: subrelation weq (flip leq).
Proof. intros x y E. apply weq_spec in E as [? ?]. assumption. Qed.

#[export] Instance leq_weq_iff `{laws}: Proper (weq ==> weq ==> iff) leq.
Proof.
  intros x y E x' y' E'. split; intro L.
  now rewrite <-E, <-E'.
  now rewrite E, E'.
Qed.

Utility lemmas, to deduce that a function preserves weq once we proved that it preserves leq, these are extremely useful in practice

Lemma op_leq_weq_1 {h k X Y} {HX: laws h X} {HY: laws k Y} {f: X → Y}
  {Hf: Proper (leq ==> leq) f}: Proper (weq ==> weq) f.
Proof. intros x y. rewrite 2weq_spec. intro E; split; apply Hf; apply E. Qed.

Lemma op_leq_weq_2 {h k l X Y Z} {HX: laws h X} {HY: laws k Y} {HZ: laws l Z} {f: X → Y → Z}
  {Hf: Proper (leq ==> leq ==> leq) f}: Proper (weq ==> weq ==> weq) f.
Proof.
  intros x y E x' y' E'. rewrite weq_spec in E. rewrite weq_spec in E'.
  apply antisym; apply Hf; (apply E || apply E').
Qed.

Additional hints, to speedup typeclass resolution

#[export] Instance leq_Reflexive `{laws}: Reflexive leq |1.
Proof. eauto with typeclass_instances. Qed.
#[export] Instance leq_Transitive `{laws}: Transitive leq |1.
Proof. eauto with typeclass_instances. Qed.

#[export] Instance weq_Reflexive `{laws}: Reflexive weq |1.
Proof. eauto with typeclass_instances. Qed.
#[export] Instance weq_Transitive `{laws}: Transitive weq |1.
Proof. eauto with typeclass_instances. Qed.
#[export] Instance weq_Symmetric `{laws}: Symmetric weq |1.
Proof. eauto with typeclass_instances. Qed.

We declare most projections as Opaque for typeclass resolution: this saves a lot of compilation time

#[export] Typeclasses Opaque leq cup cap neg bot top.

Basic properties of ⊔, ⊓, bot, and top

Lemma leq_cupx `{laws} `{CUP ≪ l}: ∀ x y z, x ≦ z → y ≦ z → x ⊔ y ≦ z.
Proof. intros. apply cup_spec. split; assumption. Qed.

Lemma leq_xcup `{laws} `{CUP ≪ l}: ∀ x y z, z ≦ x ∨ z ≦ y → z ≦ x ⊔ y.
Proof.
  intros x y z. assert (C:= cup_spec x y (x ⊔ y)).
  intros [E|E]; rewrite E; apply C; reflexivity.
Qed.

Lemma leq_xcap `{laws} `{CAP ≪ l}: ∀ x y z, z ≦ x → z ≦ y → z ≦ x ⊓ y.
Proof. intros. apply cap_spec. split; assumption. Qed.

Lemma leq_capx `{laws} `{CAP ≪ l}: ∀ x y z, x ≦ z ∨ y ≦ z → x ⊓ y ≦ z.
Proof.
  intros x y z. assert (C:= cap_spec x y (x ⊓ y)).
  intros [E|E]; rewrite <- E; apply C; reflexivity.
Qed.

Lemma leq_bx `{L: laws} {Hl:BOT ≪ l}: ∀ x, bot ≦ x.
Proof.
  destruct leq_bx_ as [Hl'|H]. 2: apply H.
  intro x. rewrite <-(capneg x). apply leq_capx. left. reflexivity.
Qed.

Lemma leq_xb_iff `{L: laws} {Hl:BOT ≪ l}: ∀ x, x ≦ bot ↔ x ≡ bot.
Proof.
  split; intro. apply antisym. assumption. apply leq_bx.
  now apply weq_leq.
Qed.

Lemma leq_xt `{L: laws} {Hl:TOP ≪ l}: ∀ x, x ≦ top.
Proof.
  destruct leq_xt_ as [Hl'|H]. 2: apply H.
  intro x. rewrite <-(cupneg x). apply leq_xcup. left. reflexivity.
Qed.

Lemma leq_tx_iff `{L: laws} {Hl:TOP ≪ l}: ∀ x, top ≦ x ↔ x ≡ top.
Proof.
  split; intro. apply antisym. apply leq_xt. assumption.
  now apply weq_leq.
Qed.

Subtyping / weakening

laws that hold at any level h hold for all level k ≪ h

Lemma lower_lattice_laws {h k} {X} {H: laws h X} {le: k ≪ h}: laws k X.
Proof.
  constructor; try solve [ apply H | intro; apply H; eauto using lower_trans ].
   intro. right. eapply @leq_bx. apply H. eauto using lower_trans.
   intro. right. eapply @leq_xt. apply H. eauto using lower_trans.
Qed.

Solving (in)equations in non distributive lattices

simple tactic to solve lattice (in)equations, using a basic focused proof search algorithm

Ltac lattice :=
  let rec async := solve
    [ apply leq_cupx; async
    | apply leq_xcap; async
    | apply leq_bx
    | apply leq_xt
    | sync_l false || sync_r false ]
  with sync_l b := solve
    [ reflexivity
    | assumption
    | apply leq_capx; ((left; sync_l true) || (right; sync_l true))
    | match b with true ⇒ async end ]
  with sync_r b := solve
    [ reflexivity
    | assumption
    | apply leq_xcup; ((left; sync_r true) || (right; sync_r true))
    | match b with true ⇒ async end ]
  in
  (try apply antisym); async || fail "not a lattice theorem".

extension of the above tactic so that it also tries to exploit hypotheses in a more agressive way

Ltac hlattice :=
  repeat
    match goal with
      | H: _ ≡ _ |- _ ⇒ apply weq_spec in H as [? ?]
      | H: _ ⊔ _ ≦ _ |- _ ⇒ apply cup_spec in H as [? ?]
      | H: _ ≦ _ ⊓ _ |- _ ⇒ apply cap_spec in H as [? ?]
    end; lattice.

Reasoning by duality

dual lattice operations: we reverse the preorder, and swap cup with cap, and resp bot with top)

Definition dual (X: ops) := {|
  leq := flip leq;
  weq := weq;
  cup := cap;
  cap := cup;
  neg := neg;
  bot := top;
  top := bot |}.

Lemma capcup_ `{laws} `{DL ≪ l}: ∀ x y z, x ⊓ (y ⊔ z ) ≦ (x ⊓ y ) ⊔ (x ⊓ z ).
Proof.
  intros. rewrite <- cupcap_. apply leq_xcap. lattice.
  transitivity (z ⊔ x ⊓ y). 2: lattice.
  rewrite <- cupcap_. lattice.
Qed.

Ltac inverse_lower l Hl :=
  revert Hl; clear; destruct l; unfold lower, merge; simpl; rewrite ?landb_spec; tauto.

laws on a given set of operations can be transferred to the dual set of operations

Lemma dual_laws l (X: ops): laws (level.dual l) X → laws l (dual X).
Proof.
  intro H. constructor; try (destruct l; apply H).
  constructor. apply H. intros x y z H1 H2. revert H2 H1. simpl. apply H.
  intros x y. simpl. rewrite weq_spec. tauto.
  intro. simpl. eapply @capcup_. apply H. inverse_lower l Hl.
  intro. simpl. eapply @cupneg. apply H. inverse_lower l Hl.
  intro. simpl. eapply @capneg. apply H. inverse_lower l Hl.
Qed.

this gives us a tactic to prove properties by lattice duality

Lemma dualize {h} {P: ops → Prop} (L: ∀ l X, laws l X → h ≪ l → P X)
  {l X} {H: laws l X} {Hl:level.dual h ≪ l}: P (dual X).
Proof.
  apply L with (level.dual l). apply dual_laws.
  destruct l; apply H.
  revert Hl. rewrite 2lower_spec. destruct l; destruct h; simpl. tauto.
Qed.

Ltac dual x := apply (dualize x).

(⊔,bot) forms a commutative, idempotent monoid

Lemma cupA `{laws} `{CUP ≪ l}: ∀ x y z, x ⊔ (y ⊔ z ) ≡ (x ⊔ y ) ⊔ z.
Proof. intros. lattice. Qed.
Lemma cupC `{laws} `{CUP ≪ l}: ∀ x y, x ⊔ y ≡ y ⊔ x.
Proof. intros. lattice. Qed.
Lemma cupI `{laws} `{CUP ≪ l}: ∀ x, x ⊔ x ≡ x.
Proof. intros. lattice. Qed.
Lemma cupbx `{laws} `{CUP +BOT ≪ l}: ∀ x, bot ⊔ x ≡ x.
Proof. intros. lattice. Qed.
Lemma cupxb `{laws} `{CUP +BOT ≪ l}: ∀ x, x ⊔ bot ≡ x.
Proof. intros. lattice. Qed.

Lemma cuptx `{laws} `{CUP +TOP ≪ l}: ∀ x, top ⊔ x ≡ top.
Proof. intros. lattice. Qed.
Lemma cupxt `{laws} `{CUP +TOP ≪ l}: ∀ x, x ⊔ top ≡ top.
Proof. intros. lattice. Qed.

Lemma leq_cup_l `{laws} `{CUP ≪ l} x y: x ≦ x ⊔ y.
Proof. lattice. Qed.
Lemma leq_cup_r `{laws} `{CUP ≪ l} x y: y ≦ x ⊔ y.
Proof. lattice. Qed.

#[export] Instance cup_leq `{laws} `{CUP ≪ l}: Proper (leq ==> leq ==> leq) cup.
Proof. intros x x' Hx y y' Hy. lattice. Qed.

#[export] Instance cup_weq `{laws} `{CUP ≪ l}: Proper (weq ==> weq ==> weq) cup.
Proof. apply op_leq_weq_2. Qed.

distribution of ⊔ over ⊓

Lemma cupcap `{laws} `{DL ≪ l}: ∀ x y z, x ⊔ (y ⊓ z ) ≡ (x ⊔ y ) ⊓ (x ⊔ z ).
Proof. intros. apply antisym. lattice. apply cupcap_. Qed.

characterisation of the preorder by the semilattice operations

Lemma leq_iff_cup `{laws} `{CUP ≪ l} (x y: X): x ≦ y ↔ x ⊔ y ≡ y.
Proof. split. intro. hlattice. intro E. rewrite <- E. lattice. Qed.

Lemma comm4 `{laws} `{CUP ≪ l} (a b c d: X): a ⊔ b ⊔ c ⊔ d ≡ (a ⊔ c ) ⊔ (b ⊔ d ).
Proof. lattice. Qed.

(⊓,top) forms a commutative, idempotent monoid (by duality)

Lemma capA `{laws} `{CAP ≪ l}: ∀ x y z, x ⊓ (y ⊓ z ) ≡ (x ⊓ y ) ⊓ z.
Proof. dual @cupA. Qed.
Lemma capC `{laws} `{CAP ≪ l}: ∀ x y, x ⊓ y ≡ y ⊓ x.
Proof. dual @cupC. Qed.
Lemma capI `{laws} `{CAP ≪ l}: ∀ x, x ⊓ x ≡ x.
Proof. dual @cupI. Qed.
Lemma captx `{laws} `{CAP +TOP ≪ l}: ∀ x, top ⊓ x ≡ x.
Proof. dual @cupbx. Qed.
Lemma capxt `{laws} `{CAP +TOP ≪ l}: ∀ x, x ⊓ top ≡ x.
Proof. dual @cupxb. Qed.

Lemma capbx `{laws} `{CAP +BOT ≪ l}: ∀ x, bot ⊓ x ≡ bot.
Proof. dual @cuptx. Qed.
Lemma capxb `{laws} `{CAP +BOT ≪ l}: ∀ x, x ⊓ bot ≡ bot.
Proof. dual @cupxt. Qed.

Lemma leq_cap_l `{laws} `{CAP ≪ l} x y: x ⊓ y ≦ x.
Proof. lattice. Qed.
Lemma leq_cap_r `{laws} `{CAP ≪ l} x y: x ⊓ y ≦ y.
Proof. lattice. Qed.

#[export] Instance cap_leq `{laws} `{CAP ≪ l}: Proper (leq ==> leq ==> leq) cap.
Proof. intros x x' Hx y y' Hy. lattice. Qed.

#[export] Instance cap_weq `{laws} `{CAP ≪ l}: Proper (weq ==> weq ==> weq) cap.
Proof. apply op_leq_weq_2. Qed.

Lemma leq_iff_cap `{laws} `{CAP ≪ l} (x y: X): x ≦ y ↔ x ⊓ y ≡ x.
Proof. split. intro. hlattice. intro E. rewrite <- E. lattice. Qed.

Lemma capcup `{laws} `{DL ≪ l}: ∀ x y z, x ⊓ (y ⊔ z ) ≡ (x ⊓ y ) ⊔ (x ⊓ z ).
Proof. dual @cupcap. Qed.

Lemma cupcap' `{laws} `{DL ≪ l}: ∀ x y z, (y ⊓ z ) ⊔ x ≡ (y ⊔ x ) ⊓ (z ⊔ x ).
Proof. intros. now rewrite cupC, cupcap, 2(cupC x). Qed.

Lemma capcup' `{laws} `{DL ≪ l}: ∀ x y z, (y ⊔ z ) ⊓ x ≡ (y ⊓ x ) ⊔ (z ⊓ x ).
Proof. dual @cupcap'. Qed.

Properties of negation

Lemma neg_unique' `{laws} `{BL ≪ l} (x y: X): y ⊓ x ≦ bot → y ≦ !x.
Proof.
  intros E. rewrite <-(capxt y). rewrite <-(cupneg x).
  rewrite capcup. rewrite E. lattice.
Qed.

Lemma neg_unique `{laws} `{BL ≪ l} (x y: X):
  top ≦ y ⊔ x → y ⊓ x ≦ bot → y ≡ !x.
Proof.
  intros Ht Hb. apply antisym.
  now apply neg_unique'.
  revert Ht. dual @neg_unique'.
Qed.

#[export] Instance neg_leq `{laws} `{BL ≪ l}: Proper (leq --> leq) neg.
Proof.
  intros x y E. apply neg_unique'.
  rewrite <-E, capC. now rewrite capneg.
Qed.

#[export] Instance neg_weq `{laws} `{BL ≪ l}: Proper (weq ==> weq) neg.
Proof. intros x y. rewrite 2weq_spec. intro E; split; apply neg_leq, E. Qed.

Lemma negneg `{laws} `{BL ≪ l} (x: X): !!x ≡ x.
Proof. symmetry. apply neg_unique. now rewrite cupneg. now rewrite capneg. Qed.

Lemma negbot `{laws} `{BL ≪ l}: !bot ≡ top.
Proof. symmetry. apply neg_unique; lattice. Qed.

Lemma negtop `{laws} `{BL ≪ l}: !top ≡ bot.
Proof. dual @negbot. Qed.

Lemma negcap' `{laws} `{BL ≪ l} (x y: X): !x ⊔ !y ≦ !(x ⊓ y ).
Proof. apply leq_cupx; apply neg_leq; lattice. Qed.

Lemma negcup `{laws} `{BL ≪ l} (x y: X): !(x ⊔ y ) ≡ !x ⊓ !y.
Proof.
  apply antisym. dual @negcap'.
  rewrite <- (negneg x) at 2.
  rewrite <- (negneg y) at 2.
  now rewrite negcap', negneg.
Qed.

Lemma negcap `{laws} `{BL ≪ l} (x y: X): !(x ⊓ y ) ≡ !x ⊔ !y.
Proof. dual @negcup. Qed.

switching negations

Lemma neg_leq_iff `{laws} `{BL ≪ l} (x y: X): !x ≦ !y ↔ y ≦ x.
Proof. split. intro E. apply neg_leq in E. now rewrite 2negneg in E. apply neg_leq. Qed.
Lemma neg_leq_iff' `{laws} `{BL ≪ l} (x y: X): x ≦ !y ↔ y ≦ !x.
Proof. now rewrite <- neg_leq_iff, negneg. Qed.
Lemma neg_leq_iff'' `{laws} `{BL ≪ l} (x y: X): !x ≦ y ↔ !y ≦ x.
Proof. now rewrite <- neg_leq_iff, negneg. Qed.

Lemma neg_weq_iff `{laws} `{BL ≪ l} (x y: X): !x ≡ !y ↔ y ≡ x.
Proof. now rewrite 2weq_spec, 2neg_leq_iff. Qed.
Lemma neg_weq_iff' `{laws} `{BL ≪ l} (x y: X): x ≡ !y ↔ !x ≡ y.
Proof. now rewrite <-neg_weq_iff, negneg. Qed.
Lemma neg_weq_iff'' `{laws} `{BL ≪ l} (x y: X): !x ≡ y ↔ x ≡ !y.
Proof. now rewrite <-neg_weq_iff, negneg. Qed.

Ltac neg_switch := first [
  rewrite neg_leq_iff |
  rewrite neg_leq_iff' |
  rewrite neg_leq_iff'' |
  rewrite <-neg_leq_iff |
  rewrite neg_weq_iff |
  rewrite neg_weq_iff' |
  rewrite neg_weq_iff'' |
  rewrite <-neg_weq_iff ].

Lemma leq_cap_neg `{laws} `{BL ≪ l} (x y: X): y ≦ x ↔ y ⊓ !x ≦ bot.
Proof.
  split. intro E. now rewrite E, capneg.
  intro E. now rewrite (neg_unique' _ _ E), negneg.
Qed.

Lemma leq_cap_neg' `{laws} `{BL ≪ l} (x y: X): y ⊓ x ≦ bot ↔ y ≦ !x.
Proof. rewrite <-(negneg x) at 1. symmetry. apply leq_cap_neg. Qed.

Lemma leq_cup_neg `{laws} `{BL ≪ l} (x y: X): x ≦ y ↔ top ≦ y ⊔ !x.
Proof. dual @leq_cap_neg. Qed.

Lemma leq_cup_neg' `{laws} `{BL ≪ l} (x y: X): top ≦ y ⊔ x → !x ≦ y.
Proof. dual @leq_cap_neg'. Qed.

Morphisms

an l-morphism betwen to sets of operations are defined as expected: the function is requried to preserve only the operations listed in l

Class morphism l {X Y: ops} (f: X → Y) := {
  fn_leq: Proper (leq ==> leq) f;
  fn_weq: Proper (weq ==> weq) f;
  fn_cup {Hl:CUP ≪ l}: ∀ x y, f (x ⊔ y) ≡ f x ⊔ f y;
  fn_cap {Hl:CAP ≪ l}: ∀ x y, f (x ⊓ y) ≡ f x ⊓ f y;
  fn_bot {Hl:BOT ≪ l}: f bot ≡ bot;
  fn_top {Hl:TOP ≪ l}: f top ≡ top;
  fn_neg {Hl:NEG ≪ l}: ∀ x, f (!x) ≡ !(f x )
}.

generating a structure by injective embedding

Lemma laws_of_injective_morphism {h l X Y} {L: laws h Y} {Hl: l ≪ h} f:
  @morphism l X Y f →
  (∀ x y, f x ≦ f y → x ≦ y ) →
  (∀ x y, f x ≡ f y → x ≡ y ) →
  laws l X.
Proof.
  intros Hf Hleq Hweq. apply (@lower_lattice_laws _ _ _ L) in Hl. clear L.
  assert (Hleq_iff: ∀ x y, f x ≦ f y ↔ x ≦ y).
   split. apply Hleq. apply fn_leq.
  assert (Hweq_iff: ∀ x y, f x ≡ f y ↔ x ≡ y).
   split. apply Hweq. apply fn_weq.
  constructor. constructor.
   intro. apply Hleq. reflexivity.
   intros x y z. rewrite <-3Hleq_iff. apply Hl.
   intros. now rewrite <-Hweq_iff, weq_spec, 2Hleq_iff.
   intros. rewrite <-3Hleq_iff, fn_cup. apply cup_spec.
   intros. rewrite <-3Hleq_iff, fn_cap. apply cap_spec.
   right. intros. apply Hleq. rewrite fn_bot. apply leq_bx.
   right. intros. apply Hleq. rewrite fn_top. apply leq_xt.
   intros. apply Hleq. rewrite fn_cup, fn_cap, 2fn_cup, fn_cap. apply cupcap_.
   intros. rewrite <-Hweq_iff. rewrite fn_cap, fn_neg, fn_bot. apply capneg.
   intros. rewrite <-Hweq_iff. rewrite fn_cup, fn_neg, fn_top. apply cupneg.
Qed.

Pointwise extension of a structure

Definition pw0 {Y X} (f: X) (y: Y) := f.
Definition pw1 {Y X} (f: X → X) (u: Y → X) (y: Y) := f (u y).
Definition pw2 {Y X} (f: X → X → X) (u v: Y → X) (y: Y) := f (u y) (v y).

Arguments pw0 {Y X} _ _ /.
Arguments pw1 {Y X} _ _ _ /.
Arguments pw2 {Y X} _ _ _ _ /.

Universe pw.

As explained above, we use canonical structures for operations inference

Canonical Structure pw_ops (X: ops) (Y : Type@{pw}) : ops := {|
  car := Y → X;
  leq := pwr leq;
  weq := pwr weq;
  cup := pw2 cup;
  cap := pw2 cap;
  neg := pw1 neg;
  bot := pw0 bot;
  top := pw0 top
|}.

In contrast, we use typeclass resolution for laws inference. Note the level polymorphism in the instance below: laws of level l on X yield laws of the same level l on Y → X.

#[export] Instance pw_laws `{laws} (Y : Type@{pw}) : laws l (pw_ops X Y).
Proof.
  constructor; simpl; intros. constructor.
   intros f x. reflexivity.
   intros f g h ? ? x. now transitivity (g x).
   setoid_rewrite weq_spec. firstorder.
   setoid_rewrite cup_spec. firstorder.
   setoid_rewrite cap_spec. firstorder.
   right; intros; apply leq_bx.
   right; intros; apply leq_xt.
   apply cupcap_.
   apply capneg.
   apply cupneg.
Qed.

trick to factorise code in various tactics: make the choice between leq or weq first-class

Definition leq_or_weq (b: bool) := if b then @leq else @weq.
Arguments leq_or_weq _ {_} (_ _)%ra.
Notation "x <=[ b ]= y" := (leq_or_weq b x y) (at level 79): ra_scope.

Lemma leq_or_weq_weq `{laws} b: Proper (weq ==> weq ==> iff) (leq_or_weq b).
Proof. unfold leq_or_weq; case b; eauto with typeclass_instances. Qed.