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.
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-blowingCurry Howard correspondence, we can prove it using a computer !
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 !
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
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 ?