Library allegories



From 2pdom to allegories with top

This Coq development accompanies the paper entitled `Allegories: decidability and graph homomorphisms' by Damien Pous Valeria Vignudelli, 2018
We study four equational theories:
  • p2d (2pdom in the paper), that characterises isomorphism of connected K4-free graphs
  • p2t (2p in the paper), that characterise isomorphism of arbitrary K4-free graphs
  • all, allegories
  • alt, allegories with top
Those theories can be organised using the following lattice: 
         alt
        /   \ 
      2pt   all
        \   /
         2pd
We give formal proofs of the following results:
  • if x <= y in the above lattice, then `every y is an x' (e.g., every allegory with top is a 2p-algebra, which is Prop. 18 in the paper)
  • every 2pdom-algebra embeds in a 2p-algebra (Prop. 39)
  • every allegory embeds in an allegory with top (Prop. 43)
Proving those results requires us to formalise various laws about those equational theories, including for instance those in Prop. 13

Basic definitions


Require Import Setoid Morphisms.

Ltac now tac := tac; solve [auto].

Delimit Scope ra_terms with ra.

In order to share both notations and lemmas, we consider a single signature including all operations.
  • in 2pdom, the constant top will be unspecified
  • in alltop and in 2p, dom is axiomatised by its term definition
We moreover add the derived codomain operation in order to facilitate proofs by duality.
Class ops := mk_ops {
  car: Type;
carrier
  leq: relation car;
preorder
  weq: relation car;
equality
  dot: car → car → car;
product
  cap: car → car → car;
intersection
  cnv: car → car;
converse
  dom: car → car;
domain
  cod: car → car;
codomain
  one: car;
neutral element (1)
  top: car;
top element
}.
Implicit Arguments car [].
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 dot {ops} (x y)%ra / : simpl nomatch.
Arguments cap {ops} (x y)%ra / : simpl nomatch.
Arguments cnv {ops} (x)%ra / : simpl nomatch.
Arguments dom {ops} (x)%ra / : simpl nomatch.
Arguments cod {ops} (x)%ra / : simpl nomatch.
Arguments one {ops} / : simpl nomatch.
Arguments top {ops} / : simpl nomatch.

Notations

Infix "<==" := leq (at level 79): ra_scope.
Infix "==" := weq (at level 79): ra_scope.
Infix "*" := dot (left associativity, at level 40): ra_terms.
Infix "∩" := cap (left associativity, at level 50): ra_terms.
Notation "x `" := (cnv x) (at level 30): ra_terms.
Notation "1" := one: ra_terms.
Open Scope ra_scope.
Open Scope ra_terms.

Hint Extern 0 (_ <== _) ⇒ reflexivity.
Hint Extern 0 (_ == _) ⇒ reflexivity.

We use the following inductive type to denote the four equational theories
Inductive level := p2d | p2t | all | alt.

We formalise of the aforementionned lattice as a binary relation and we setup a small typeclass mechanism to infer automatically that we are at least at a certain point in the lattice
Definition le (h k: level) :=
  match h,k with
  | p2d,_ | _,alt | p2t,p2t | all,all ⇒ True
  | _,_ ⇒ False
  end.
Class Cle (h k: level) := mk_cle: le h k.
Infix "<<" := Cle (at level 79): ra_scope.
Ltac solve_cle := solve [exact I | assumption].
Hint Extern 0 (_ << _) ⇒ solve_cle: typeclass_instances.

Axioms

