代码之家 › 专栏 › 技术社区 › Greg Nisbet

Coq为内射函数定义一个类型构造函数

coq

Greg Nisbet · 技术社区 · 6 年前

类型的内射函数 A 到 B

例如

f : â -> â
f = Î»x. 2*x

我在想怎么用Coq来表达这样的东西。

A -> B

我试着把一些东西放在这里的ellpies里,但是不能捕获函数。

Definition injection (A : Prop) (B: Prop) :=
  A -> B /\ ...

我不知道该把什么放在椭圆里。

Definition injection (A : Prop) (B: Prop) :=
  A * (not (A = A)) -> B * (not (B = B)).

= 正在操作类型本身。。。而且,即使这个定义可以被修改成更好的定义,它也需要大量令人讨厌的管道。

1 回复 | 直到 6 年前

Anton Trunov 6 年前

一种方法是定义一个名为 injective 把它作为引理的一个条件,要求它们的函数是内射的:

Definition injective {A B} (f : A -> B) := forall x1 x2, f x1 = f x2 -> x1 = x2.

Lemma inj_comp {A B C} (f : B -> C) (g : A -> B) :
  injective f -> injective g -> injective (fun x => f (g x)).

这是Mathcomp/SSReflect中采用的方法(参见 definition 以及一个用法,例如。 here ).

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

6 年前