我仍然对COQ中排序Set的含义感到困惑.我何时使用Set,何时使用Type？
在Hott中,Set被定义为一种类型,其中身份证明是唯一的.但我认为在Coq中它有不同的解释.
有人可以告诉我之间的区别
Require 名字.Require Import 名字.Import 名称？
我很好奇discriminate战术背后的策略是如何运作的.因此我做了一些实验.
首先是一个简单的归纳定义:
Inductive AB:=A|B.
然后是一个简单的引理,可以通过discriminate策略证明:
Lemma l1: A=B -> False.
intro.
discriminate.
Defined.
让我们看看证明的样子:
Print l1.
l1 =
fun H : A = B =>
(fun H0 : False => False_ind False H0)
(eq_ind A
(fun e : AB => match e with
| A => True
| B => False
end) I B H)
: A = B -> False
这看起来相当复杂,我不明白这里发生了什么.因此,我试图更明确地证明相同的引理:
Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined. …我在Coq中寻找一个不同的相等证明的例子.
这意味着:
给出一些类型T和两个元素x,y:T和两个样张p1,p2:x = y,其中p1 <> p2.
我想知道该simpl策略如何在 COQ 中发挥作用。
假设以下引理：
Parameter n:nat.
Lemma test: S n + 0 = S (n+0).
现在，simpl.战术产生
S (n + 0) = S (n + 0)
我的理解是simpl执行一系列
cbv beta, delta, iota转换。我试过了，但无法获得与simpl. 基本问题是，在cbv delta展开之后，该plus术语一直在展开。我怎样才能去扩展它，即重新替换plus扩展定义的名称？
或者，谁能告诉我如何simpl通过手动执行更基本的策略来获得效果？
将Axioms添加到COQ通常会使证明更容易,但也会引入一些副作用.例如,通过使用经典公理,人们离开了直觉主义领域,并且证明不再是可计算的.我的问题是,使用功能扩展性公理的缺点是什么？
我注意到 Coq 综合了关于 Prop 和 Type 等式的不同归纳原理。有人对此有解释吗？
平等定义为
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
与之相关的归纳原理有以下类型：
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
现在让我们定义一个 eq 的 Type 挂件：
Inductive eqT {A:Type}(x:A):A->Type:= eqT_refl: eqT x x.
自动生成归纳原理为
eqT_ind
: forall (A : Type) (x : A) (P : forall a …在HOTT和COQ中,人们无法证明UIP,即
\ Prod_ {p:a = a} p = refl a
但是可以证明:
\ Prod_ {p:a = a}(a,p)=(a,refl a)
为什么定义它是这样的？是吗,因为人们希望有一个很好的同伦解释？或者这个定义有一些自然的,更深层次的原因吗？
我仍然想知道eqCOQ 中相等类型的术语可以与eq_refl.
下面的术语是一个例子吗？
((fun x:nat => eq_refl x) 2).
该术语在语法上与 不同eq_refl，但它计算为eq_refl。
是否存在不计算为的术语示例eq_refl？
PS 这不是作业问题;-)
我正在试验 Coq Coinductive 类型。我使用 Coq'Art 书（第 13.1.4 节）中的惰性列表类型：
Set Implicit Arguments.
CoInductive LList (A:Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.
Implicit Arguments LNil [A].
CoFixpoint LAppend (A:Set) (u v:LList A) : LList A :=
match u with
| LNil => v
| LCons a u' => LCons a (LAppend u' v)
end.
为了匹配保护条件，我还使用了本书中的以下分解函数：
Definition LList_decomp (A:Set) (l:LList A) : LList A :=
match l with
| LNil => …