天道酬勤,学无止境

Coq 归纳从特定的 nat 开始(Coq induction start at specific nat)

问题

我正在尝试学习 coq,所以请假设我对此一无所知。

如果我在 coq 中有一个引理

forall n m:nat, n>=1 -> m>=1 ...

我想通过对 n 进行归纳。 我如何从 1 开始归纳? 目前当我使用“归纳n”时。 策略它从零开始,这使得基本语句为假,从而难以继续。

任何提示?

回答1

以下是证明每个命题P对所有n>=1为真,如果P1为真并且P归纳为真。

Require Import Omega.

Parameter P : nat -> Prop.
Parameter p1 : P 1.
Parameter pS : forall n, P n -> P (S n).

Goal forall n, n>=1 -> P n.

我们通过归纳法开始证明。

  induction n; intro.

如果您有一个错误的假设,那么错误的基本案例是没有问题的。 在这种情况下0>=1

  - exfalso. omega.

归纳的情况很棘手,因为要获得P n的证明,我们首先必须证明n>=1 。 诀窍是对n进行案例分析。 如果n=0 ,那么我们可以简单地证明目标P 1 。 如果n>=1 ,我们可以访问P n ,然后证明其余的。

  - destruct n.
    + apply p1.
    + assert (S n >= 1) by omega.
      intuition.
      apply pS.
      trivial.
Qed.
标签

受限制的 HTML

  • 允许的HTML标签:<a href hreflang> <em> <strong> <cite> <blockquote cite> <code> <ul type> <ol start type> <li> <dl> <dt> <dd> <h2 id> <h3 id> <h4 id> <h5 id> <h6 id>
  • 自动断行和分段。
  • 网页和电子邮件地址自动转换为链接。

