在我的证明中,我偶然发现了A /\ B /\ C我的假设存在的问题,我需要证明(A /\ B) /\ C.这些在逻辑上完全相同,但是coq不能解决这些问题assumption..
我一直在通过应用公理来解决这些问题,但是有更优雅(和正确)的方法来处理这个问题吗？
从Coq中提取的Ocaml代码包括(在某些情况下)定义的类型__和函数__,如下所示:
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
文档说,在过去,这种类型被定义为unit(因此__可以被视为()),但存在(罕见的)类型__的值应用于类型的值的情况__.
__使用Obj来自OCaml 的模块的未记录的函数,但似乎所定义的本质上是一个完全多态的函数,它吃掉它的所有参数(无论它们的数量是多少).
是否存在一些关于__无法消除的情况的文档,并且这种类型的值应用于相同类型的值,既来自理论(构造Coq术语,其中消除是不可能的),也来自实际的(表明发生这种情况的现实情况) ) 观点看法？
假设我有一组函数,每个函数都可以依赖于一个或两个隐式变量A B: Type.我怎么指定这个？即将这些变量添加到它们的变量列表中并将它们设置为隐式变量.
最明显的方法是添加{A B: Type}到他们的定义中.然而,在现实生活和中等复杂的发展中,这些共享的隐含列表很容易就是6-10个条目,并且包括复杂的类型,因此使得函数定义难以阅读,甚至更难理解它们的相似性或对所提到的类型进行更改.因此,该解决方案不适用.
我可以在一个部分或模块中包含所有函数并Variables (A B: Type) etc在开头写入,但这不会使变量隐含,我将不得不在部分末尾手动设置所有函数的参数.更糟糕的是,这将使所有变量共享.即如果我宣布
Section sect.
Variable A B: Type.
Definition f (t: A -> Type) := (..).
Definition g (t: A -> Type) (s: B -> Type) := G (f t) (f s).
End sect.
(G是一些双变量函数)然后g不会被接受,因为s不存在A -> Type,即使基本上f只需要一个任意类型的族.
我可以制作一个部分并宣布Context {A B: Type}.这将使这些变量隐含在所有函数中,但是像以前一样的共享问题仍将存在.因此,我必须随意将我的函数分成几个部分,以便我可以使用隐式参数的不同值来调用Sect.1中的函数.这很有效,但很难看,而且我可以很容易地想象出每个部分都必须有2-3个函数才能正常调用它们的情况.
有更好的解决方案吗？
我知道可以将Coq程序提取到Haskell和OCaml程序中.有没有办法用C做到这一点？
我想象的是一个模拟C语言的库.也许这样的库将包含关于C构造如何与过程存储器相互作用的公理集合,以及关于IEEE浮点数的公理和定理.然后,它将能够在Coq中构建一个C程序以及有关该程序的定理.
比方说,我会使用这样一个库来构建一个C快速排序算法,该算法适用于可由GCC编译的浮点数组.
我有重写引理的基础。其中一些由类型类参数化。当应用引理时，重要的是当 Coq 无法自动解析类型类时重写会失败。我发现获得这种行为的唯一方法是隐式声明大多数参数。
Class T (t:Type) : Type.
Instance T1 : T nat.
Instance T2 : forall {A1 A2:Type} {t1:T A1} {t2:T A2}, T (A1*A2).
Definition f {A:Type} (x:A) := x.
Lemma f_eq : forall {A:Type} (t:T A) (x:A), f x = x.
Proof.
reflexivity.
Qed.
Lemma test1 : f (0,1) = (0,1).
Proof.
rewrite f_eq.
(* a subgoal T (nat * nat) is generated,
which should have been resolved directly *)
Abort.
Lemma test2 : f (0,true) = (0,true). …我注意到 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 …我有以下 Coq 环境。
1 subgoals
m : nat
IHm : forall n : nat, n + n = m + m -> n = m
n : nat
H : S (n + S n) = S (m + S m)
ll := ll : forall k : nat, k + S k = S k + k
这样做，只改变rewrite ll in HLHS ，而不改变RHS 。 应该适用于 nat 类型的所有变量。这里有什么问题吗？S (n + S n)S (S n + n)S …
我有一个类型，比如说
Inductive Tt := a | b | c.
定义它的子类型的最简单和/或最好的方法是什么？假设我希望子类型仅包含构造函数a和b. 一种方法是对二元素类型进行参数化，例如 bool：
Definition filt (x:bool): Tt := match x with
| true => a
| false => b end.
Check filt true: Tt.
这是可行的，但如果您的表达式具有以这种方式定义的多个（可能相互依赖的）子类型，则非常尴尬。此外，它只能工作一半，因为没有定义子类型。为此我必须另外定义例如
Notation _Tt := ltac: (let T := type of (forall {x:bool}, filt x) in exact T).
Fail Check a: _Tt. (*The term "filt x" has type "Tt" which should be Set, Prop or Type.*)
在这种情况下也不起作用。另一种方法是使用类型类，例如
Class s_Tt: Type := s: Tt.
Instance …当我查看 QuickChick 项目时，遇到了这句话“Require Import Ltac.我不知道这是做什么的以及Ltac模块在哪里”。我找到了一个文件plugins/ltac/Ltac.v，但这不可能是这个文件，因为该文件是空的（顺便说一句，包含空文件的目的是什么？）。我尝试过Locate Ltac.，但得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更令人困惑。
该模块的作用是什么Ltac，文件在哪里Ltac.v，为什么该Loacte命令在这种情况下不起作用？谢谢！
我有一个关于 Coq 中类型检查定义的问题。我遇到了这样一种情况，我有两个类型为 t1 和 t2 的项，从定义中我知道 t1 和 t2 相等 (t1 = t2)。但是，我不能一起使用这两个术语，因为类型检查器认为这些类型不相等。我试图隔离一个最小的示例来模拟情况（是的，我知道这是一个愚蠢的属性，但我只是希望它得到类型检查；））：
Require Import Coq.Lists.List.
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
t1 = t2 ->
l1 = l2.
假设我不能(l2 : list t1)直接写，因为我从另一个定义中得到它。
我尝试使用，Program因为我希望我可以以某种方式推迟任务来证明类型匹配，但这没有帮助（得到相同的类型检查错误）。
如果上面的例子不足以让问题清楚，这里是我的实际问题的摘录：
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') …