The following class defines the four equational theories, at once. laws l X intuitively states that the algebra X is an l-algebra, where ranges over {2pd,2pt,all,allt}.
Class laws (l: level) (X: ops) := mk_laws {
  
The first 12 fields correspond to axioms that are shared by the four theories (the last one just characterises codomain as a derived operation)
  weq_Equivalence:> Equivalence weq;
  dot_weq:> Proper (weq ==> weq ==> weq) dot;
  cap_weq:> Proper (weq ==> weq ==> weq) cap;
  cnv_weq:> Proper (weq ==> weq) cnv;
  dotA: ∀ x y z, x*(y*z) == (x*y)*z;
  dot1x: ∀ x, 1*x == x;
  capA: ∀ x y z, x∩(y∩z) == (x∩y)∩z;
  capC: ∀ x y, x∩y == y∩x;
  cnvdot: ∀ x y, (x*y)` == y`*x`;
  cnvcap: ∀ x y, (x∩y)` == x`∩y`;
  cnvI: ∀ x, x`` == x;
  domcnv: ∀ x, dom (x`) == cod x;

  
captx is an axiom only when top is there (p2d, alt).
This is constraint is expressed as p2t<<l
  captx `{p2t<<l}: ∀ x, top ∩ x == x;
  
  
Below: remaining axioms for p2d/p2t.
They are all derivable from allegories axioms.
Their names ends with an underscore since they have more general (derivable) statements (see the underscore-free lemma below in the file)
  dotxt_: l=p2t → ∀ x, x*top == dom x*top;
  dotax_: l=p2t → ∀ x y, (1∩x)*y == (1∩x)*top ∩ y;
  domdot_: l=p2d → ∀ x y, dom (x*y) == dom (x * dom y);
  dotacap_: l=p2d → ∀ x y z, dom x * (y∩z) == dom x * y ∩ z;
  cap11_ `{l<<p2t}: 1∩1 == 1;
  domcap_ `{l<<p2t}: ∀ x y, dom (x∩y) == 1 ∩ x*y`;
  dom_weq_ `{l<<p2t}: Proper (weq ==> weq) dom;
  
  
Below: the remaining axioms for allegories (note that we use monotonicity of product rather than semi-distributivity)
  dot_leq `{all<<l}:> Proper (leq ==> leq ==> leq) dot;
  leq_spec `{all<<l}: ∀ x y, x <== y ↔ x ∩ y == x;
  dom_aldef `{all<<l}: ∀ x, dom x == 1 ∩ x*x`;
  capdotx `{all<<l}: ∀ x y z, (x*y) ∩ z <== x*(y ∩ (x`*z));
  capI `{all<<l}: ∀ x, x ∩ x == x;
}.

Simple tactic to simplify terms using the easy laws
Hint Rewrite @dot1x @cnvdot @cnvcap @cnvI @captx using eauto with typeclass_instances: simpl.
Ltac simplify := autorewrite with simpl.

Typeclass for tests: those elements below 1
This typeclass make it possible to infer automatically that some elements are tests, and thus have additional properties (e.g., composition is commutative and idempotent on tests)

Class tst {X: ops} (x: X) := mk_tst: 1∩x == x.

Basic laws

As for the axioms, the lemmas below are all parametrised by a `level' l, indicating in which theory we are working.
When there are no constraint on this level, the law holds (is proved to hold) in the four equational theories.
Otherwise, the constraint indicates in which theories the lemma holds. For instance, Lemma cnvtop below only holds in theories where top exists: p2t and alt; this is expressed by the constraint p2t<<l.
Section s.
Context {l} {X} {L: laws l X}.

Lemma cnv_weq_iff x y: x` == y` ↔ x == y.
Proof.
  split; intro E.
  rewrite <-(cnvI x), <-(cnvI y). now apply cnv_weq.
  now apply cnv_weq.
Qed.

Lemma cnv_weq_iff' x y: x == y` ↔ x` == y.
Proof. split; intro; apply cnv_weq_iff; now rewrite cnvI. Qed.

Lemma splitl0: l<<p2t ∨ all<<l.
Proof. destruct l; intuition. Qed.

Lemma splitl1: l=p2d ∨ p2t<<l ∨ all<<l.
Proof. destruct l; intuition. Qed.

Lemma cap11: 1∩1 == 1.
Proof. destruct splitl0. apply cap11_. apply capI. Qed.

Lemma cnv1: 1` == 1.
Proof. rewrite <- (dot1x (1`)). apply cnv_weq_iff. now simplify. Qed.

Lemma dotx1 x: x*1 == x.
Proof. apply cnv_weq_iff. now rewrite cnvdot,cnv1,dot1x. Qed.

Global Instance tst_one: tst 1.
Proof. apply cap11. Qed.

Global Instance tst_cap1 {a} {Ha: tst a} x: tst (a ∩ x).
Proof. unfold tst in *. rewrite <- Ha at 2. apply capA. Qed.

Global Instance tst_cap2 {a} {Ha: tst a} x: tst (x ∩ a).
Proof. unfold tst. rewrite (capC x a). apply tst_cap1. Qed.

Lemma capxt `{p2t<<l} x: x ∩ top == x.
Proof. rewrite capC. apply captx. Qed.

Lemma cnvtop `{p2t<<l}: top` == top.
Proof.
  rewrite <- (captx (top`)). apply cnv_weq_iff.
  now rewrite cnvcap, cnvI, capC, captx.
Qed.

Global Instance leq_PreOrder `{all<<l}: PreOrder leq.
Proof.
  constructor.
  intro x. rewrite leq_spec. apply capI.
  intros x y z. rewrite 3leq_spec.
  intros XY YZ. rewrite <-XY. now rewrite <-capA, YZ.
Qed.

Lemma weq_spec `{all<<l} x y: x==y ↔ x<==y ∧ y<==x.
Proof.
  rewrite 2leq_spec.
  split; intro E. now rewrite E, capI.
  destruct E as [Ex Ey]. now rewrite <-Ex, capC.
