`No more subgoals, but there are non-instantiated existential variables` in Coq proof language?

2
votes

I was following (incomplete) examples in Coq 8.5p1 's reference manual in chapter 11 about the mathematical/declarative proof language. In the example below for iterated equalities (~= and =~), I got a warning Insufficient Justification for rewriting 4 into 2+2, and eventually got an error saying:

No more subgoals, but there are non-instantiated existential variables:

?Goal : [x : R H : x = 2 _eq0 : 4 = x * x |- 2 + 2 = 4]

You can use Grab Existential Variables.

Example:

Goal forall x, x = 2 -> x + x = x * x.
Proof. 
proof. Show.
let x:R. 
assume H: (x = 2). Show. 
have ( 4 = 4). Show.
~= (2*2). Show. 
~= (x*x) by H. Show.
=~ (2+2). Show. (*Problem Here: Insufficient Justification*)
=~ H':(x + x) by H.
thus thesis by H'.
end proof.
Fail Qed.

I'm not familiar with the mathematical proof language in Coq and couldn't understand why this happens. Can someone help explain how to fix the error?

--EDIT-- @Vinz

I had these random imports before the example:

Require Import Reals.
Require Import Fourier.
2
coq
Could you add the Require or library you use to have such a syntax ? – Vinz
Sorry I don't have a Coq 8.5 to test your script atm. Usually this happens when you manage to prove a goal but some metavariable (think holes with types, that you usually fill by solving a subgoal) was left un-instantiated. – Vinz

2 Answers

2
votes

Your proof would work for nat or Z, but it fails in case of R.

From the Coq Reference Manual (v8.5):

The purpose of a declarative proof language is to take the opposite approach where intermediate states are always given by the user, but the transitions of the system are automated as much as possible.

It looks like the automation fails for 4 = 2 + 2. I don't know what kind of automation uses the declarative proof engine, but, for instance, the auto tactic is not able to prove almost all simple equalities, like this one:

Open Scope R_scope.
Goal 2 + 2 = 4. auto. Fail Qed.

And as @ejgallego points out we can prove 2 * 2 = 4 using auto only by chance:

Open Scope R_scope.
Goal 2 * 2 = 4. auto. Qed.
(* `reflexivity.` would do here *)

However, the field tactic works like a charm. So one approach would be to suggest the declarative proof engine using the field tactic:

Require Import Coq.Reals.Reals.
Open Scope R_scope.
Unset Printing Notations.  (* to better understand what we prove *)
Goal forall x, x = 2 -> x + x = x * x.
Proof.
  proof.
  let x : R. 
  assume H: (x = 2).
  have (4 = 4).
  ~= (x*x) by H.
  =~ (2+2) using field.  (* we're using the `field` tactic here *)
  =~ H':(x + x) by H.
  thus thesis by H'.
  end proof.
Qed.
2
votes

The problem here is that Coq's standard reals are defined in an axiomatic way.

Thus, + : R -> R -> R and *, etc... are abstract operations, and will never compute. What does this mean? It means that Coq doesn't have a rule on what to do with +, contrary for instance to the nat case, where Coq knows that:

  • 0 + n ~> 0
  • S n + m ~> S (n + m)

Thus, the only way to manipulate + for the real numbers it to manually apply the corresponding axioms that characterize the operator, see:

https://coq.inria.fr/library/Coq.Reals.Rdefinitions.html https://coq.inria.fr/library/Coq.Reals.Raxioms.html

This is what field, omega, etc... do. Even 0 + 1 = 1 is not probable by computation.

Anton's example 2 + 2 = 4 works by chance. Actually, Coq has to parse the numeral 4 to a suitable representation using the real axioms, and it turns out that 4 is parsed as Rmult (Rplus R1 R1) (Rplus R1 R1) (to be more efficient), which is the same than the left side of the previous equality.