This is the story of my semi-lost weekend, since I tried to prove something, but I ended proving it was false. This is the story in my step into the (fabulous ?) world of computer-validated logic.

Using Agda

A cool part with alga is that it is based on tangible mathematical results and thus, some behaviors can be proved. Thanks to the mind-blowing Curry Howard correspondence, we can prove it using a computer !

Already a good part is described in Agda, a proof assistant written “à la Haskell” here: https://github.com/algebraic-graphs/agda/.

I am more used to Coq (a proof-assistant “à la OCaml”), because it is actually developed by some of my teachers, but I started to read the code.

A cool feature of Agda is the simplicity of working with functions !

Alga’s agda

Actually, there is the core of the Agda code:

data Graph (A : Set) : Set where
    ε   : Graph A                       -- Empty graph
    v   : A -> Graph A                  -- Graph comprising a single vertex
    _+_ : Graph A -> Graph A -> Graph A -- Overlay two graphs
    _*_ : Graph A -> Graph A -> Graph A -- Connect two graphs

data __ {A} : (x y : Graph A) -> Set where
    -- Equivalence relation
    reflexivity  :  {x     : Graph A} ->                   x  x
    symmetry     :  {x y   : Graph A} -> x  y ->          y  x
    transitivity :  {x y z : Graph A} -> x  y -> y  z -> x  z

    -- Congruence
    +left-congruence  :  {x y z : Graph A} -> x  y -> x + z  y + z
    -- +right-congruence holds as a theorem
    *left-congruence  :  {x y z : Graph A} -> x  y -> x * z  y * z
    *right-congruence :  {x y z : Graph A} -> x  y -> z * x  z * y

    -- Axioms of +
    +commutativity :  {x y : Graph A}   -> x + y        y + x
    +associativity :  {x y z : Graph A} -> x + (y + z)  (x + y) + z

    -- Axioms of *
    *left-identity  :  {x     : Graph A} -> ε * x        x
    *right-identity :  {x     : Graph A} -> x * ε        x
    *associativity  :  {x y z : Graph A} -> x * (y * z)  (x * y) * z

    -- Other axioms
    left-distributivity  :  {x y z : Graph A} -> x * (y + z)  x * y + x * z
    right-distributivity :  {x y z : Graph A} -> (x + y) * z  x * z + y * z
    decomposition :  {x y z : Graph A} -> x * y * z  x * y + x * z + y * z

So, if we have a relation for which all the axioms holds, then the proved results (like idempotence of +) holds (major theorems can be found here).

It seems very quickly strange to have the congruences axioms. I believed that x ≡ y -> f x ≡ f y was holding as a theorem. I investigated, and the actual implementation of the alga standard library actually stands that (see here):

infix 4 __
data __ {a} {A : Set a} (x : A) : A  Set a where
  instance refl : x  x

cong :  {a b} {A : Set a} {B : Set b} (f : A  B) {x y}  x  y  f x  f y
cong f refl = refl

But this is not trivial at all, this stackoverflow answer will explain it better than me.

So this does not hold with alga’s .

The library author quickly showed my a counter-example:

-- Replace all overlays with connects, essentially producing something similar
-- to a transitive closure, but not exactly it.
-- This is a cruel function: I added it to demonstrate that from x ≡ y we cannot
-- in general conclude that f x ≡ f y. Indeed:
--                 x ≡ x + x
--           close x ≡ x
--     close (x + x) ≡ x * x
close :  {A} -> Graph A -> Graph A
close ε       = ε
close (v x)   = v x
close (x + y) = x * y
close (x * y) = x * y

Is *right-identity provable ?

So let’s search for other unnecessary axioms. I thought I found that

*right-identity :  {x : Graph A} -> x * ε  x

could be deduced from

*left-identity :  {x : Graph A} -> ε * x  x

In fact, my idea was to use:

transpose :  {A} -> Graph A -> Graph A
transpose ε       = ε
transpose (v x)   = v x
transpose (x + y) = transpose x + transpose y
transpose (x * y) = transpose y * transpose x

It is easy to prove that transpose is involutive (an involution is function a function f such as f (f x) == x). In agda that is to define:

transpose-inv :  {A} {x : Graph A} -> transpose (transpose x)  x

Next, the idea was:

*right-identity :  {A} {x : Graph A} -> x * ε  x
*right-identity : {_} {x} =
  begin
    x * ε                         ≡⟨ symmetry transpose-inv 
    transpose (transpose (x * ε)) ≡⟨ reflexivity 
    transpose (ε * transpose x)   ≡⟨ anAdaptedVersionOfCong *left-identitiy 
    transpose (transpose x)       ≡⟨ transpose-inv 
    x
  

It seems obvious to me that

anAdaptedVersionOfCong :  {A} {x y : Graph A} -> x  y -> transpose x  transpose y

was true.

I spent some hours trying to prove it… And then I recall that we wasn’t playing with the graph equality, or even with the graph isomorphism as : it’s definition states only that is an equivalence relation with some axioms.

And thus, maybe I can find a relation that broke what I am trying to prove. And, you have guessed it, it is the case. Let’s take the relation R

x R y = hasEdge 0 1 x == hasEdge 0 1 y

It is of course an equivalence relation, and congruence axioms holds.

And here is the sad truth:

let x = 0 * 1 + 1 * 0 :: Graph Int
let y = 0 * 1 :: Graph Int

x R y == True

-- BUT

transpose x == 1 * 0 + 0 * 1 
transpose y == 1 * 0

-- THUS

(transpose x) R (transpose y) == False

So what I was trying to prove (anAdaptedVersionOfCong) is not provable. I will sleep well tonight :) .

But this leads to other questions:

  • Is there functions non-trivial for which cong can be defined ?
  • Concerning equality: https://en.wikipedia.org/wiki/Equality_(mathematics) states that cong can be seen as the definition of equality. So is there a specialized version of alga’s for which cong can be defined ?

All of this to say that never forget to take a step back and look at what you are trying to prove!