Coq証明言語に「それ以上の副目標はありませんが、インスタンス化されていない実在変数がありますか？

Question

私は、第11章のCoq 8.5p1のリファレンスマニュアルの数学的/宣言的証明言語についての例を（不完全な）例に従っていました。反復等式（~=と=~）については、以下の例では、私は2+2へ4を書き換えるための警告Insufficient Justificationを得て、最終的に言ってエラーを得た：

これ以上のサブゴールを、しかし非インスタンス化実存 変数があります：

目標：[X：RH：x = 2の_eq0：= X * X 4 | - 2 + 2 = 4]？

あなたはグラブ実存変数を使用することができます。

例：

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. 

私はCoqの中に数学的な証明の言語に精通していないよ、これがなぜ起こるか理解できませんでした。誰かがエラーを修正する方法を説明するのを助けることができますか？

--EDIT-- @Vinz

私は例の前にこれらのランダム輸入していた：

Require Import Reals. 
Require Import Fourier. 

Answer 1

あなたの証明はnatまたはZのために働くだろうが、それはRの場合に失敗します。

コックReference Manual（V8.5）から：

宣言プルーフ言語の目的は、中間状態は、常にユーザによって与えられる逆のアプローチをとることであるが、システムの遷移があります可能な限り自動化されています。

4 = 2 + 2の自動化に失敗したようです。私は、宣言証明エンジンを使用して自動化の種類を知らないが、例えば、auto戦術は、このように、ほとんどすべての単純な等式を証明することができません。

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

そして@ejgallego points out我々として唯一のチャンスでautoを使用して2 * 2 = 4を証明することができます

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

しかし、field戦術は魔法のように動作します。だから、一つのアプローチはfield戦術を使用して、宣言証明エンジンを提案することです：

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. 

Answer 2

ここでの問題は、コックの標準的な実数は公理的な方法で定義されていることです。

したがって、+ : R -> R -> Rおよび*などは抽象的な操作であり、決して計算されません。これは何を意味するのでしょうか？、したがって、

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

：それはコックのコックがい​​ることを知っているNAT場合に+、例えば逆をどうするかのルールを持っていないことを意味します実数のために+を操作する唯一の方法は、オペレータを特徴付ける対応する公理を手動で適用することです。

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

これはfield, omegaなどです。 0 + 1 = 1さえも計算ではありません。

アントンの例2 + 2 = 4は偶然に動作します。実際には、Coqは実際の公理を使用して数字4を適切な表現に解析しなければならず、4はRmult (Rplus R1 R1) (Rplus R1 R1)（より効率的である）として解析されていることが判明しています。これは以前の等価性の左側と同じです。