作为一个粗略和未经训练的背景,在HoTT中,可以推断出归纳定义的类型
Inductive paths {X : Type } : X -> X -> Type :=
| idpath : forall x: X, paths x x.
这允许非常一般的建筑
Lemma transport {X : Type } (P : X -> Type ){ x y : X} (? : paths x y):
P x -> P y.
Proof.
induction ?.
exact (fun a => a).
Defined.
这Lemma transport 将是HoTT"替换"或"改写"战术的核心; 据我所知,诀窍就是假设你或我可以抽象地认出的目标
...
H : paths x y
[ Q : (G x) ]
_____________ …我们怎样才能像那些符号的定义/类型"+",或"++"的List？
我曾尝试:Search ++,Search "++",Search (++),
SearchAbout ...和
Check ++,Check "++",Check(++).
然而,他们都没有工作......
SearchAbout "++"确实显示了一些信息,但没有显示"++".
我正在使用Coq Proof Assistant来实现(小)编程语言的模型(扩展由Bruno De Fraine,Erik Ernst,MarioSüdholt执行的Featherweight Java).使用induction策略时不断出现的一件事是如何保存包含在类型构造函数中的信息.
我有一个子类型Prop实现为
Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
extends C D ->
sub_type (c_typ C) (c_typ D).
Hint Constructors sub_type.
extends在Java中看到的类扩展机制在哪里,它typ表示可用的两种不同类型,
Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ …我已经阅读了Fortify静态检查工具的一些文档.此工具使用的概念之一称为taints.某些来源(例如Web请求)提供以一种或多种方式受到污染的数据,而某些接收器(例如Web响应)要求数据不受污染.
Fortify的好处在于你可以拥有几种类型的污点.例如,您可以标记srand输出,NON_CRYPTO_RAND然后要求在使用变量进行加密时不存在此污点.其他示例包括非绑定的检查号码等.
是否有可能使用Haskell或其他编程语言中使用的更强大的静态类型系统来模拟污点,甚至更复杂的类型系统？
在Haskell中,我可以做类型,Tainted [BadRandom,Unbounded] Int但是使用它们进行计算似乎很困难,因为这种新类型限制了不限制污点的操作.
有没有更好的方法来实现这一目标？有关该主题的任何现有工作？
我在Coq中从模块导入定义时遇到问题.我是Coq的新手,但无法使用该语言的参考手册或在线教程解决问题.我有一个模块定义了有限集的签名和公理,我打算在另一个模块中实现.还有更多,但它看起来像这样(作为参考,我正在密切关注Filliatre关于有限自动机的论文):
Module FinSet.
...
Parameter fset : Set -> Set.
Parameter member : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union :
forall A : Set, forall a b : fset A, forall x : …将Coq源转换为Idris有哪些有用的指导原则(例如,它们的类型系统有多相似,以及可以对翻译进行翻译)？从我收集的内容来看,伊德里斯的内置战术库很小但可扩展,所以我认为有一些额外的工作应该是可行的.
我试着 通过形式化教自己Coq 形式化 我熟悉的数学定理:停止问题的不可判定性 可计算性理论中的各种定理.
由于我对形式化计算模型的细节不感兴趣(例如,图灵机,注册机,lambda calculi等),我试图通过 "教授Coq Church-Turing论文",即假设Axioms表示Coq认为可计算的函数的属性(即,可定义的类型函数nat -> nat).
例如,如果我想告诉Coq有部分可计算函数的有效枚举,我可以说
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
这里,部分可计算函数被认为是(总)可计算函数,给定第一个参数s,模拟s许多步骤的原始部分可计算函数的计算.我还可以添加其他Axioms,如Padding Lemma,我可能能够证明停止问题的不可判定性,以及可计算性理论中的其他一些定理.
我的第一个问题是我到目前为止是否走在正确的轨道上.难道不是我正在尝试做的事情显然不可能出现不完整现象或Coq类型系统的性质吗？
我的第二个问题是关于相对化.如果我试图在可计算性理论中证明更严肃的事情,我会考虑在oracles中进行计算.由于oracles经常被构造为部分二值函数的极限,所以似乎(至少天真地)使oracles具有类型是自然的nat -> bool.同时,为了使神谕变得不平凡,它们必须是不可计算的.考虑到这一点,具有类型的oracle是否nat -> bool有意义？
这是关于oracles的另一个问题:如果对于每个oracle,存在相对于该特定oracle的部分可计算函数的类型,那将是非常好的.我可以通过在Coq中利用依赖类型系统来做到这一点吗？这种可能性是否取决于上文所述的一些形式化神谕的选择？
编辑:上面的方法肯定不能正常工作,因为我需要一个额外的公理:
Axiom Phi_inverse: partial -> nat.
这应该不会成为预言真的.有没有像我上面描述的方法(我的意思是,那个不涉及计算模型形式化的方法)？
编辑:为了澄清我的意图,我编辑了上面的问题陈述.另外,为了呈现我想到的形式化的风格,我提出了一个不完整的证据,证明这里停止问题的不可解决性:
Require Import Arith.
Require Import Classical.
Definition ext_eq (A B : Set) (f g : A -> …我正在通过软件基础工作,目前正在进行关于教会数字的练习.这是自然数的类型签名:
Definition nat := forall X : Type, (X -> X) -> X -> X.
我已经定义了一个succ类型的函数nat -> nat.我现在想定义一个这样的加法函数:
Definition plus (n m : nat) : nat := n nat succ m.
但是,我收到以下错误消息:
Error: Universe inconsistency.
这个错误信息实际意味着什么？
我正在阅读关于Coq的教程.它构造一个bool类型如下:
Coq < Inductive bool : Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined
然后它显示了这些东西正在使用"检查".
Coq < Check bool_ind.
bool_ind
: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
Coq < Check bool_rec.
bool_rec
: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
Coq < Check bool_rect.
bool_rect
: …是否可以切换当前目标或子目标以在Coq中证明？
例如,我有一个这样的目标(来自eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
我想要做的是首先split证明合适的合并.我认为这将给出存在变量的值?s,而左合并应该只是一个简化.
但split默认情况下,将左合并设置?s > 0为当前目标.
______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
我知道我可以在战术2:上加上第二个子目标的操作,但这很尴尬因为
1)我看不到目标#2和.的假设
2)如果它处于不同的上下文中,目标#2可能是第三个或第k个目标.证明不可移植.
这就是为什么我想把第二个目标设定为当前目标.
顺便说一下,我正在使用CoqIDE(8.5).