Qed.

Lemma antisym `{all<<l}: ∀ x y, x<==y → y<==x → x==y.
Proof. intros. apply weq_spec; split; assumption. Qed.

Lemma from_below `{all<<l}: ∀ x y, (∀ z, z<==x ↔ z<==y) → x==y.
Proof. intros x y E. apply antisym; apply E; reflexivity. Qed.

Lemma from_above `{all<<l}: ∀ x y, (∀ z, x<==z ↔ y<==z) → x==y.
Proof. intros x y E. apply antisym; apply E; reflexivity. Qed.

Global Instance weq_leq `{all<<l}: subrelation weq leq.
Proof. intros x y E. apply weq_spec in E as [? ?]. assumption. Qed.

Global Instance weq_geq `{all<<l}: subrelation weq (Basics.flip leq).
Proof. intros x y E. apply weq_spec in E as [? ?]. assumption. Qed.

Global Instance leq_weq_iff `{all<<l}: Proper (weq ==> weq ==> iff) leq.
Proof.
  intros x y E x' y' E'. split; intros ?.
  now rewrite <-E, <-E'.
  now rewrite E, E'.
Qed.

Global Instance cnv_leq `{all<<l}: Proper (leq ==> leq) cnv.
Proof.
  intros x x'. rewrite 2leq_spec. intro Hx. rewrite <-Hx at 2.
  symmetry. apply cnvcap.
Qed.

Lemma cnv_leq_iff `{all<<l} x y: x` <== y` ↔ x <== y.
Proof. split. intro E. apply cnv_leq in E. now rewrite 2cnvI in E. apply cnv_leq. Qed.

Lemma cnv_leq_iff' `{all<<l} x y: x <== y` ↔ x` <== y.
Proof. now rewrite <- cnv_leq_iff, cnvI. Qed.

Lemma cap_spec `{all<<l} x y z: z <== x ∩ y ↔ z <== x ∧ z <== y.
Proof.
  rewrite 3leq_spec. split.
  intros <-. split.
  now rewrite <-capA, (capC x), <-capA, capI.
  now rewrite <-2capA, capI.
  intros [Ex Ey]. rewrite <-Ey at 2. rewrite <-Ex at 2. apply capA.
Qed.

Global Instance cap_leq `{all<<l}: Proper (leq ==> leq ==> leq) cap.
Proof.
  intros x x' Hx y y' Hy. rewrite leq_spec in Hx, Hy.
  rewrite leq_spec. rewrite <-capA, (capC y), 2capA.
  rewrite Hx. now rewrite <-capA, (capC y'), Hy.
Qed.

Lemma leq_xcap `{all<<l} x y z: z<==x → z<==y → z <== x ∩ y.
Proof. intros. apply cap_spec. split; assumption. Qed.

Lemma leq_capx `{all<<l} x y z: x<==z ∨ y<==z → x ∩ y <== z.
Proof.
  assert (C:= cap_spec x y (x ∩ y)).
  intros [E|E]; rewrite <- E; apply C; reflexivity.
Qed.

Lemma leq_xt `{alt<<l} x: x <== top.
Proof.
  replace l with alt in L by (destruct l; intuition contradiction).
  rewrite leq_spec. rewrite capC. apply captx.
Qed.

End s.

Hint Rewrite @dotx1 @cnv1 @cnvtop @capxt using eauto with typeclass_instances: simpl.

Tactic to exploit converse for duality reasonning (apply converse and normalise)

Ltac cnv_switch := first [
  rewrite cnv_leq_iff |
  rewrite cnv_leq_iff' |
  rewrite <-cnv_leq_iff' |
  rewrite <-cnv_leq_iff |
  rewrite cnv_weq_iff |
  rewrite cnv_weq_iff' |
  rewrite <-cnv_weq_iff' |
  rewrite <-cnv_weq_iff ]; simplify.

Tactics to solve goals about the semilattice structure

Ltac lattice :=
  let rec async := solve
    [ apply leq_xcap; async
    | apply leq_xt
    | apply dot_leq; async
    | apply cnv_leq; async
    | 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
    | match b with true ⇒ async end ]
  in
  (try apply antisym); async || fail "not a lattice theorem".

Ltac hlattice :=
  repeat
    match goal with
      | H: _ == _ |- _ ⇒ apply weq_spec in H as [? ?]
      | H: _ <== _ ∩ _ |- _ ⇒ apply cap_spec in H as [? ?]
    end; lattice.

Advanced laws


Section s'.
Context {l} {X} {L: laws l X}.

Lemma cap1 `{all<<l} x y: x ∩ y <== x.
Proof. lattice. Qed.

Lemma cap2 `{all<<l} x y: x ∩ y <== y.
Proof. lattice. Qed.

Lemma scapdotx `{all<<l} x x' y z: ((x∩x')*y) ∩ z <== x' * (y ∩ (x`*z)).
Proof. rewrite capdotx. lattice. Qed.

