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:

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):

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:

## Is *right-identity provable ?

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

could be deduced from

In fact, my idea was to use:

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:

Next, the idea was:

It seems obvious to me that

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:

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!