Is Coq able to prove the identity x = x for infinite precision real numbers?

Miscellaneous
1

Hi all,

I come from a computational complexity background and I think I have spotted an huge blunder in Classical logic.

There is a conflation between identity and value in symbols, but there is a clear distinction between these concepts on a Turing machine.

IDENTITY means “memory address” (a unique identifier)
VALUE means “contents-of-memory address.”

Classical logic overloads “=” to mean both identity and equality. Thus leading to a massive blunder.
It mistakes the complex for the simple.

From Curry-Howard isomorphism it follows that proofs compute. And computation is work. And work requires energy.

Therefore rather than assuming that x = x => true some amount of work needs to be done as proof-of-work. And so trying to prove that x = x for an infinite-precision value should take infinite time e.g the turing machine will not halt.

Proving x = x for Integer(1) is trivial complexity.
Proving x = x for infinite-precision float is infinite complexity.

In x = x hides the principle of explosion itself! Complexity explosion.

So my question : Is Coq capable of “proving” that x = x for infinite precision real numbers?
If so - how is this implemented. A simple “return true” ?

2

In Coq, proving x=x is trivial for every x of every type:

Goal forall (X : Type), forall (x : X), x = x.
Proof. intros X x. apply eq_refl. Qed.

Note that this also works for the case that x is “infinite” in some sense. But it is not always possible to prove x=y in case of infinite data structures (see in the link below).

In the standard library of Coq, reals are not defined constructively. Rather, we assume a set of axioms, for example the existence of a type R of reals, together with the usual axioms of real numbers. Using the axioms, we can construct new reals, and prove theorems about them. For example, there is a theorem that says cos (2*PI) = 1. So an identity proof for reals can be seens as a derivation from the axioms of reals, rather then a “computation of infinite precission”.

However, this doesn’t mean that Coq doesn’t support the notion of “infinite data structures” or “infinite computations/proofs”. They are called “co-inductive types” and “coinduction” in Coq.

It follows a minimal example, how we can define and use streams (i.e. infinite sequences) of natural numbers in Coq. I will also show at which point we have to introduce the notion of “infinite proof”.

Require Import Setoid.

(** Define streams as an infinite list of numbers *)
CoInductive stream :=
| stream_cons : nat -> stream -> stream.


(** As long as we only do finite computations, we can still compute and show equalities *)
Definition hd (s : stream) : nat :=
  match s with
  | stream_cons x s' => x
  end.

