勒柯克實數-lexing和解析3.14

Question

隨着雷亞爾庫中導入

Require Import Reals. 

我如何定義常量，如3.14或10.1，並將其用於函數定義或計算？

Answer 1

您可以定義常量，如下所示：

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

但是請注意，該標準庫定義雷亞爾公理。 您可以找到主要定義here。請注意定義爲Parameter s，這是Axiom的同義詞。 例如，R0和R1代表實數0和1,Rplus和Rmult表示加法和乘法，但是這些定義不是歸納數據類型和函數，因爲它們缺少定義。爲了能夠處理實數，我們需要公理，控制它們之間的相互作用（給出here）。

您可以將標準庫中的實數看作​​，標記爲R0,R1,Rplus等節點。你會得到一些規則（公理），它們指定你可以在這些AST上執行的（唯一的）轉換。

讓我們來看看勒柯克如何代表實數：

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 S IN進行類似的情況）：

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

失敗的原因是在平等的兩側的AST（條款）是不同的，勒柯克不會將它們轉換爲某種規範值，他們在最後進行比較。這次我們需要證明兩個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. 

標準庫的方法是但不是唯一可能的。 This answer by @gallais可以幫助您探索您的其他選項。