Library allegories
From 2pdom to allegories with top
- 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
alt / \ 2pt all \ / 2pd
- 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)
Basic definitions
- in 2pdom, the constant top will be unspecified
- in alltop and in 2p, dom is axiomatised by its term definition
carrier
preorder
equality
product
intersection
converse
domain
codomain
neutral element (1)
top element
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.
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
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.
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 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;
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
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;
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;
}.
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.
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)
Basic laws
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.
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.
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'.
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.
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.
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.
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.
Proof.
destruct h; destruct k; try contradiction; intros _;
eauto using laws_alt2pt, laws_altal, laws_2p.
Qed.
Duality reasonning
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.
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).
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.
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'
|}.
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'.
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.
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.
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.