Как доказать (2 ^ 2)% R = 4% R - PullRequest
Новая
       61

Как доказать (2 ^ 2)% R = 4% R

2 голосов
/ 01 мая 2020

Как доказать следующее в Coq? 

Require Import Coq.Reals.Reals.

Definition f (x:R) :R := pow x 2.

Lemma f_2: f 2 = 4%R.
Proof.
Admitted.

Ответы [ 2 ]

3 голосов
/ 01 мая 2020

Подход 1: используйте мощные такти c.

ring такти c достаточно мощный, чтобы легко объединить 2^2 и 4. Вам придется развернуть f, поскольку это не кольцевая операция. 

Lemma f_2: f 2 = 4%R.
Proof.
  unfold f.
  ring.
Qed.

Подход 2: трудный путь. Чтобы увидеть все, что подразумевается в простом утверждении f 2 = 4, поможет временно отключить нотацию. Я также открыл область действия R_scope, чтобы везде мне не требовался суффикс * 1013.

Получается что-то вроде eq (f (IZR (Zpos (xO xH)))) (IZR (Zpos (xO (xO xH))))

IZR - функция, которая преобразует целые числа на реальные цифры. Давайте развернем это, а также f.

Теперь мы можем снова включить нотацию, и в качестве цели мы получим IPR 2 ^ 2 = IPR 4. Так что продолжайте, развернув IPR. (IPR преобразует положительные целые числа в действительные числа).

Тогда цель IPR_2 1 ^ 2 = IPR_2 2. IPR_2 также преобразует натуральные числа в вещественные числа, но вводит коэффициент 2. Это в основном вспомогательная функция для IPR. Разверните его тоже.

Наконец-то мы подошли к базовым c константам. Цель - (R1 + R1) ^ 2 = (R1 + R1) * (R1 + R1). Давайте упростим власть. Одна из тактик упрощения вроде cbn будет работать. Цель становится (R1 + R1) * ((R1 + R1) * 1) = (R1 + R1) * (R1 + R1). Итак, наконец, мы можем использовать это x * 1 = x. В поисках "*" (еще лучше Search (?x * 1 = ?x).) я обнаружил, что Rmult_1_r - это то, что мы хотим. Используйте rewrite Rmulti_1_r, а затем reflexivity. 

Lemma f_2: f 2 = 4.
Proof.
  unfold f, IZR.
  unfold IPR.
  unfold IPR_2.
  cbn.
  (* Search (?x * 1 = ?x). *)
  rewrite Rmult_1_r.
  reflexivity.
Qed.

Конечно, все эти развертываемые шаги являются чисто вычислительными, поэтому мы могли бы пропустить до конца, сказав что-то вроде change 4 with (2 * 2)., но это определенно не очевидно 4 определено как 2 * 2, если вы уже не знакомы с тем, как целые числа переводятся в действительные числа. 

Lemma f_2: f 2 = 4.
Proof.
  unfold f; cbn.
  change 4 with (2 * 2).
  rewrite Rmult_1_r.
  reflexivity.
Qed.
1 голос
/ 01 мая 2020

Сначала нужно раскрыть определение функции f, «развернув» ее: 

Require Import Coq.Reals.Reals.  (* "Require Import Reals." would be OK as well. *)
Definition f (x : R) : R := pow x 2.

Lemma f_2 : f 2 = 4%R.
Proof.
unfold f.

Затем вы получите: 

1 subgoal

  ============================
  (2 ^ 2)%R = 4%R

и один идиоматический c способ для достижения этой цели над аксиоматизированными реалами стоит положиться на ring tacti c: 

ring.
Qed.

Подробнее об этой тактике c см. официальный Coq do c.

...