Lemma capdotx' `{all<<l} x y z: (y*x) ∩ z <== (y ∩ (z*x`))*x.
Proof. cnv_switch. rewrite capdotx. now simplify. Qed.

Lemma scapdotx' `{all<<l} x x' y z: (y*(x∩x')) ∩ z <== (y ∩ (z*x`))*x'.
Proof. cnv_switch. rewrite scapdotx. now simplify. Qed.

Lemma exchange `{all<<l} x y z t: (x∩z)*(y∩t) <== x*y ∩ z*t.
Proof. lattice. Qed.

Lemma dedekin `{all<<l} x y z: (x*y) ∩ z <== (x ∩ (z*y`))*(y ∩ (x`*z)).
Proof.
  rewrite <-scapdotx'. rewrite capA, capI.
  now rewrite <-capdotx, <-capA, capI.
Qed.

Global Instance dom_leq `{all<<l}: Proper (leq ==> leq) dom.
Proof. intros x x'. rewrite 2dom_aldef. intro E. now rewrite E. Qed.

Lemma tst1 `{all<<l} {a} {Ha: tst a}: a <== 1.
Proof. rewrite <-Ha. lattice. Qed.

Global Instance dom_weq: Proper (weq ==> weq) dom.
Proof.
  destruct splitl0 as [?|?]. apply dom_weq_.
  intros x y E. now rewrite 2dom_aldef, E.
Qed.

Global Instance cod_weq: Proper (weq ==> weq) cod.
Proof. intros x y E. rewrite <-2domcnv. now rewrite E. Qed.

Lemma domcap x y: dom (x∩y) == 1 ∩ x*y`.
Proof.
  destruct splitl0. now apply domcap_.
  rewrite dom_aldef. apply antisym.
  rewrite <-(capI 1) at 1.
  rewrite <-capA. lattice.
  apply leq_xcap. lattice.
  rewrite capC, dedekin. simplify. lattice.
Qed.

Lemma cap1dot x y: 1 ∩ x*y == dom (x∩y`).
Proof. now rewrite domcap, cnvI. Qed.

Lemma dom_2pdef `{p2t<<l} x: dom x == 1 ∩ x*top.
Proof. rewrite cap1dot. now rewrite cnvtop, capxt. Qed.

Lemma domtst {a} {Ha: tst a}: dom a == a.
Proof. rewrite <-Ha, capC, domcap, cnv1, dotx1. apply capC. Qed.

Lemma cnvtst {a} {Ha: tst a}: a` == a.
Proof. rewrite <-Ha, cnvcap, cnv1, <-(dot1x (a`)), <-domcap. apply domtst. Qed.

Global Instance tst_cnv {a} {Ha: tst a}: tst (a`).
Proof. unfold tst. now rewrite cnvtst. Qed.

Global Instance tst_dom x: tst (dom x).
Proof.
  unfold tst.
  destruct splitl1 as [->|[?|?]].
  rewrite <-(dotx1 (dom x)) at 2. rewrite <-cap11 at 2.
  rewrite dotacap_, dotx1 by reflexivity. apply capC.
  rewrite dom_2pdef. now rewrite capA,cap11.
  rewrite dom_aldef. now rewrite capA,cap11.
Qed.

Lemma dotax `{p2t<<l} {a} {Ha: tst a} x: a*x == a*top ∩ x.
Proof.
  destruct splitl0.
  rewrite <-Ha. apply dotax_. now destruct l.
  assert (alt<<l) by now destruct l.
  apply antisym. apply leq_xcap. lattice. now rewrite tst1, dot1x.
  now rewrite capdotx, captx, (tst1 (a:=a`)), dot1x.
Qed.

