ssreflect是否假設被排除的中間？

Question

我讀了ssreflect教程，which reads：

下面，我們證明了...通過翻譯命題陳述 到其布爾對應，這是很容易使用暴力 力證明。這種證明技術被稱爲反射。 Ssreflect的設計 允許和ssreflect的精神建議廣泛使用這種技術 。

這（反射）是否意味着ssreflect假定被排除的中間（forall A:Prop, A \/ ~A）？

它看起來就是這樣，因爲所有的布爾值都滿足E.M.如果是這樣，這將是一個很大的假設，以遵循ssreflect風格。

另外，我不太明白，遵循的是「本地」或「小規模」的一部分：

由於它通常用於本地處理的 的證明有效的小零件（而不是被用於整體校樣結構），這稱爲小尺度反射，因此稱爲ssreflect。

這是什麼意思小零件v.s.整體的證明結構。這是否意味着我們可以在本地假設E.M.有時沒有傷害，一般不使用E.M.，或者當地在這裏是否有其他意義？

另外，我沒有足夠的Coq經驗，也不太清楚「布爾對應」（主要基於迄今爲止我所讀到的case分析）上的這種「強力」風格比香草Coq的方式。對我來說，蠻力不是很直觀，不容易事先猜測，直到看到結果。

任何具體的例子來說明這裏的效率？

Answer 1

Ssreflect不承擔排中，但是庫的大的部分是建立在布爾命題，那就是，bool的類型，它的確認爲

forall b : bool, b = true \/ b = false 

以上的等效版本通常被寫成，使用隱式is_true鑄造，如：

forall b : bool, b \/ ~ b. 

「可反射」謂詞是那些在bool有一個版本;自然數之間的「小於或等於」關係就是一個很好的例子。

在標準Coq中，le被編碼爲一個歸納類型，而在ssreflect中它是一個計算函數leq: nat -> nat -> bool。

使用leq函數進行證明更「有效」，原因如下：假設您想證明102 < 203。使用標準的Coq定義，你將不得不建立一個大的證明術語，你必須明確地編碼證明的每一步。

但是，在其計算對象中，證明僅僅是術語erefl，見證該算法返回true。除了IMO的許多其他優勢之外，這對於大規模證明至關重要。

最後，我不同意「ssreflect只涉及可判定類型」的說法。雖然很大一部分庫是基於可判斷（布爾）謂詞的，但還有很多其他的地方沒有做出這種假設，或者在存在一些公理時非常有用。

Answer 2

Ssreflect不承擔一般排中，你將不能夠證明

forall A: Prop, A \/ ~A 

然而，ssreflect只關心可判定類型：哪些類型的平等可以決定的，通常表示爲

Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}. 

in Coq。這意味着對於T類型的任何兩個元素，都可以得到一個建設性的結果（在Set中，而不是在Prop中，如排除的中間），證明它們相同或不同。因此，大多數推理可以在bool而不是Prop中完成，所以你有某種排除中間的限制形式，只適用於布爾語句。