coq

1热度

1回答

我无法证明使用coq的策略的简单逻辑max a b <= a+b。我应该如何解决它？以下是我到现在为止的代码。 s_le_n已被证明，但为简单起见，此处未提及。 Theorem s_le_n: forall (a b: nat), a <= b -> S a <= S b. Proof. Admitted. Theorem max_sum: forall (a b: nat), max a

-1热度

2回答

勒柯克：如何证明如果语句涉及字符串？

我有一个string b和string a上比较，如果有平等的string c，否则有string x。我知道的假设fun x <= fun c。我如何证明以下陈述？ fun是一些函数，它发生在string并返回nat。 fun (if a == b then c else x) <= S (fun c) 的逻辑似乎是显而易见的，但我无法将拆分COQ的if语句。任何帮助，将不胜感激。谢谢！

1热度

1回答

在绑定器下泛化表达式

我需要在绑定器下泛化表达式。例如，我有我的目标，两个表达式： (fun a b => g a b c) 和 (fun a b => f (g a b c)) 我想概括g _ _ c部分：一种方法做的是第一重写它们分为： (fun a b => (fun x y => g x y c) a b) 第二入： (fun a b => f ( (fun x y => g

0热度

1回答

减少配以鉴于假设</p> <pre><code>H0 : n <> 0 </code></pre> <p>在COQ

自然数条件如何减少术语 ... if match n with | 0 => false | S m' => n =? m' end then ... 在目标？

2热度

1回答

从可计算函数移动到归纳关系

我想了解如何从运算可计算函数的定理转移到使用归纳定义关系来表示计算的定理。考虑下面这个简单的开发。让我们先从关系及其属性的标准定义： Definition relation (X : Type) := X -> X -> Prop. Definition reflexive {X : Type} (R : relation X) := forall a, R a a. Defin

0热度

1回答

有没有一种很好的方法来阻止自动发生在目标中的beta减少？

假设您想证明(fun (x : unit) => false) <> (fun (x : unit) => true)。证明这一点的明显方法是将intro一些H : (fun _ : unit => false) = (fun _ : unit => true)和使用H进行重写以证明false = (fun x => false) tt = (fun x => true) tt = true)。但

0热度

1回答

错误：非法应用（非功能性构造）

我正在尝试使用HoTT书籍中的类型构造函数/消除器来阐述各种deMorgans法则的一些证明。我已经跳过了相关的东西挑选https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf并将其全部转储到.v文本文件中。我需要消除/介绍产品，联产品和建立否定的方法规则。到目前为止，我有， Definition idmap {A:Type} (x:A) : A

0热度

2回答

错误：在当前环境中找不到参考fst

我正在编写一个小程序，以便我可以使用HoTT书（等）中的类型导入/消除规则来对deMorgans定律进行一些证明。我的模型/示例代码都在这里，https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf。到目前为止，我有， Definition idmap {A:Type} (x:A) : A := x. Inductive prod (A B:T

2热度

2回答

有关函数值的嵌套归纳的定点证明

我试图在Coq中证明归纳原理。由于数据结构的定义，必须通过两个嵌套式导入来显示该原理。外部感应通过Fixpoint构造完成，内部感应通过原理list_ind完成。发生的问题是现在内部归纳的归纳论证是一个函数的结果，即dfs t。 Inductive SearchTree (A : Type) : Type := | empty : SearchTree A | leaf :

0热度

1回答

FORALL平等勒柯克

我试图证明以下等式： Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A) (ic0 : 0 < S n) (ic1 : 0 mod S n < S n): gen (n - n) ic1 = gen 0 ic0. 的n-n值为0 Nat.sub_diag和0 mod S n也为0的Nat.mod_0