Lemma dotacap {a} {Ha: tst a} x y: a*(x∩y) == a*x ∩ y.
Proof.
  destruct splitl1 as [?|[?|?]].
  rewrite <-domtst. now apply dotacap_.
  rewrite dotax, (dotax x). apply capA.
  apply antisym. apply leq_xcap. lattice. rewrite tst1, dot1x. lattice.
  now rewrite capdotx, (tst1 (a:=a`)), dot1x.
Qed.

Lemma dottst {a b} {Ha: tst a} {Hb: tst b}: a * b == a ∩ b.
Proof. rewrite <-Hb at 1. now rewrite dotacap, dotx1. Qed.

Global Instance tst_dot {a b} {Ha: tst a} {Hb: tst b}: tst (a * b).
Proof. unfold tst. rewrite dottst. apply tst_cap1. Qed.

Lemma dom_cycle x y z: dom (x*y ∩ z) == dom (x ∩ z*y`).
Proof. now rewrite 2domcap, cnvdot, cnvI, dotA. Qed.

Global Instance tst_cod x: tst (cod x).
Proof. unfold tst. rewrite <-domcnv. apply tst_dom. Qed.

Lemma dotxt `{p2t<<l} x: x*top == dom x*top.
Proof.
  assert (E: l=p2t ∨ all<<l ∧ alt<<l) by (destruct l; intuition contradiction).
  destruct E as [?|[??]]. now apply dotxt_.
  apply antisym.
  rewrite dom_2pdef.
  transitivity (1*top ∩ x*top). now rewrite dot1x, captx.
  now rewrite capdotx', <-dotA, (leq_xt (top*top`)).
  now rewrite dom_aldef, cap2, <-dotA, (leq_xt (x`*top)).
Qed.

Lemma dotC {a b} {Ha: tst a} {Hb: tst b}: a*b == b*a.
Proof. rewrite 2dottst. apply capC. Qed.

Lemma dotI `{all<<l} {a} {Ha: tst a}: a*a == a.
Proof. rewrite dottst. apply capI. Qed.

Lemma xdomdot `{all<<l} x y: x∩y <== x*(1 ∩ x`*y).
Proof. rewrite <-(dotx1 x) at 1. now rewrite capdotx. Qed.

Lemma domdot x y: dom (x*y) == dom (x * dom y).
Proof.
  destruct splitl1 as [->|[Hl|Hl]].
  now apply domdot_.
  now rewrite dom_2pdef, <-dotA, dotxt, dotA, <-dom_2pdef.
  apply antisym.
  rewrite dom_aldef, cnvdot, dotA, <-domcap. apply dom_leq.
  set (z:=x*y). rewrite capC, xdomdot. apply dot_leq; trivial.
  now rewrite dotA, <-domcap, cap2.
  rewrite dom_aldef, cnvdot, cnvtst, dotA, <-(dotA _ _ (dom _)), dotI.
  now rewrite 2dom_aldef, (cap2 1 (y*_)), dotA, cnvdot, !dotA.
Qed.

Lemma domax {a} {Ha: tst a} x: dom (a*x) == a*dom x.
Proof. rewrite domdot. apply domtst. Qed.

Lemma domxa `{all<<l} {a} {Ha: tst a} x: dom (x*a) <== x*a*x`.
Proof. rewrite dom_aldef, cnvdot, (tst1 (a:=a`)), dot1x. lattice. Qed.

Lemma domxx `{all<<l} x: x == dom x * x.
Proof.
  apply antisym.
  rewrite dom_aldef. now rewrite <-capdotx', dot1x, capI.
  now rewrite tst1, dot1x.
Qed.

Lemma codcnv x: cod (x`) == dom x.
Proof. now rewrite <-domcnv, cnvI. Qed.

Lemma dottx `{p2t<<l} x: top*x == top*cod x.
Proof. cnv_switch. now rewrite <-domcnv, dotxt, cnvtst. Qed.

Lemma coddot x y: cod (y*x) == cod (cod y * x).
Proof. rewrite <-3domcnv, 2cnvdot, cnvtst. apply domdot. Qed.

Lemma codcap x y: cod (x∩y) == 1 ∩ y`*x.
Proof. now rewrite cap1dot, <-domcnv, cnvcap, capC. Qed.

Lemma dotxa `{p2t<<l} {a} {Ha: tst a} x: x*a == top*a ∩ x.
Proof. cnv_switch. apply dotax. Qed.

Lemma dotcapa {a} {Ha: tst a} x y: (x∩y)*a == x*a ∩ y.
Proof. cnv_switch. apply dotacap. Qed.

Lemma cod_aldef `{all<<l} x: cod x == 1 ∩ x`*x.
Proof. rewrite <-domcnv, dom_aldef, <-cnvtst. now simplify. Qed.

Lemma cap1xdom `{all<<l} x: 1∩x <== dom x.
Proof.
  rewrite dom_aldef. apply leq_xcap. apply cap1.
  rewrite <-capI, <-dottst. apply dot_leq. apply cap2.
  rewrite <-cnvtst. now rewrite cap2.
Qed.

End s'.

Inclusions of theories

all structures are 2pdom algebras (gives Lem. 41 when h=all)
Proposition laws_2p h X (L: laws h X): laws p2d X.
Proof.
  constructor; simpl; intros; try solve [discriminate | now destruct L].
  apply domdot.
  apply dotacap.
  apply cap11.
  apply domcap.
  apply dom_weq.
Qed.

every allegory with top is an allegory
Proposition laws_altal X (L: laws alt X): laws all X.
Proof.
  constructor; simpl; intros; try solve [discriminate | now destruct L].
  apply dot_leq.
  apply leq_spec.
  apply dom_aldef.
  apply capdotx.
  apply capI.
Qed.

every allegory with top is a 2p-algebra (Prop. 18)
Proposition laws_alt2pt X (L: laws alt X): laws p2t X.
Proof.
  constructor; simpl; intros; try solve [discriminate | now destruct L].
  apply captx.
  apply dotxt.
  apply dotax.
  apply cap11.
  apply domcap.
  apply dom_weq.
Qed.

Summing up, we indeed have a lattice of equational theories
Theorem laws_dec X h k: h<<k → laws k X → laws h X.
Proof.
  destruct h; destruct k; try contradiction; intros _;
  eauto using laws_alt2pt, laws_altal, laws_2p.
Qed.

Duality reasonning

We show that every algebra gives rises to a dual one, where composition is reversed and cod/dom are exchanged
This makes it possible to exploit duality arguments in a streamlined way
Definition dual (X: ops) := {|
  car := X;
  leq := leq;
  weq := weq;
  dot x y := y*x;
  cap := cap;
  cnv := cnv;
  dom := cod;
  cod := dom;
  one := one;
  top := top
|}.
Notation "X ^op" := (dual X) (at level 1): ra_scope.

the construction is uniform and works for the four equational theories
Proposition dual_laws {l} {X} {L: laws l X}: laws l X^op.
Proof.
  constructor; intros; simpl; try subst l.
   apply L.
   intros ??????. simpl. now apply dot_weq.
   apply L.
   intros ???. simpl. now apply cnv_weq.
   symmetry. apply dotA.
   apply dotx1.
   apply capA.
   apply capC.
   apply cnvdot.
   apply cnvcap.
   apply cnvI.
   apply codcnv.
   apply captx.
   apply dottx.
   apply dotxa.
   apply coddot.
   apply dotcapa.
   apply cap11.
   apply codcap.
   intros ???. simpl. now apply cod_weq.
   intros ??????. simpl. now apply dot_leq.
   apply leq_spec.
   apply cod_aldef.
   apply capdotx'.
   apply capI.
Qed.

Lemma dualize {P: ops → Prop} (L: ∀ l X, laws l X → P X)
  {l X} {H: laws l X}: P (dual X).
Proof. apply L with l. now apply dual_laws. Qed.

Lemma dualize' {h} {P: ops → Prop} (L: ∀ l X, laws l X → h<<l → P X)
  {l X} {H: laws l X} {Hl:h<<l}: P (dual X).
Proof. apply L with l. now apply dual_laws. assumption. Qed.

Ltac dual x := apply (dualize x) || apply (dualize' x).

below we complete our set of lemmas by duality

Section d.
Context {l} {X} {L: laws l X}.

Lemma cap1dot' x y: 1 ∩ y*x == cod (x∩y`).
Proof. dual @cap1dot. Qed.

Lemma cod_2pdef `{p2t<<l} x: cod x == 1 ∩ top*x.
Proof. dual @dom_2pdef. Qed.

Global Instance cod_leq `{all<<l} : Proper (leq ==> leq) cod.
Proof. dual @dom_leq. Qed.

Lemma cod_cycle x y z: cod (y*x ∩ z) == cod (x ∩ y`*z).
Proof. dual @dom_cycle. Qed.

Lemma codtst {a} {Ha: tst a}: cod a == a.
Proof. now dual @domtst. Qed.

Lemma codxa {a} {Ha: tst a} x: cod (x*a) == cod x*a.
Proof. now dual @domax. Qed.

Lemma codax `{all<<l} {a} {Ha: tst a} x: cod (a*x) <== x`*a*x.
Proof. rewrite <-dotA. now dual @domxa. Qed.

Lemma xcodx `{all<<l} x: x == x * cod x.
Proof. dual @domxx. Qed.

Lemma cap1xcod `{all<<l} x: 1∩x <== cod x.
Proof. dual @cap1xdom. Qed.

End d.

Conservativity results (Sect. 8 in the paper)


Module conservativity.
Section s.

Assuming an arbitrary structure X, we construct the extended one, X', as in Def. 37
  Context {l} {X} {L: laws l X}.
  Inductive X' :=
  | c(x: X)
  | d: ∀ (a b: X) {Ha: tst a} {Hb: tst b}, X'.

  Definition weq' x y :=
    match x,y with
    | c x,c y ⇒ x==y
    | d a b, d a' b' ⇒ a==a' ∧ b==b'
    | _,_ ⇒ False
    end.
  Definition leq' x y :=
    match x,y with
    | c x,c y ⇒ x<==y
    | d a b, d a' b' ⇒ a<==a' ∧ b<==b'
    | c x, d a b ⇒ x<==a*x*b
    | _,_ ⇒ False
    end.
  Definition dot' x y :=
    match x,y with
    | c x,c y ⇒ c (x*y)
    | d a _, d _ b ⇒ d a b
    | c x, d a b ⇒ d (dom (x*a)) b
    | d a b, c y ⇒ d a (cod (b*y))
    end.
  Definition cap' x y :=
    match x,y with
    | c x,c y ⇒ c (x∩y)
    | d a b, d a' b' ⇒ d (a∩a') (b∩b')
    | c z, d a b
    | d a b, c z ⇒ c (a*z*b)
    end.
  Definition cnv' x :=
    match x with
    | c x ⇒ c (x`)
    | d a b ⇒ d b a
    end.
  Definition dom' x :=
    match x with
    | c x ⇒ c (dom x)
    | d a b ⇒ c a
    end.
  Definition cod' x :=
    match x with
    | c x ⇒ c (cod x)
    | d a b ⇒ c b
    end.
  Definition one' := c 1.
  Definition top' := d 1 1.

  Definition eX: ops := {|
      car := X';
      leq := leq';
      weq := weq';
      dot := dot';
      cap := cap';
      cnv := cnv';
      dom := dom';
      cod := cod';
      one := one';
      top := top'
    |}.

Conservativity of 2p over 2pdom.
Note that we have L: laws l X in the local context,
Prop. 39 follows by taking l=2pd.
  Theorem eX_p2t: laws p2t eX.
  Proof.
    constructor; try contradiction || discriminate.
    - constructor.
     -- now intros [x|a b]; simpl.
     -- intros [x|a b] [y|a' b']; simpl; try contradiction.
        now intro; symmetry.
        now intros [??]; split; symmetry.
     -- intros [x|a b] [y|a' b'] [z|a'' b'']; simpl; try contradiction.
        intros; etransitivity; eassumption.
        intros [??] [??]; split; etransitivity; eassumption.
    - intros [x|a b] [x'|a' b'] H [y|e f] [y'|e' f'] H'; try contradiction; simpl in *.
      now apply dot_weq.
      destruct H' as [-> ->]; now rewrite H.
      destruct H as [-> ->]; now rewrite H'.
      tauto.
    - intros [x|a b] [x'|a' b'] H [y|e f] [y'|e' f'] H'; try contradiction; simpl in *.
      now apply cap_weq.
      destruct H' as [-> ->]; now rewrite H.
      destruct H as [-> ->]; now rewrite H'.
      now destruct H as [-> ->]; destruct H' as [-> ->].
    - intros [x|a b] [x'|a' b'] H; try contradiction; simpl in *.
      now apply cnv_weq.
      tauto.
    - intros [x|a b] [x'|a' b'] [x''|a'' b'']; simpl; intuition try reflexivity.
      apply dotA.
      now rewrite <-domdot, dotA.
      now rewrite <-coddot, dotA.
    - intros [x|a b]; simpl; intuition try reflexivity.
      apply dot1x.
      rewrite dot1x. apply domtst.
    - intros [x|a b] [x'|a' b'] [x''|a'' b'']; simpl; intuition try reflexivity.
      apply capA.
      now rewrite capC, <-dotcapa, <-dotacap, capC.
      now rewrite capC, <-2dotcapa, <-2dotacap, capC.
      now rewrite capC, <-2dottst, !dotA.
      now rewrite <-dotcapa, <-dotacap.
      now rewrite !dotA, dotC, <-!dotA, dotC.
      now rewrite <-dottst,capC,<-dottst,!dotA.
      apply capA.
      apply capA.
    - intros [x|a b] [x'|a' b']; simpl; intuition try reflexivity; apply capC.
    - intros [x|a b] [x'|a' b']; simpl; intuition try reflexivity.
      apply cnvdot.
      now rewrite <-codcnv, cnvdot, cnvtst.
      now rewrite <-domcnv, cnvdot, cnvtst.
    - intros [x|a b] [x'|a' b']; simpl; intuition try reflexivity.
      apply cnvcap.
      now rewrite 2cnvdot, 2cnvtst, dotA.
      now rewrite 2cnvdot, 2cnvtst, dotA.
    - intros [x|a b]; simpl; intuition try reflexivity.
      apply cnvI.
    - intros [x|a b]; simpl; intuition try reflexivity.
      apply domcnv.
    - intros _ [x|a b]; simpl; intuition try reflexivity.
      now rewrite dotx1,dot1x.
    - intros _ [x|a b]; simpl; intuition try reflexivity.
      now rewrite 2dotx1, domtst.
      now rewrite dotx1, domtst.
    - intros _ [x|a b] [z'|a' b']; simpl; intuition.
      now rewrite 2dotx1, domtst.
      rewrite dotx1, 2domtst, dottst. lattice.
      now rewrite Hb.
      now rewrite domtst, !dotx1.
      rewrite !dotx1, 2domtst, !dottst. lattice.
      now symmetry.
    - intros _; simpl. apply cap11.
    - intros _ [x|a b] [x'|a' b']; simpl; intuition try reflexivity.
      apply domcap.
      now rewrite dotx1, dotC, <-domax, dotA.
      now rewrite dotx1, dotC, <-codxa, <-codcnv, 2cnvdot, 2cnvtst, dotA.
      now rewrite dotx1, dottst.
    - intros _ [x|a b] [x'|a' b'] H; try contradiction; simpl in *.
      now apply dom_weq.
      tauto.
  Qed.
End s.
Section s'.
Conservativity of allegories with top over allegories.
Prop. 43 follows by taking l=all.
  Context {l} {X} {L: laws l X} {Hl: all<<l}.
  Theorem eX_alt: laws alt eX.
  Proof.
by trying to use eX_p2t (Prop. 39 + Lem. 41), we get only a few laws to prove
    pose proof eX_p2t as L'.
    constructor; try solve [apply L'|contradiction|discriminate]; intros _.
    - intros [x|a b] [x'|a' b'] H [y|e f] [y'|e' f'] H'; simpl in *; intuition.
      -- now apply dot_leq.
      -- rewrite H' at 1. rewrite !dotA, (domxx (x*e')).
         rewrite (tst1 (a:=e')) at 2. rewrite H at 1. now rewrite dotx1.
      -- apply dom_leq; now apply dot_leq.
      -- rewrite H at 1. rewrite <-!dotA, (xcodx (b'*y)).
         rewrite (tst1 (a:=b')) at 1. rewrite H' at 2. now rewrite dot1x.
      -- rewrite H at 1. rewrite H' at 1.
         now rewrite (tst1 (a:=b')), (tst1 (a:=e')), dot1x, dotx1, !dotA.
      -- now rewrite H, <-!dotA, domax, (tst1 (a:=dom _)), dotx1.
      -- apply cod_leq; now apply dot_leq.
      -- now rewrite H', !dotA, codxa, (tst1 (a:=cod _)), dot1x.
    - intros [x|a b] [y|e f]; simpl.
      -- apply leq_spec.
      -- split. intro H. apply antisym; trivial. now rewrite tst1, dot1x, tst1, dotx1.
         rewrite weq_spec. tauto.
      -- tauto.
      -- rewrite 2leq_spec. tauto.
    - intros [x|a b]; simpl.
      -- apply dom_aldef.
      -- now rewrite dotx1, dotI.
    - intros [x|a b] [y|e f] [z|g h]; simpl; intuition.
      -- apply capdotx.
      -- rewrite 2dotA, (xcodx (g*x)), tst1 at 1.
         now rewrite dot1x, <-domcnv, cnvdot, cnvtst, dotA.
      -- now rewrite domxa, !dotA.
      -- rewrite <-(dottst (a:=e)), dotA, <-domdot, !dotA, (domdot _ g).
         rewrite <-(cap1xdom (_*dom _)), cap1dot, domtst.
         rewrite <-mk_tst, domxa. apply leq_xcap.
         now rewrite cap2, cap1.
         rewrite (cap2 _ g), cnvtst. apply cap1xdom.
      -- rewrite !dotA, 2dotI, codxa.
         rewrite <-!dotA, (dotA (cod _)), dotI, dotC, !dotA.
         now rewrite <-xcodx.
      -- apply cap1.
      -- rewrite 2dotA, dotI.
         rewrite <-(cap2 1 h) at 2. rewrite codxa, dottst.
         now rewrite capA, (capC _ 1), mk_tst.
      -- rewrite <-dottst,!dotA, dotI, <-!dotA, 2(dotC (a:=f)), <-dotA, dotI, !dotA.
         now rewrite <-xcodx.
      -- apply cap1.
    - intros [x|a b]; simpl.
      -- apply capI.
      -- split; apply capI.
  Qed.
End s'.
End conservativity.