相关推荐
  • Coq - 在不丢失信息的情况下对函数进行归纳(Coq - Induction over functions without losing information)
    问题 在尝试对函数的结果(返回归纳类型)执行案例分析时,我在 Coq 中遇到了一些麻烦。 当使用通常的战术,像elim , induction , destroy等,信息丢失。 我举个例子: 我们首先有一个像这样的函数: Definition f(n:nat): bool := (* definition *) 现在,假设我们正处于证明特定定理的这一步: n: nat H: f n = other_stuff ------ P (f n ) 当我应用一种策略时,比如说, induction (fn) ,会发生这种情况: Subgoal 1 n:nat H: true = other_stuff ------ P true Subgoal 2 n:nat H: false = other_stuff ------ P false 但是,我想要的是这样的: Subgoal 1 n:nat H: true = other_stuff H1: f n = true ------ P true Subgoal 2 n:nat H: false = other_stuff H1: f n = false ------ P false 在它实际工作的方式中,我丢失了信息,特别是我丢失了有关fn任何信息。 在我处理的问题中,我需要使用fn = true或fn = false ,用于其他假设等
  • 使用定义明确的归纳定义的递归函数进行计算(Compute with a recursive function defined by well-defined induction)
    问题 当我在 Coq 中使用Function定义一个非结构化递归函数时,当要求进行特定计算时,结果对象的行为很奇怪。 实际上, Eval compute in ...指令不是直接给出结果,而是返回一个相当长(通常为 170 000 行)的表达式。 Coq 似乎无法计算所有内容,因此返回一个简化(但很长)的表达式而不仅仅是一个值。 问题似乎来自我证明Function产生的义务的方式。 首先,我认为问题来自我使用的不透明术语,我将所有引理转换为透明常量。 顺便说一句,有没有办法列出出现在术语中的不透明术语? 或者任何其他方式将不透明的引理变成透明的引理? 然后我评论说,问题更准确地来自所使用的顺序是有充分根据的证明。 但我得到了奇怪的结果。 例如,我通过重复应用div2在自然数上定义log2 。 这是定义: Function log2 n {wf lt n} := match n with | 0 => 0 | 1 => 0 | n => S (log2 (Nat.div2 n)) end. 我得到两个证明义务。 第一个检查n尊重递归调用中的关系lt并且可以很容易地证明。 forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1) intros. apply Nat.lt_div2
  • 我如何证明 Coq 中的两个 Fibonacci 实现是相等的?(How do I prove that two Fibonacci implementations are equal in Coq?)
    问题 我有两个 Fibonacci 实现,如下所示,我想证明它们在功能上是等效的。 我已经证明了自然数的性质,但是这个练习需要另一种我无法弄清楚的方法。 我正在使用的教科书介绍了 Coq 的以下语法,因此应该可以使用此表示法证明相等性: <definition> ::= <keyword> <identifier> : <statement> <proof> <keyword> ::= Proposition | Lemma | Theorem | Corollary <statement> ::= {<quantifier>,}* <expression> <quantifier> ::= forall {<identifier>}+ : <type> | forall {({<identifier>}+ : <type>)}+ <proof> ::= Proof. {<tactic>.}* <end-of-proof> <end-of-proof> ::= Qed. | Admitted. | Abort. 下面是两个实现: Fixpoint fib_v1 (n : nat) : nat := match n with | 0 => O | S n' => match n' with | O => 1 | S n'' => (fib_v1 n') + (fib_v1 n'')
  • 我可以将 Coq 证明提取为 Haskell 函数吗?(Can I extract a Coq proof as a Haskell function?)
    问题 自从我学了一点 Coq 就想学写一个 Coq 证明所谓的除法算法,它实际上是一个逻辑命题: forall nm : nat, exists q : nat, exists r : nat, n = q * m + r 我最近使用从 Software Foundations 中学到的知识完成了这项任务。 Coq 是一个用于开发构造性证明的系统,我的证明实际上是一种从值m和n构造合适的值q和r的方法。 Coq 有一个有趣的工具,可以将 Coq 算法语言 (Gallina) 中的算法“提取”为通用函数式编程语言,包括 Haskell。 另外我已成功地写divmod运营为加利纳Fixpoint和提取物。 我想仔细指出,该任务不是我在这里考虑的。 Adam Chlipala 在 Certified Programming with Dependent Types 中写道,“Curry-Howard 通信的许多粉丝支持从证明中提取程序的想法。实际上,很少有 Coq 和相关工具的用户会做这样的事情。” 甚至有可能将我的证明中隐含的算法提取到 Haskell 中吗? 如果可能,将如何实现? 回答1 感谢Dan Feltey 建议的Pierce 教授2012 年夏季视频4.1,我们看到关键是要提取的定理必须提供Type的成员,而不是通常的命题类型Prop 。 对于特定的定理,受影响的构造是归纳
  • 为什么不能对用于结论的术语进行归纳?(Why is it impossible to perform induction on a term that is used in conclusion?)
    问题 假设以下特定场景。 我们有一个平等的定义: Inductive eqwal {A : Type} (x : A) : A -> Prop := eqw_refl : eqwal x x. 和花生: Inductive nawt : Prop := | zewro : nawt | sawc : nawt -> nawt. 我们在 nats 上定义加法: Fixpoint plaws (m n : nawt) : nawt := match m with | zewro => n | sawc m' => sawc (plaws m' n) end. 现在我们想证明零是正确的。 总结: Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n. 可悲的是,以下校对的最后一行说“错误:结论中使用了 n。 ”。 Proof. intros. induction n. - this is the culprit 官方文档中没有太多关于错误的内容,我有些困惑——为什么会出现这个错误? 使用标准库,我可以轻松证明定理: Theorem neutral_r : forall n : nat, n + 0 = n. Proof. induction n; try reflexivity. cbn; rewrite IHn
  • 如何解决 Coq 中无效类型相等的目标?(How to solve goals with invalid type equalities in Coq?)
    问题 我的证明脚本给了我愚蠢的类型nat = bool比如nat = bool或nat = list unit ,我需要用它来解决矛盾的目标。 在普通数学中,这将是微不足道的。 给定集合bool := { true, false }和nat := { 0, 1, 2, ... }我知道true ∈ bool ,但true ∉ nat ,因此bool ≠ nat 。 在 Coq 中,我什至不知道如何true :̸ nat 。 问题 有没有办法证明这些等式是错误的? 或者,这是不可能的吗? (编辑:删除了一长串失败的尝试,仍然可以在历史记录中查看。) 回答1 tl;dr基数参数是显示类型不相等的唯一方法。 您当然可以通过一些反思更有效地自动化基数参数。 如果您想更进一步,请通过构建一个 Universe 来为您的类型提供句法表示,确保您的证明义务被构建为表示的句法不等式,而不是类型的语义不等式。 作为等式的同构 人们普遍认为(甚至可能在某处证明了这一点),Coq 的逻辑与同构集合在命题上相等的公理一致。 事实上,这是 Vladimir Voevodsky 的Univalence Axiom 的结果,人们现在玩得很开心。 我必须说,它是一致的(在没有 typecase 的情况下)似乎非常合理,并且可以构造一个计算解释,通过在任何给定时刻插入任何需要的同构组件
  • Coq induction start at specific nat
    I'm trying to learn coq so please assume I know nothing about it. If I have a lemma in coq that starts forall n m:nat, n>=1 -> m>=1 ... And I want to proceed by induction on n. How do I start the induction at 1? Currently when I use the "induction n." tactic it starts at zero and this makes the base statement false which makes it hard to proceed. Any hints?
  • 分解构造函数的相等性 coq(Decomposing equality of constructors coq)
    问题 通常在 Coq 中,我发现自己在做以下事情:我有证明目标,例如: some_constructor a c d = some_constructor b c d 我真的只需要证明a = b因为无论如何其他一切都是相同的,所以我这样做: assert (a = b). 然后证明子目标,然后 rewrite H. reflexivity. 完成证明。 但是让那些在我的证明底部徘徊似乎只是不必要的混乱。 Coq 中是否有一个通用的策略来获取构造函数的相等性并将其拆分为构造函数参数的相等性,有点像split但用于相等而不是连接。 回答1 特别是,标准 Coq 提供了f_equal策略。 Inductive u : Type := U : nat -> nat -> nat -> u. Lemma U1 x y z1 z2 : U x y z1 = U x y z2. f_equal 此外, ssreflect 提供了一个通用的一致性策略congr 。 回答2 您可以使用 Coq 的搜索功能: Search (?X _ = ?X _). Search (_ _ = _ _). 在一些噪音中它揭示了一个引理 f_equal: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y 以及它的多参数f_equal2兄弟:
  • 证明可逆列表是 Coq 中的回文(Proving that a reversible list is a palindrome in Coq)
    问题 这是我对回文的归纳定义: Inductive pal { X : Type } : list X -> Prop := | pal0 : pal [] | pal1 : forall ( x : X ), pal [x] | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ). 我想证明的定理来自软件基础: Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ), l = rev l -> pal l. 我对证明的非正式概述如下: 假设l0是一个任意列表,使得l0 = rev l0 。 那么以下三种情况之一必须成立。 l0有: (a) 零元素,在这种情况下,根据定义它是回文。 (b) 一个元素,在这种情况下,根据定义它也是回文。 (c) 两个或更多元素,在这种情况下, l0 = x :: l1 ++ [x]用于某些元素x和某些列表l1使得l1 = rev l1 。 现在,由于l1 = rev l1 ,以下三种情况之一必须成立...... 对于任何有限列表l0 ,递归案例分析将终止,因为分析的列表长度通过每次迭代减少 2。 如果它终止于任何列表ln ,则其直到l0所有外部列表也是回文
  • Coq - Induction over functions without losing information
    I'm having some troubles in Coq when trying to perform case analysis on the result of a function (which returns an inductive type). When using the usual tactics, like elim, induction, destroy, etc, the information gets lost. I'll put an example: We first have a function like so: Definition f(n:nat): bool := (* definition *) Now, imagine we are at this step in the proof of a specific theorem: n: nat H: f n = other_stuff ------ P (f n ) When I apply a tactic, like let's say, induction (f n), this happens: Subgoal 1 n:nat H: true = other_stuff ------ P true Subgoal 2 n:nat H: false = other_stuff
  • 如何指示两种Coq感应类型的尺寸减小(How to indicate decreasing in size of two Coq inductive types)
    问题 我正在尝试为组合游戏定义game归纳类型。 我想要一个比较方法来判断两个游戏是否为lessOrEq , greatOrEq , lessOrConf或greatOrConf 。 然后,我可以检查两个游戏是否相等,如果它们都是lessOrEq和greatOrEq 。 但是,当我尝试定义进行此检查的相互递归方法时,我得到: 错误:无法猜测到fix递减参数。 我认为这是因为每次递归调用时,只有一个游戏或另一个游戏的大小会减少(但不能同时减少)。 我该如何向Coq指出? 这是我的代码。 失败的部分是gameCompare , innerGCompare , listGameCompare , gameListCompare的相互递归定义。 Inductive game : Set := | gameCons : gamelist -> gamelist -> game with gamelist : Set := | emptylist : gamelist | listCons : game -> gamelist -> gamelist. Definition side := game -> gamelist. Definition leftSide (g : game) : gamelist := match g with | gameCons gll glr => gll
  • 我如何阅读 ex_intro 的定义?(How do I read the definition of ex_intro?)
    问题 我正在阅读 Mike Nahas 的介绍性 Coq 教程,其中说: “ex_intro”的参数是: 谓词证人与证人一起传唤的谓词的证明 我看了下定义: Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. 我在解析它时遇到了麻烦。 表达式forall x:A, P x -> ex (A:=A) P哪些部分对应于这三个参数(谓词、见证和证明)? 回答1 要理解 Mike 的意思,最好启动 Coq 解释器并查询ex_intro的类型: Check ex_intro. 然后你应该看到: ex_intro : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x 这表示ex_intro不仅需要 3 个参数,还需要 4 个参数: 你正在量化的事物的类型, A ; 谓词P : A -> Prop ; 证人x : A ; 和 P x的证明,断言x是有效的证人。 如果你把所有这些东西结合起来,你就会得到一个exists x : A, P x的证明exists x : A, P x 。 例如, @ex_intro nat (fun n => n = 3) 3 eq_refl是exists n, n
  • Why does Coq use unnamed parameters in Inductive Types of Propositions?
    I was looking at IndProp and I saw: Fail Inductive wrong_ev (n : nat) : Prop := | wrong_ev_0 : wrong_ev 0 | wrong_ev_SS : ∀ n, wrong_ev n → wrong_ev (S (S n)). (* ===> Error: A parameter of an inductive type n is not allowed to be used as a bound variable in the type of its constructor. *) except that it seems to behave exactly as if it was taking an argument but it seems to throw an error. Why is this? The text provides some explanation but I don't understand it: what I don't understand specifically it. The part I don't understand is the part it says: it is allowed to take different values in
  • 在 Coq 中对等式两边应用函数?(Apply a function to both sides of an equality in Coq?)
    问题 我在 Coq 试图证明这一点 Theorem evenb_n__oddb_Sn : ∀n : nat, evenb n = negb (evenb (S n)). 我在n上使用归纳法。 基本情况是微不足道的,所以我在归纳情况下,我的目标是这样的: k : nat IHk : evenb k = negb (evenb (S k)) ============================ evenb (S k) = negb (evenb (S (S k))) 现在当然有一个基本的函数公理断言 a = b -> f a = f b 对于所有函数f : A -> B 。 所以我可以对双方都申请negb ,这会给我 k : nat IHk : evenb k = negb (evenb (S k)) ============================ negb (evenb (S k)) = negb (negb (evenb (S (S k)))) 这会让我从右到左使用我的归纳假设,右边的否定会相互抵消,并且evenb的定义将完成证明。 现在,可能有更好的方法来证明这个特定的定理(编辑:有,我用另一种方式做了),但是由于这通常看起来是一件有用的事情,所以修改 Coq 中的相等目标的方法是什么?对双方应用一个函数? 注意:我意识到这不适用于任何任意函数:例如
  • 在 Coq 中建立良好的递归(Well founded recursion in Coq)
    问题 我正在尝试编写一个用于在 Coq 中计算自然除法的函数,但在定义它时遇到了一些麻烦,因为它不是结构递归。 我的代码是: Inductive N : Set := | O : N | S : N -> N. Inductive Bool : Set := | True : Bool | False : Bool. Fixpoint sum (m :N) (n : N) : N := match m with | O => n | S x => S ( sum x n) end. Notation "m + n" := (sum m n) (at level 50, left associativity). Fixpoint mult (m :N) (n : N) : N := match m with | O => O | S x => n + (mult x n) end. Notation "m * n" := (mult m n) (at level 40, left associativity). Fixpoint pred (m : N) : N := match m with | O => S O | S x => x end. Fixpoint resta (m:N) (n:N) : N := match n with | O => m | S x => pred
  • 在Coq中实现向量加法(Implementing vector addition in Coq)
    问题 在某些依赖类型的语言(例如Idris)中实现向量加法非常简单。 按照Wikipedia上的示例: import Data.Vect %default total pairAdd : Num a => Vect n a -> Vect n a -> Vect n a pairAdd Nil Nil = Nil pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys (请注意,Idris的总计检查器如何自动推断出Nil和非Nil向量的加法运算在逻辑上是不可能的。) 我正在尝试使用自定义矢量实现在Coq中实现等效功能,尽管与官方Coq库中提供的功能非常相似: Set Implicit Arguments. Inductive vector (X : Type) : nat -> Type := | vnul : vector X 0 | vcons {n : nat} (h : X) (v : vector X n) : vector X (S n). Arguments vnul [X]. Fixpoint vpadd {n : nat} (v1 v2 : vector nat n) : vector nat n := match v1 with | vnul => vnul | vcons _ x1 v1' => match
  • Coq: Prop versus Set in Type(n)
    I want to consider the following three (related?) Coq definitions. Inductive nat1: Prop := | z1 : nat1 | s1 : nat1 -> nat1. Inductive nat2 : Set := | z2 : nat2 | s2 : nat2 -> nat2. Inductive nat3 : Type := | z3 : nat3 | s3 : nat3 -> nat3. All three types give induction principles to prove a proposition holds. nat1_ind : forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P nat2_ind : forall P : nat2 -> Prop, P z2 -> (forall n : nat2, P n -> P (s2 n)) -> forall n : nat2, P n nat3_ind : forall P : nat3 -> Prop, P z3 -> (forall n : nat3, P n -> P (s3 n)) -> forall n : nat3, P n The set and type
  • 在 Coq 中使用自己的可判定性时,Eval 计算是不完整的(Eval compute is incomplete when own decidability is used in Coq)
    问题 Eval compute命令并不总是计算为一个简单的表达式。 考虑代码: Require Import Coq.Lists.List. Require Import Coq.Arith.Peano_dec. Import ListNotations. Inductive I : Set := a : nat -> I | b : nat -> nat -> I. Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}. Proof. repeat decide equality. Qed. 并且,如果我执行以下命令: Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2). Coq 告诉我结果是2 。 但是,当我执行以下表达式时: Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2). 我得到一个长表达式,其中 In-predicate 似乎展开了,但没有给出结果。 为了在最后一个Eval compute行中获得答案1 ,我需要更改什么? 回答1 在 Coq 中,有两个用于证明脚本的终止符命令: Qed和Defined 。 它们之间的区别在于前者创建了不透明项
  • Compute with a recursive function defined by well-defined induction
    When I use Function to define a non-structurally recursive function in Coq, the resulting object behaves strangely when a specific computation is asked. Indeed, instead of giving directly the result, the Eval compute in ... directive return a rather long (typically 170 000 lines) expression. It seems that Coq cannot evaluate everything, and therefore returns a simplified (but long) expression instead of just a value. The problem seems to come from the way I prove the obligations generated by Function. First, I thought the problem came from the opaque terms I used, and I converted all the
  • Coq equality implementation
    I'm writing a toy language where nodes in the AST can have any number of children (Num has 0, Arrow has 2, etc). You might call these operators. Additionally, exactly one node in the AST might be "focused". We index the data type with Z if it has a focus, or H if it doesn't. I need advice on a few parts of the code. Hopefully it's alright to ask all of these at once, since they're related. How would you define the type of internal nodes with one focus, InternalZ? Right now I say "we have S n children -- n of them are unfocused and one (at some given index) is focused. A slightly more intuitive