Lemma hd_correct (s s' : stream) (x : nat) :
  s = stream_cons x s' ->
  hd s = x.
Proof. intros ->. reflexivity. Qed.


Definition tl (s : stream) : stream :=
  match s with
  | stream_cons x s' => s'
  end.

Lemma tl_correct (s s' : stream) (x : nat) :
  s = stream_cons x s' ->
  tl s = s'.
Proof. intros ->. reflexivity. Qed.

Lemma stream_eta (s : stream) :
  s = stream_cons (hd s) (tl s).
Proof. destruct s. reflexivity. Qed.



(** [constant x] is the stream that only consists of [x]s. *)
CoFixpoint constant (x : nat) : stream := stream_cons x (constant x).


Lemma constant_hd (x : nat) :
  hd (constant x) = x.
Proof. reflexivity. Qed.

Lemma constant_tl (x : nat) :
  tl (constant x) = constant x.
Proof. reflexivity. Qed.


Lemma constant_correct (x : nat) :
  constant x = stream_cons x (constant x).
Proof.
  rewrite stream_eta at 1.
  rewrite constant_hd, constant_tl.
  reflexivity.
Qed.



(** Add two stream *)
CoFixpoint add_streams (s1 : stream) (s2 : stream) : stream :=
  match s1, s2 with
  | stream_cons x s1', stream_cons y s2' => stream_cons (x+y) (add_streams s1' s2')
  end.

Lemma add_stream_hd (s1 s2 : stream) :
  hd (add_streams s1 s2) = hd s1 + hd s2.
Proof. destruct s1, s2. reflexivity. Qed.

Lemma add_stream_tl (s1 s2 : stream) :
  tl (add_streams s1 s2) = add_streams (tl s1) (tl s2).
Proof. destruct s1, s2. reflexivity. Qed.

Lemma add_streams_cons (s1 s2 : stream) (x y : nat) :
  add_streams (stream_cons x s1) (stream_cons y s2) = stream_cons (x+y) (add_streams s1 s2).
Proof.
  rewrite stream_eta at 1.
  rewrite add_stream_hd, add_stream_tl.
  reflexivity.
Qed.
  


(** Let's try to prove that if we add [constant 0] to a stream, we get the same stream *)
Lemma add_zero (s : stream) :
  add_streams s (constant 0) = s.
Proof.
  Fail cofix IH.
  (* This fails, because identity ([eq]) is not a co-inductive type. *)
Abort.


(** This property captures the idea of infinite proof/computation: In order to show that two streams are "equal", we have show that all the elements in the stream are identical. Note that it is not possible to proof [forall s1 s2, stream_eq s1 s2 -> s1 = s2]. *)
CoInductive stream_eq : stream -> stream -> Prop :=
| stream_eq_cons : forall (x : nat) (s1 s2 : stream), stream_eq s1 s2 -> stream_eq (stream_cons x s1) (stream_cons x s2).


(** The proof for this theorem is "infinite", because we need to show that all elements of the stream are equal *)
Lemma add_zero (s : stream) :
  stream_eq (add_streams s (constant 0)) s.
Proof.
  revert s. cofix IH. intros s.
  destruct s.
  rewrite constant_correct.
  rewrite add_streams_cons.
  rewrite <- plus_n_O. (* Here is the actual "computation": we need to show infinitely often that [x + 0 = x] *)
  constructor.
  apply IH.
Qed.

For more information about this topic, I would refer you to Chapter 5 of “Certified Programming with Dependent Types”

1 Like
3

Not sure whether related or not: Is it provable in Coq that 1 = 0.999…?

4

In Coq, x = x means that x is convertible to x. Convertibility is a quasi-syntactic relation [basically syntactic equality of programs modulo alpha, beta, and some form of eta], so indeed it is possible to decide, however it is not the case that all equal real numbers are convertible, as you point out.

A Turing machine for deciding convertibility is easy. In Coq, every term has a normal form, thus, first, normalize the term, then compare them syntactically. Note that this strategy is not used in practice as it is very expensive, so Coq implements a much more sophisticated convertibility strategy, and it fact it is one of the strongest features of the system.

5

There is a difference between having evidence of equalities, and the process of deciding equality for two arbitrary values (which can generate evidence when it succeeds). For real numbers, equality is undecidable, so in general comparing numbers for equality may not terminate. On the other hand, there are cases where we can prove equalities (without having to check them through a comparison); x = x is the simplest such case, but for example the equality eq_real (x + (y + z)) ((x + y) + z) can also be proved (in finite time), even if it describes an equality between infinite objects – I use eq_real here to emphasize that this may have to be limited to a user-defined notion of equality on reals which is less strict than the builtin equality of Coq’s logic.

Classical logic overloads “=” to mean both identity and equality. Thus leading to a massive blunder.

I believe that things are more subtle than that. As formalists, we are used to the idea that there are several different ways to look at our objects, ignoring some aspects in some circumstances and taking them into account in others, and most reasoning systems allow to represent objects in different ways to make these distinctions. Even in classical logic you can define reals as infinite objects and reason correctly about the decidability (for example) of operations on these objets.

I believe that starting from an over-simplified description and then talking about “massive blunder” is not really an appropriate way to communicate nuances about the various logics involved.

1 Like
6

The question boils down to “How does Coq” deal with the range-precision trade-off?
At some point you run out of memory…

Any claims for “arbitrary precision” trigger my spidey sense that somebody, somewhere is cheating physics.

7

Indeed, I am talking about the distinction between decidability and provability.
Whereas provability is axiomatic. Decidability is computational

If proofs compute (Curry-Howard isomorphism) I would think that provability mandates that a proof halts?

and from that perspective even the proof of the Z+ integers is undecidable. Because the set is infinite - the proof never halts.

Basically - I am taking a “finitist” perspective on Mathematics.

8

The short answer is that Coq does not, that’s up to you as the algorithm writer; usually you will provide some epsilon or some short of limit. If you are interested in constructive analysis and Coq you can check for example [1106.3448] Type classes for efficient exact real arithmetic in Coq

9

Many thanks. Paper added to my reading material.

I guess this boils down to the philosophy of Mathematics intersecting with the domain of information security.

If proofs compute (Curry-Howard), then exploiting the limits in the arbitrary range-precision choice is literally all one needs to leverage the principle of explosion and prove anything in Mathematics.

That’s basically how all buffer overflows work. Improper input validation…

10

This reply by Andrej Bauer on the question of the decidability of the reals might be helpful in this context. For example:

As you note, classically all sets have decidable equality. In fact, the statement “all sets have decidable equality” is equivalent to excluded middle.

11

It does not follow that proving x = x when x is infinite requires infinite work. In fact, it doesn’t follow that proving that x = x requires computing or testing whether x = x, because even in Curry-Howard systems, x = x still holds “axiomatically” (in the sense relevant to your distinction).
The problem here is that “proofs compute” is ambiguous shorthand for a very specific mathematical statement, and you seem to misread the shorthand because it is ambiguous. It is tempting to reason on this ambiguous shorthand, and what you write suggests that is what you might be doing, but that is bound to confuse you and produce nonsense sooner or later. Instead, you must study the formal definitions and reason on those.

Since later you write “prove anything in mathematics”, which is impossible, you might have indeed confused yourself. That’s the danger of informal discussions about mathematics; theorem provers can help avoid that danger.

12

even in Curry-Howard systems, x = x still holds “axiomatically” (in the sense relevant to your distinction).

This is not true. Curry-Howard systems are Turing complete. Turing machines are generalized as Lambda calculus which is basically search-and-replace ( Regular language - Wikipedia ). As such the “law” of identity is not fundamental e.g it’s not required for the logic-system to remain functional because all symbols can be interpreted contextually.

Demonstration is here: https://repl.it/@TodorGenov/Identity

In a constructive realm this is a proposition, not an axiom: A = A => True

Which is effectively the standard form of Hilbert’s Entscheidungsproblem and so there is a procedure (algorithm) to determine the correct answer.

Now, of course - any bit-wise comparison of infinite-length information streams will produce “True” as the result, but what you are ignoring is that comparing a stream of 1 bit and comparing a stream of infinite bits takes infinitely more time. Hence work.

Whereas x = x assumes it true axiomatically and ignores the cost-of-work. Time.

Instead, you must study the formal definitions and reason on those.

Indeed. Computer science is the study of formal systems. It all stems down from the Chomsky hierarchy.
I have been studying and practicing it for most of my life.

Unless, of course, you think Mathematics is exempt from being classified as a formal language?

The problem here is that “proofs compute” is ambiguous shorthand for a very specific mathematical statement, and you seem to misread the shorthand because it is ambiguous.

It may be a very ambiguous mathematical statement, but it is a very unambiguous and precise computer science statement. A halting algorithm which produces the correct result.

And all I can do to demonstrate to you the error in ignoring the amount of work required is this Gedankenexperiment. Look at these two (in?)equalities:

1 = 1
888888888888888888881 = 88888888888888888881

Notice how the truth-value of the first one is trivial to determine, but the 2nd one is harder for your brain.

x = x is actually an algorithm: equality(A,B). What you are really doing on a Turing machine is
A = 888888888888888888881
B = 88888888888888888881

( Observe how it got really easy to determine that A !=B when you compared their length? :wink: )
equality(A,B) => False

Assuming x = x is an error. You are taking infinite time(required to iterate over an infinite set) for granted.
Alas - this discussion will quickly devolve to Ultrafinitism.

The mathematics may be right, but the physics and the computer science doesn’t make sense…
And as history has shown us, the three fields are conjoined at the hip…

Computation is all about decidability. To ignore decidability while speaking about Curry-Howard is to speak of square circles.