在我的证明中,我偶然发现了A /\ B /\ C我的假设存在的问题,我需要证明(A /\ B) /\ C.这些在逻辑上完全相同,但是coq不能解决这些问题assumption..
我一直在通过应用公理来解决这些问题,但是有更优雅(和正确)的方法来处理这个问题吗？
我试图证明一个关于道具的替代定理,而且我失败了.可以在coq中证明以下定理,如果不是,为什么不.
Theorem prop_subst:
forall (f : Prop -> Prop) (P Q : Prop),
(P <-> Q) -> ((f P) <-> (f Q)).
关键是逻辑上的证据是归纳的.就我所见,Prop没有归纳定义.如何在Coq中证明这样的定理？
关于关系Rle(<=),我可以在Rplus(+)和Rminus( - )内重写,因为两个二元运算符的两个位置都有固定的方差:
Require Import Setoid Relation_Definitions Reals.
Open Scope R.
Add Parametric Relation : R Rle
reflexivity proved by Rle_refl
transitivity proved by Rle_trans
as Rle_setoid_relation.
Add Parametric Morphism : Rplus with
signature Rle ++> Rle ++> Rle as Rplus_Rle_mor.
intros ; apply Rplus_le_compat ; assumption.
Qed.
Add Parametric Morphism : Rminus with
signature Rle ++> Rle --> Rle as Rminus_Rle_mor.
intros ; unfold Rminus ;
apply Rplus_le_compat;
[assumption | apply Ropp_le_contravar ; …在尝试在列表上的归纳谓词上编写可重用代码时,我自然会声明:
Parameter A:Type.
然后我继续定义二元谓词(例如):
Inductive prefix : list A -> list A -> Prop :=
| prefixNil: forall (l: list A), prefix nil l
| prefixCons: forall (a: A)(l m:list A), prefix l m -> prefix (a::l) (a::m).
表达了给定列表是另一个列表的前缀这一事实.然后,人们可以继续研究这种关系并显示(例如)它是一个偏序.到现在为止还挺好.但是,很容易定义一个与数学概念不符的归纳谓词.我想通过进一步定义函数来验证归纳定义:
isPrefixOf: list A -> list A -> bool
为了证明等价:
Theorem prefix_validate: forall (l m: list A),
prefix l m <-> isPrefixOf l m = true.
这是我需要限制代码的一般性的地方,因为我不能再使用了list A.在Haskell,我们有isPrefixOf :: Eq a => [a] -> [a] -> Bool,所以我理解我需要做一些假设A …
Coq'Art中的练习6.7 ,或者软件基础中的逻辑章节的最终练习:表明以下内容是等效的.
Definition peirce := forall P Q:Prop, ((P->Q)->P)->P.
Definition classic := forall P:Prop, ~~P -> P.
Definition excluded_middle := forall P:Prop, P\/~P.
Definition de_morgan_not_and_not := forall P Q:Prop, ~(~P/\~Q)->P\/Q.
Definition implies_to_or := forall P Q:Prop, (P->Q)->(~P\/Q).
解决方案集通过一个循环的含义链表达了这一点,使用了五个独立的引理.但是"TFAE"证明在数学中很常见,我想用它来表达它们.Coq中有一个吗？
假设我们有以下形式的结论：a + b + c + d + e。
我们还有一个引理：plus_assoc : forall n m p : nat, n + (m + p) = n + m + p。
将术语任意“插入一对括号”的惯用方法是什么？也就是说，如果有多个可用位置，我们如何轻松地选择重写位置。
我最终要做的事情如下：
replace (a + b + c + d + e)
with (a + b + c + (d + e))
by now rewrite <- ?plus_assoc
尽管此公式确实说明了我要执行的操作，但是对于比“ ab c ...”更复杂的公式而言，它变得非常漫长。
当在Ltac中实现复杂的策略时,有一些Ltac命令或策略调用我期望失败以及预期的位置(例如终止a repeat或导致回溯).这些故障通常在故障级别0时引发.
在较高级别上升的故障"逃离"周围try或repeat阻塞,并且对于发出意外故障是有用的.
我缺少的是一种运行策略tac并将其失败(即使在0级)处于更高水平,同时保留失败信息的方法.这将让我确保repeat不会因为我身边的Ltac编程错误而终止.
我能否在Ltac中实施这种提升级别的高阶战术？
考虑以下发展:
Require Import Relation RelationClasses.
Set Implicit Arguments.
CoInductive stream (A : Type) : Type :=
| scons : A -> stream A -> stream A.
CoInductive stream_le (A : Type) {eqA R : relation A}
`{PO : PartialOrder A eqA R} :
stream A -> stream A -> Prop :=
| le_step : forall h1 h2 t1 t2, R h1 h2 ->
(eqA h1 h2 -> stream_le t1 t2) ->
stream_le (scons h1 t1) (scons h2 t2).
如果我有一个假设stream_le …
我试图去通过著名的和精彩的软件基础的书,但我到这里的例子simpl.和reflexivity.刚做多在幕后,并阻碍了我的学习和理解.
我正在经历以下定理:
Theorem plus_1_neq_0 : forall n : nat,
beq_nat (n + 1) 0 = false. (* n+1 != 0 *)
Proof.
intros n.
destruct n as [| n'].
-simpl. reflexivity.
-simpl. reflexivity.
Qed.
我真正想要的是什么,让我一步该怎么走至步骤simpl.和reflexivity.所做.有什么东西可以让我这样做吗？
Destruct可以解决以下问题:
因为第一个参数beq_nat(这只是
not equal如!=)不匹配,但第一输入取决于未知的变量n和同样的事情,+这样的匹配不能做任何事情,这样做simpl.会让我们卡住了(出于某种原因).
它显然必须解决它,因为Coq后来接受了证据.但如果仔细观察第二个目标是什么,似乎重新引入了与上述相同的问题:
2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false
现在我们已经n' 为双方的第一个参数beq_nat …
I'm trying to formalize each integer as an equivalence class of pairs of natural numbers, where the first component is the positive part, and the second component is the negative part.
Definition integer : Type := prod nat nat.
I want to define a normalization function where positives and negatives cancel as much as possible.
Fixpoint normalize (i : integer) : integer :=
let (a, b) := i in
match a with
| 0 => (0, b)
| S a' …