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

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

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 (как это могло бы быть сделано для nats в аналогичной ситуации):

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 может помочь вам изучить другие варианты.