coq

0热度

1回答

我有一个归纳关系，如下所示标题为后缀。我试图证明有关定理 suffix_app。我的一般想法是使用后缀xs ys这一事实来表明xs等于ys或者它是某些系列元素缺点'd到ys。 Require Import Coq.Lists.List. Import ListNotations. Inductive suffix {X : Type} : list X -> list X -> Prop :

1热度

1回答

构建Coq代码

我有一个通常的设置：首先定义一些类型，然后定义这些类型的一些函数。然而，由于有很多方法来形式化我所做的事情，我会在3个版本中做到这一点。为了简单（并保持概述），我希望我的代码在一个文件中。我也想尽量减少重复代码。的功能f: A -> B一般Definition，可访问： - 要为此，设置W/3 Module S代表具体的东西，在他们面前的一般定义可能会奏效，但不是在形势的类型如下所述在所有部

3热度

1回答

在勒柯克运算符重载符号

我想对几种判断创建符号，例如用于打字和子类型关系： Reserved Notation "Г '⊢' t '∈' T" (at level 40). Reserved Notation "Г '⊢' T '<:' U" (at level 40). Inductive typing_relation : context -> term -> type -> Prop := ... wher

1热度

1回答

Coq：定义前缀记法

我试过w /不同的符号，但不能让我的前缀表示法工作（中缀，另一方面，作品）。我想这是一个级别的问题，但无法整理出来。有任何想法吗？ Variable (X R: Type)(x:X)(r:R). Variable In: X -> R -> Prop. Variable rt:> R -> Type. Variable rTr: forall (x:X)(y:R), In x y -> y.

1热度

1回答

如果在CoC上不可能有O（1）pred，那么为什么这会起作用？

我一直认为已经证明pred不能在任何数据类型编码的微积分结构中以恒定时间表示。现在，考虑到这一点编码NATS： S0 : ∀ (r : *) . (r -> r) -> r -> r S0 = λ s z . z S1 : ∀ (r : *) (((∀ (r : *) . (r -> r) -> r -> r) -> a) -> (a -> a))) S1 = λ s z . (s (λ

3热度

1回答

如何正式确定Coq中的期限缩减关系的终止？

我有一个术语重写系统（A→→），其中A是一个集合→→是一个中缀二元关系。给定x的x和y，x→y表示x简化为y。要实现一些属性，我只需使用Coq.Relations.Relation_Definitions和Coq.Relations.Relation_Operators中的定义。现在我想正式以下属性： →被终止，那就是：没有无限递减链A0→A1→... 我怎样才能做到这一点在Coq？

1热度

1回答

减法的Coq证明不通勤

我想证明减法不能通过Coq，但是我被卡住了。我相信我想在Coq中证明的陈述将被写入forall a b : nat, a <> b -> a - b <> b - a 以下是我迄今为止证明的内容。 Theorem subtraction_does_not_commute : forall a b : nat, a <> b -> a - b <> b - a. Proof.

1热度

1回答

Coq的不产生归纳假设

我得到的溶液与以下定理，如下所示： Require Import Coq.Lists.List. Import ListNotations. Inductive suffix {X : Type} : list X -> list X -> Prop := | suffix_end : forall xs, suffix xs xs | suffix_ste

1热度

1回答

如何证明半汇合意味着Coq汇合？

我用Coq.Relations提供的定义，我有以下定义： Definition joinable (x:A) (y:A) : Prop := exists z, (clos_refl_trans A R x z) /\ (clos_refl_trans A R y z). Notation "X ↓ Y" := (joinable X Y) (at level 70, right a

1热度

1回答

勒柯克 - 证明涉及bigops在Ssreflect

我试图证明使用数学组件库遵循严格的不等式： Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R): (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) -> \sum_(i < q) F i < \sum_(i < q) G i. 起初，我试图找到一些引理相当于b