Coq: Associativity of relational composition

Link:: https://stackoverflow.com/q/70377028

Display all goals and responses

Question

I am working on verifying a system based on relation algebra. I found D. Pous's relation algebra library popular among the Coq society.

https://github.com/damien-pous/relation-algebra

On this page, binary relation hrel is defined together with its relational composition hrel_dot.

http://perso.ens-lyon.fr/damien.pous/ra/html/RelationAlgebra.rel.html

In this library, a binary relation is defined as

Universe U.
Definition hrel (n m : Type@{U}) := n -> m -> Prop.

And the relational composition of two binary relations is defined as

Definition hrel_dot n m p (x : hrel n m) (y : hrel m p) : hrel n p :=
  fun i j => exists2 k, x i k & y k j.

I believe that the relational composition is associative, i.e.

Lemma dot_assoc :
  forall m n p q (x : hrel m n) (y : hrel n p) (z : hrel p q),
    hrel_dot m p q (hrel_dot m n p x y) z = hrel_dot m n q x (hrel_dot n p q y z).forall (m n p q : Type) (x : hrel m n) (y : hrel n p)
  (z : hrel p q),
hrel_dot m p q (hrel_dot m n p x y) z =
hrel_dot m n q x (hrel_dot n p q y z)

I got to the place where I think the LHS and RHS of the expressions are equivalent, but I have no clues about the next steps.

1 subgoal

  m : Type
  n : Type
  p : Type
  q : Type
  x : hrel m n
  y : hrel n p
  z : hrel p q
  ============================
  (fun (i : m) (j : q) =>
   exists2 k : p,
     exists2 k0 : n, x i k0 & y k0 k & z k j) =
  (fun (i : m) (j : q) =>
   exists2 k : n,
     x i k & exists2 k0 : p, y k k0 & z k0 j)

I don't know how to reason about the nested exists2, although the results seem straightforward by exchanging the variables k and k0.

A (Ana Borges): I'm not sure you can prove the equality of those two expressions, at least not without proof irrelevance. If you rewrite your goal as a logical equivalence things should be easier.

Answer

As Ana pointed out, it is not possible to prove this equality without assuming extra axioms. One possibility is to use functional and propositional extensionality:

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.PropExtensionality.

Universe U.
Definition hrel (n m : Type@{U}) := n -> m -> Prop.

Definition hrel_dot n m p (x : hrel n m) (y : hrel m p) : hrel n p :=
  fun i j => exists2 k, x i k & y k j.

Lemma dot_assoc :
  forall m n p q (x : hrel m n) (y : hrel n p) (z : hrel p q),
    hrel_dot m p q (hrel_dot m n p x y) z = hrel_dot m n q x (hrel_dot n p q y z).forall (m n p q : Type) (x : hrel m n) (y : hrel n p)
  (z : hrel p q),
hrel_dot m p q (hrel_dot m n p x y) z =
hrel_dot m n q x (hrel_dot n p q y z)
Proof.forall (m n p q : Type) (x : hrel m n) (y : hrel n p)
  (z : hrel p q),
hrel_dot m p q (hrel_dot m n p x y) z =
hrel_dot m n q x (hrel_dot n p q y z)
  intros m n p q x y z.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
hrel_dot m p q (hrel_dot m n p x y) z =
hrel_dot m n q x (hrel_dot n p q y z)
  apply functional_extensionality.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
forall x0 : m,
hrel_dot m p q (hrel_dot m n p x y) z x0 =
hrel_dot m n q x (hrel_dot n p q y z) x0 intros a.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
hrel_dot m p q (hrel_dot m n p x y) z a =
hrel_dot m n q x (hrel_dot n p q y z) a
  apply functional_extensionality.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
forall x0 : q,
hrel_dot m p q (hrel_dot m n p x y) z a x0 =
hrel_dot m n q x (hrel_dot n p q y z) a x0 intros b.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
hrel_dot m p q (hrel_dot m n p x y) z a b =
hrel_dot m n q x (hrel_dot n p q y z) a b
  apply propositional_extensionality.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
hrel_dot m p q (hrel_dot m n p x y) z a b <->
hrel_dot m n q x (hrel_dot n p q y z) a b
  unfold hrel_dot; split.m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
(exists2 k : p,
   exists2 k0 : n, x a k0 & y k0 k & z k b) ->
exists2 k : n, x a k & exists2 k0 : p, y k k0 & z k0 b
m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
(exists2 k : n,
   x a k & exists2 k0 : p, y k k0 & z k0 b) ->
exists2 k : p, exists2 k0 : n, x a k0 & y k0 k & z k b
  -m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
(exists2 k : p,
   exists2 k0 : n, x a k0 & y k0 k & z k b) ->
exists2 k : n, x a k & exists2 k0 : p, y k k0 & z k0 b intros [c [d ? ?] ?].m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
c: p
d: n
H: x a d
H0: y d c
H1: z c b
exists2 k : n, x a k & exists2 k0 : p, y k k0 & z k0 b eauto.
  -m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
(exists2 k : n,
   x a k & exists2 k0 : p, y k k0 & z k0 b) ->
exists2 k : p, exists2 k0 : n, x a k0 & y k0 k & z k b intros [c ? [d ? ?]].m, n, p, q: Type
x: hrel m n
y: hrel n p
z: hrel p q
a: m
b: q
c: n
H: x a c
d: p
H0: y c d
H1: z d b
exists2 k : p, exists2 k0 : n, x a k0 & y k0 k & z k b eauto.
Qed.