Coq Вещественные числа - сбор и разбор 3.14

Question

С импортированной библиотекой Reals

Require Import Reals.

Как я могу определить константы, такие как 3.14 или 10.1, и использовать их для определения функции или вычисления?

Answer 1

Вы можете определить свои константы следующим образом:

Definition a := 10 + /10.
Definition b := 3 + 14/100.

Обратите внимание, однако, что стандартная библиотека определяет реалы аксиоматически. Вы можете найти основные определения здесь. Обратите внимание, что определения даны как Parameters, который является синонимом Axiom, Например, R0 а также R1 обозначать реальные цифры 0 и 1, Rplus а также Rmult представляют сложение и умножение, но эти определения не являются индуктивными типами данных и функциями, поскольку в них отсутствуют определения. Чтобы иметь возможность иметь дело с реалами, нам нужны аксиомы, регулирующие взаимодействие между ними (приведено здесь).

Вы можете думать о реальных числах в стандартной библиотеке как AST, сделанные с отмеченными узлами R0, R1, Rplus, и так далее. И вам даны некоторые правила (аксиомы), которые определяют (только) преобразования, которые вы можете выполнять с этими AST.

Давайте посмотрим, как Coq представляет действительные числа:

Require Import Coq.Reals.Reals.
Local Open Scope R_scope.
Unset Printing Notations.
Check 5+/2  (* 5½ *).

(*
Rplus (Rplus R1
             (Rmult (Rplus R1 R1)
                    (Rplus R1 R1)))
      (Rinv (Rplus R1 R1)).
i.e. (1 + (1 + 1) * (1 + 1)) + (1 + 1)⁻¹ 
*)

Среди последствий этого аксиоматического подхода есть тот факт, что следующая цель не может быть доказана reflexivity больше (как это можно сделать для natв аналогичной ситуации):

Set Printing Notations.
Goal a = 9 + 1 + /10.
  Fail reflexivity.

Это терпит неудачу, потому что AST (термины) с обеих сторон равенства различны, и Coq не преобразовывает их в некоторые канонические значения, чтобы сравнить их в конце. На этот раз нам нужно показать, что два AST взаимно конвертируемы.

  enough (9 + 1 = 10).
  - now rewrite H.

Теперь нам нужно доказать 9 + 1 = 10:

  - rewrite Rplus_comm, <-Rplus_assoc.
    rewrite <-(Rmult_1_r 2) at 1.
    rewrite <-Rmult_plus_distr_l.
    reflexivity.

К счастью для нас, существует тактика, которая может сделать эту утомительную работу за нас:

    Restart.
    unfold a; field.
Qed.

Однако подход стандартной библиотеки не единственный возможный. Этот ответ @gallais может помочь вам изучить другие варианты.