# Trying to prove an alga's axiom, a tale of a weekend

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!