- Нет больше подцели, но там не создается экзистенциальные переменные в Кок язык доказательство?

Я следовал (неполным) примерам в справочном руководстве Coq 8. 5p1 в главе 11 о математическом / декларативном языке доказательства. В приведенном ниже примере для итерационных равенств (~= и =~) я получил предупреждение Insufficient Justification для перезаписи 4 в 2+2, и в конечном итоге получил ошибку, говорящую:

Больше нет подцелей, но есть не-инстанцированные экзистенциальные переменные:

?Цель : [x : R H: x = 2 _eq0 : 4 = x * x |- 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 и не мог понять, почему это происходит. Кто-нибудь может помочь объяснить, как исправить ошибку?

-- править-- @Vinz

У меня были эти случайные импорта перед примером: 

Require Import Reals.
Require Import Fourier.
2 2
coq

2 ответа:

Ваше доказательство будет работать для nat или Z, но оно не работает в случае R.

Из справочного руководства Coq (v8. 5):

Цель декларативного языка доказательства состоит в том, чтобы использовать противоположный подход, когда промежуточные состояния всегда задаются пользователем, но переходы системы максимально автоматизированы.

Похоже, что автоматизация не работает для 4 = 2 + 2. Я не знаю, какая автоматизация использует декларативное доказательство но, например, тактика auto не способна доказать почти все простые равенства, как это: 

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

И как указывает @ejgallego , мы можем доказать 2 * 2 = 4, используя auto только случайно: 

Open Scope R_scope.
Goal 2 * 2 = 4. auto. Qed.
(* `reflexivity.` would do here *)
Однако тактика

Работает как заклинание. Таким образом, один из подходов состоит в том, чтобы предложить механизм декларативного доказательства, используя тактику 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.
2

Проблема здесь заключается в том, что стандартные реалы Coq определяются аксиоматическим образом.

Таким образом, + : R -> R -> R и * и т. д... это абстрактные операции,и они никогда не будут вычисляться. Что это значит? Это означает, что Coq не имеет правила о том, что делать с +, в отличие, например, от случая nat, где Coq знает, что:

  • 0 + n ~> 0
  • S n + m ~> S (n + m)
Таким образом, единственный способ манипулировать + для действительных чисел-это вручную применять соответствующие аксиомы, что охарактеризуйте оператора, см.:

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) (чтобы быть более эффективным), что то же самое чем левая сторона предыдущего равенства.

2