标签: coq

我试图less_than在Coq中证明一些定理.我正在使用这个归纳定义:

Inductive less_than : nat->nat->Prop :=
   | lt1 : forall a, less_than O (S a)
   | lt2 : forall a b, less_than a b -> less_than a (S b)
   | lt3 : forall a b, less_than a b -> less_than (S a) (S b).

我总是需要显示lt3的倒数,

Lemma inv_lt3, forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
   ???

我被困住了,如果有人对如何继续进行提示,我将非常感激.

(我的归纳定义是否有问题less_than？)

谢谢!

我有这种类型

Inductive coef :=
| Mycoef_ex2 : matrix -> coef
with matrix :=
| My_matrix : list (list coef) -> matrix.

Inductive my_type :=
| Mytype_ex1 : list my_type  -> my_type
| Mytype_int : Z -> my_type
| Mytype_coef : coef -> my_type.

在Ocaml我可以这样写:

let test_mytype := function
| Mytype_ex1 [Mytype_coef (Mycoef_ex2 (My_matrix m)); Mytype_int i] :: ps -> ...

我想使用参数m并i在同一函数中,我的函数需要两个参数.但是Coq我不能这样做,例如,如果我写入Coq

Definition test_mytype (m: my_type) :=
 match m with
  | Mytype_ex1 …

我可能遗漏了一些基本的东西.

我可以证明以下"身份":

Theorem identity_simple : forall a : Prop, a -> a.

随着intro. intro. assumption..

但是,我似乎无法证明:

Theorem identity : forall a : Prop, a.

我当然能做到intro,但这让我:

a : Prop
_________(1/1)
a

我不知道该怎么做.
第一种形式似乎是多余的,表明对所有人而言a,a意味着a.

我正在Coq做练习并试图证明一个列表是否等于它的反向,它是一个回文.以下是我定义回文的方法:

Inductive pal {X : Type} : list X -> Prop :=
  | emptypal : pal []
  | singlpal : forall x, pal [x]
  | inducpal : forall x l, pal l -> pal (x :: l ++ [x]).

这是定理:

Theorem palindrome3 : forall {X : Type} (l : list X),
  l = rev l -> pal l.

根据我的定义,我需要做感应我提取前面和尾部元素,但显然coq不会让我这样做,如果我强迫它这样做,它给出一个绝对不会做的归纳结果任何意义:

Proof.
  intros X l H. remember (rev l) as rl. induction l, rl.
  - apply emptypal.
  - inversion H.
  - inversion …

我刚开始使用Coq.

我如何定义命题myProp,使得给定一个集合H,myProp Hiff是真的 ？

特别是,我如何表达作为命题的H一个子集的事实nat？或者我怎样才能简单地说让H成为nat的一个子集？

在问题中Coq中有一套最小的完整策略吗？,提到的答案exact足以证明所有目标.有人可以解释一下吗？例如,A \/ B -> B \/ AA,B作为Prop 的目标如何仅通过一堆来证明exact？如果您有其他更好的例子,请不要犹豫,也请回答.关键是要对这个问题给出一些解释并给出一个非常重要的例子.

在Coq教程 1.3.1和1.3.2节中，有两个elim应用程序：第一个应用程序：

1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   B /\ A

申请后elim H，

Coq < elim H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   A -> B -> B /\ A

第二个：

1 subgoal

  H : A \/ B
  ============================
   B \/ A

申请后elim H，

Coq < elim H.
2 subgoals

  H …

我需要证明该方程组没有解决方案（原因是它被过度确定）。在Coq中有一种简单的方法吗？是战术还是图书馆？

Require Import Reals.
Open Scope R.

Lemma no_solution:
  forall 
    b11 b12 b13 b14 b21 b22 b23 b24 b31 b32 b33 b34
    r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 : R,
   1 = r * b11 + r0 * b21 + r1 * b31    ->
   0 = r * b12 + r0 * b22 + r1 * b32    ->
   0 = r * b13 + r0 * b23 + r1 * b33    -> …

我正在阅读Adam Chlipala关于Coq的书,它定义了归纳类型:

Inductive unit : Set :=
  | tt.

我试图了解它的归纳原理:

Check unit_ind.
(* unit_ind
     : forall P : unit -> Prop, P tt -> forall u : unit, P u *)

我不确定我是否理解Coq的输出意味着什么.

1)所以检查让我看看"对象"的类型吧？所以unit_ind有类型:

forall P : unit -> Prop, P tt -> forall u : unit, P u

对？

2)如何读取该类型？我无法理解括号或其他内容的位置......对于逗号之前的第一件事,我将其读作没有意义:

IF "for all P of type unit" THEN " Prop "

因为这个假设不是真的或假的.所以我假设真正的第一件事就是这样:

forall P : (unit -> Prop), ...

因此P只是类型单位到prop的函数.它是否正确？

我希望这是正确的,但根据这种解释,我不知道如何在第一个逗号后阅读该部分:

P tt -> forall u : unit, …

我不知道在哪种情况下应该使用Theorem过度Lemma或相反的用法。两者之间有什么区别（尽管在语法上）

Theorem l : 2 = 2.
  trivial.
Qed.

和这个

Lemma l : 2 = 2.
  trivial.
Qed.

？