如何读取coq量词` `forall : Set -> Prop`？
coq量词forall : Set -> Prop是Coq语言中的一个重要概念，用于表示全称量化。它的含义是对于给定的集合（Set）中的每个元素，都满足某个性质（Prop）。
在Coq中，forall量词用于定义命题，即一种可以被证明或推导的陈述。它可以用来表示普遍性的断言，例如对于所有的自然数，某个性质都成立。
读取forall : Set -> Prop的方法是将其分解为两部分来理解。首先，Set表示一个集合，可以是任意类型的集合，例如自然数集、布尔值集等。而Prop表示命题，即一个可以被证明或推导的陈述。
因此，forall : Set -> Prop表示对于给定的集合，我们可以定义一个命题，该命题对于集合中的每个元素都成立。
举个例子，假设我们有一个集合A表示所有的自然数，那么forall x : A, P(x)表示对于集合A中的每个元素x，都满足性质P(x)。
在Coq中，我们可以使用forall量词来定义这样的命题，并使用其他的逻辑连接词和证明策略来推导和证明这些命题。
关于Coq的更多信息和使用方法，您可以参考腾讯云的Coq相关产品和文档：
请注意，以上提供的链接和信息仅供参考，不代表对腾讯云产品的推荐或支持。
相关·内容
我对Coq在处理存在主义量化的过程中感到困惑。
我有一个谓词P和一个假设H
P : nat -> Prop
H : exists n, P n
而目前的目标是(不管什么)
(Some goal)
如果我想在H中实例化n，我会这样做
elim H.
然而，在淘汰之后，当前的目标变成
forall n, P n -> (Some goal)
它看起来像是Coq将一个存在量词转换为一个通用量词。我知道(forall a，p a -> Q) -> ((存在a，P) -> Q)是我对一阶逻辑的有限知识。但相反的说法似乎是不正确的。如果“forall”1和“存在”1不是等价的
浏览 3提问于2015-06-03得票数 3
回答已采纳
1回答
如何在Coq中描述一个集合Y是另一个集合X的子集
我测试了以下内容：
Definition subset (Y X:Set) : Prop :=
forall y:Y, y:X.
，试图表达如果元素y在Y中，那么y在X中。但这会产生有关y的类型错误，这并不奇怪。
有没有一种在Coq中定义subset的简单方法？
浏览 6提问于2016-07-24得票数 5
回答已采纳
我试图证明一个关于Prop的替换定理，但我失败得很痛苦。下面的定理能在coq中被证明吗?如果不能，为什么不能。
Theorem prop_subst:
forall (f : Prop -> Prop) (P Q : Prop),
(P <-> Q) -> ((f P) <-> (f Q)).
重点是，在逻辑上，证明是通过归纳的。据我所知，Prop不是归纳定义的。如何在Coq中证明这样的定理？
浏览 2提问于2012-06-17得票数 7
如何证明( /\ x，P，Q) -> (forall x，P)在Coq中？我尝试了几个小时，但不知道如何将前置条件分解为Coq可以消化的东西。(很明显，我是个新手:)
浏览 0提问于2009-05-07得票数 7
回答已采纳
Coq的Finite_sets库具有归纳类型，指定某些集合是有限的：
Inductive Finite : Ensemble U -> Prop :=
| Empty_is_finite : Finite (Empty_set U)
| Union_is_finite :
forall A:Ensemble U,
Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
我试图证明有限集合中的成员是可决定的，如下所示：
Lemma Finite_dec (A:Type) : forall f:Ensembl
浏览 0提问于2016-09-29得票数 3
就像的op一样，我正在根据实际情况在-nois下重新开发Coq.Init.Prelude。
我想用战术，但他们没有用。
我试过Declare ML Module "ltac_plugin".，但没有用。
Welcome to Coq v8.8 (eccf1d50b020e87b4d19d0bda43361e1e82d01b1)
Coq < Declare ML Module "ltac_plugin".
[Loading ML file ltac_plugin.cmxs ... done]
Coq < Goal forall A:Prop, fo
浏览 0提问于2018-06-19得票数 2
回答已采纳
2回答
我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。
在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。
Coq < Parameter Antecedent : Prop .
Coq < Parameter Consequent : Prop .
Coq < Conjecture Minor : Antecedent .
Coq < Conjecture Major : Antecedent -> Consequent .
有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Ma
浏览 4提问于2014-05-06得票数 0
2回答
我仍然不明白Set在Coq中意味着什么。何时使用Set，何时使用类型
在Hott中，集被定义为一种类型，其中标识证明是唯一的。但我认为Coq有不同的解释。
浏览 1提问于2016-09-20得票数 17
回答已采纳
我很好奇在逻辑中等效于连接词的Coq实体的类型。为了具体起见，让我们假设->和/\。如果->是一个神奇的非头等实体，那么让我们使用/\作为实体。我很好奇它的域名是Prop还是Set。
是否可以使用coqtop获取表达式的类型？
我想用ghci做一些类似于下面的事情。
> ghci
:GHCi, version 8.6.3: :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a
浏览 0提问于2019-01-08得票数 1
回答已采纳
1回答
有人能在谓词逻辑和使用coq方面帮助这两个定理吗？我很难理解coq语法。
存在x:D，(R /\ S)x-(存在y:D，R) /\ (存在z:D，S)存在x:D，(R \/S)x-(存在y:D，R)\/(存在z:D，S)
浏览 1提问于2020-11-08得票数 0
我正在尝试Coq，但我不完全确定我在做什么。是：
Theorem new_theorem : forall x, P:Prop /\ Q:Prop
等同于：
∀x ( P(x) and Q(x) )
编辑:我想是的。
浏览 3提问于2009-04-15得票数 2
1回答
我正在努力证明以下定理(假设域为非空域)： Theorem t (A: Set) (P: A -> Prop): (forall a: A, P a) -> (exists a: A, P a).
Proof.
intros H. 通常，有了forall a: A, P a，我会推导出P c，其中c是一个常量。即forall量词将被消除。一旦完成，我将再次推导exists a，并且我的简单证明将是Qeded。 然而，我找不到正确的方法来消除forall在Coq中的影响。 我是新手，我想知道如何消除Coq中的forall，或者证明上述定理的更好方法是什么？ 附言:我已经看过th
浏览 34提问于2021-08-11得票数 2
回答已采纳
1回答
根据Coq的文件
sumbool是一种布尔类型，具有其值的合理性。
我认为，在Coq实现的直观(或建设性)逻辑中，这已经是分离的一个属性。
例如，要证明Coq中排除的中间p \/ ~p，必须做实际工作，这不是一个逻辑公理。因此，p \/ q的证明必须是p的证明或q的证明。
那我们为什么需要sumbool p q呢？
编辑
通过用精确的证据代替战术，我得到了更具体的错误信息。这个很好：
Lemma sumbool_or : forall p q : Prop, sumbool p q -> p \/ q.
Proof.
exact (fun (p q : Prop) (H :
浏览 2提问于2018-07-11得票数 5
回答已采纳
2回答
在Coq中拆分带有合取结论的前提
、、、、
我经常不得不做“归纳加载”来证明Coq中的目标，在Coq中，我通过归纳同时证明多个事情。
问题是，我经常会得到以下形式的归纳假设：
forall a1 ... an,
Premise1 -> Premise2 -> ... Premisek ->
Conclusion1 /\ Conclusion2 /\ ... Conclusion_m
这很好，但是像eauto这样的策略真的不知道如何处理这样的事情，所以它在大多数情况下会扼杀自动化。
我想知道的是，有没有一种方法可以自动将这样的前提分解为m不同的前提，即
forall a1 ... an,
Premise
浏览 4提问于2018-10-23得票数 1
1回答
我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢？
例如，我想将一个定义写为：
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在Coq中可以这样做吗？
浏览 5提问于2020-11-04得票数 1
我们可以将Coq中的分配给Prop、Set和每个Type_i吗？我只在Coq的库中看到了的定义，所以也许我们首先需要大基数的定义。
根据证明无关的语义，例如暴露的，Set和Type_i形成一个递增的序列。这可以在Coq中得到证明吗？
由于不可预测性，Prop看起来更复杂。证明无关意味着我们识别同一P : Prop的所有证明，并将Prop本身解释为{false, true}对。因此，Prop的基数应该是2。但是，对于任何两个证明p1 p2 : P，Coq不接受eq_refl p1作为p1 = p2的证明。因此，Coq并不能完全识别p1和p2。另一方面，不可预测性意味着对于任何A : Type和P
浏览 13提问于2018-08-28得票数 4
回答已采纳
1回答
让我们假设：
Axiom inverse1: forall a:G, exists b:G, P a b.
Axiom only_one: forall a b1 b2:G, P a b1 /\ P a b2 -> b1 = b2.
这两个公理定义了一个映射G -> G。我想把这个映射定义为一个Coq函数。
浏览 2提问于2015-03-08得票数 1
考虑关系的自反传递闭包：
Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : star r x x
| star_step x y z : r x y -> star r y z -> star r x z.
如何在Coq中给出表示法，以便编写x ->* y，或者添加一个下标来表示关系->__r。这在伊莎贝尔身上是可能的。在Coq有干净的方法吗？
浏览 1提问于2020-04-02得票数 2
回答已采纳
我是一个全新的Coq新手，正在学习Mike Nahas的教程：。具体地说，我在理解下面的陈述时遇到了困难：
Theorem forall_exists : (forall P : Set -> Prop, (forall x, ~(P x)) -> ~(exists x, P x)).
这是我到目前为止的解释，欢迎更正。
语句Set -> Prop是一个可以扩展为forall s: Set, Prop的命题，我将其理解为“对于Set的每个证明(读取实例)，我们也有一个Prop的证明(实例)”。
因此，forall P : Set -> Prop可以粗略地理解为“对于一
浏览 14提问于2019-11-21得票数 2
回答已采纳
1回答
“`le`”的归纳原则
、、、
对于归纳类型nat，生成的归纳原则在其语句中使用构造函数O和S：
Inductive nat : Set := O : nat | S : nat -> nat
nat_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) -> forall n : nat, P n
但是对于le，生成的语句不使用构造函数le_n和le_S。
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S :
浏览 0提问于2019-03-16得票数 1
回答已采纳
1回答
我想证明一些FOL的等价性。我很难用德摩根定律来表示量词，特别是
~ (exists x. P(x)) <-> forall x. ~P(x)
我试着应用Coq.Logic.Classical_Pred_Type.的Coq.Logic.Classical_Pred_Type，并搜索了StackOverflow (，)，但都没有解决这个问题。
Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop,
~(exists (x: T), ((p x) /\ (exist
浏览 5提问于2019-07-04得票数 0
回答已采纳
我正在阅读Coq (8.5p1)参考手册，
introduction via (p1 &.& pn)是(p1，(.，(…，(…，pn).)引入的一条捷径，它期望假设是一系列右结合的二进制归纳构造函数，如conj或ex_intro；例如，A/(存在x，B/\C/\D)类型的假设可以通过模式(a &x&b&c&d)引入；
为了检验这个，我做了：
Goal forall A B C D: Prop, A/\(exists x:nat, B/\C/\D) -> D.
intros (a & x & b & c &am
浏览 5提问于2016-06-24得票数 1
回答已采纳
2回答
在一部电影中有这样的逻辑，我不能很好地形式化(例如在Coq中)。
有人想在他的农场上发射火箭，监视现场的FBI人员正在互相谈论他们为什么会在那里。一个人说：
因为如果我们不在这里，他发射，我们将看起来像*s。
然后另一个人回应说
如果我们在这里而他发射了呢？
答：
我们看起来还是像*s。
这里的逻辑似乎是这样的：
A = we look foolish
B = he launches
C = we are not here.
我们有
B /\ C -> A and
B /\ ~C -> A
此外，似乎C (我们在这里)是否成立并不重要。这一结论归结
浏览 2提问于2015-12-09得票数 1
回答已采纳
2回答
在中，可以读到：
Coq的标准库采用了一种与实数非常不同的方法:公理化方法。
我们可以找到以下公理
Axiom
completeness :
∀E:R → Prop,
bound E → (∃x : R, E x) → { m:R | is_lub E m }.
没有提到库，但是在中可以找到相同的描述：
我想知道Coq是把实数定义为Cauchy序列还是Dedekind割集，所以我检查了Coq.Reals.Raxioms和.这两个人都没有。实数是公理化的，以及它们的运算(作为参数和公理)。为什么会这样呢？而且，实数严格依赖于子集的概念，因为它们的一个定义性质是，
浏览 0提问于2021-10-22得票数 8
回答已采纳
1回答
伊莎贝尔是一种逻辑框架。你可以用元理论介绍一个逻辑的公理和规则以及关于它们的理由。例如，您可以在Isabelle发行版的IFOL.thy中看到直观一阶逻辑的编码。这里是量词常量的声明：
typedecl o
judgment
Trueprop :: ‹o ⇒ prop› (‹(_)› 5)
axiomatization
All :: ‹('a ⇒ o) ⇒ o› (binder ‹∀› 10) and
Ex :: ‹('a ⇒ o) ⇒ o› (binder ‹∃› 10)
where
allI: ‹(⋀x. P(x)) ⟹ (∀x. P(x))› a
浏览 1提问于2020-08-24得票数 1
回答已采纳
，它看起来像Coq中使用的归纳构造的演算，对于归纳类型有不相交的内射构造函数。
在普通的构造演算(例如，没有原始归纳类型)中，对类型(例如，∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat)使用模拟编码，这仍然是正确的吗？我能始终找出使用了哪个“构造函数”吗？此外，内射性(如在∀a b.I a = I b → a = b中)是否可在带有Prop或非谓词集的Coq中证明？
。
浏览 3提问于2017-05-03得票数 3
回答已采纳
1回答
仅当返回类型为Prop时，Coq才接受match的Prop证明(即只产生另一个证明)。据我所知，这避免了以下矛盾：
Require Import Hurkens.
Inductive BoolProp : Prop :=
| falseP : BoolProp | trueP : BoolProp.
Axiom b2p : BoolProp -> Prop.
Axiom b2p_spec : b2p falseP = False /\ b2p trueP = True.
Axiom EM : forall P:Prop, P \/ ~P.
Definition p2b (P : P
浏览 16提问于2019-08-08得票数 1
1回答
如何在coq中显式使用归纳法？
、、、、
我试图在Coq中显式地证明命题恒等式的对称性，但不能像在agda中那样用归纳原理来证明。我不知道如何在Coq中在本地声明变量，也不知道如何展开定义，如下所示。我怎么能得到类似于agda的证据呢？
Inductive Id (A : Type) (x : A) : A -> Type :=
| refl : Id A x x.
(* trivial with induction *)
Theorem symId {A} {x y} : Id A x y -> Id A y x.
Proof.
intros.
induction H.
apply refl.
Qed.
浏览 3提问于2020-04-26得票数 2
回答已采纳
我可以像这样在Coq中定义有限类型： Inductive fin : nat -> Set :=
| FZ : forall {n}, fin (S n)
| FS : forall {n}, fin n -> fin (S n).
Definition void := fin 0.
Definition unit := fin 1.
Definition vunit : unit := FZ.
Definition bool := fin 2.
Definition true : bool := FZ.
Definition false : bool := FS FZ.
浏览 20提问于2020-09-04得票数 4
回答已采纳
1回答
我对尝试使用Coq构建集合论很感兴趣。我想定义一个类型sets，但不指定它的成员是什么，以及一个将两个集合映射到一个属性的函数 Definition elem (s1 s1 : sets) : Prop. 然后我会建立集合论假设的公理，并将定理表达为(例如) Theorem : ZFC -> (forall s : sets, ~ elem s s). 但是，上面的语法不起作用。这个想法可以在Coq中实现吗？在Coq中有没有更好的方法来实现这个目标？我是Coq的新手，所以如果有一种我不知道的明显的方法，我很抱歉。
浏览 10提问于2020-08-21得票数 1
回答已采纳
1回答
在Coq中表示n m : nat是相邻偶数的一种可能的方法是归纳地定义这种关系，从0和2开始。
Inductive adj_ev : nat -> nat -> Prop :=
| ae_0 : adj_ev 0 2
| ae_1 : forall ( n m : nat ), adj_ev n m -> adj_ev m ( S ( S m ) )
| ae_2 : forall ( n m : nat ), adj_ev n m -> adj_ev m n.
ae_0表示0和2是相邻的偶数。ae_1指出，如果某些n m : nat是相邻的偶数，那么m和m + 2也是
浏览 4提问于2014-07-16得票数 1
回答已采纳
1回答
我正在研究字符串语法的理论，但我完全被一个特殊的定理所阻碍。我尝试过的每一种归纳法都以毫无意义和无用的归纳法假设而告终，我不确定我错过了什么。 我现在已经多次重读了这一"Varying the Induction Hypothesis"部分，试图理解我做错了什么，但似乎我很好地遵循了他们关于通用性的建议。 简单地说，我很困惑。非常感谢您的提前指导！ 下面是我的定义和困难定理的概述。稍后我会给出完整的脚本。 (* I plan to make these definitions more complex in the future *)
Definition TokenDefi
浏览 16提问于2020-12-19得票数 0
回答已采纳
我正在遵循中的说明，并试图定义一个新的表示法。(而不是用在网页中但似乎被我的coq解释为OR运算符的\{e76f})
Reserved Notation "e |\ n" (at level 50, left associativity).
但是coq仍然认为\\是一个未定义的运算符。
Inductive aevalR : aexp -> nat -> Prop :=
| E_ANum : forall n : nat, (ANum n) |\ n.
错误:符号"_声\ _“的未知解释。
我的coq版本是8.4pl6(2015年11月)。我怎样才
浏览 2提问于2015-12-24得票数 1
回答已采纳
我如何在Coq中证明以下内容？
Variables f g : nat->nat.
Hypothesis Hfg : forall x, f x = g x.
Variable F : (nat->nat)->nat.
Goal F f = F g.
我们有两个函数，f和g，它们不一定相等，但它们是等价的。例如，f x可以是0+x，g x可以是x+0。
F返回一个nat，而且由于F不能查看它的函数参数，所以返回的值应该是相同的，无论它是fed f还是g。我该怎么证明呢？
(它等价于Proper ( f_eq ==> eq) F的一个证明，其中f_eq = forall
浏览 0提问于2018-07-11得票数 3
2回答
我试图证明在一个术语上应用空代换等于给定的术语。代码如下：
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Arith.EqNat.
Require Import Recdef.
Require Import Omega.
Import ListNotations.
Set Implicit Arguments.
Inductive Term : Type :=
| Var : nat -> Term
| Fun : string ->
浏览 26提问于2017-08-31得票数 2
回答已采纳
在以下Coq代码片段(从实际示例中减少)中，我试图将第一个参数声明为exponent_valid的隐式参数：
Require Import ZArith.
Open Scope Z.
Record float_format : Set := mk_float_format {
minimum_exponent : Z
}.
Record float (fmt : float_format) : Set := mk_float {
exponent : Z;
exponent_valid : minimum_exponent fmt <= exponent
}.
Argu
浏览 0提问于2015-01-22得票数 3
回答已采纳
1回答
我刚开始用Coq。
我如何定义命题myProp，使得给定集H，myProp H是真当且仅当
？
特别是，如何表达H是命题中nat的子集这一事实？或者，我如何简单地声明，让H是nat的一个子集
浏览 2提问于2017-08-05得票数 2
回答已采纳
为了尽可能地隔离这个问题，假设我开始一个Coq会话，如下所示。
Parameter A : Type.
Parameter B : Type.
Parameter P : A -> B -> Prop.
Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.
从这里开始，我想将函数f : A -> B定义为P a (f a)始终为真的唯一
浏览 0提问于2012-10-22得票数 1
回答已采纳
我正在阅读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)所以check让我看一看“对象”的类型，对吗？所以unit_ind有以下类型：
forall P : unit -> Prop, P tt -> forall u : unit, P
浏览 9提问于2018-12-17得票数 1
1回答
我刚刚了解到'record‘关键字可以用来定义一个Prop类型，例如： Record Equivalence (A : Type) (R : relation A) : Prop := Build_Equivalence
{ Equivalence_Reflexive : Reflexive R;
Equivalence_Symmetric : Symmetric R;
Equivalence_Transitive : Transitive R } 但是当我尝试使用记录来定义一个命题时，如下所示： Record proprecord : Prop := Build
浏览 20提问于2020-09-02得票数 1
回答已采纳
1回答
我试图在中找到一个类似几何学中的直线公理的公理:如果给定两点，这两点之间就有一条线。我想看看如何在Coq中定义这一点。从本质上来说，选择这个简单的行公理来了解一些非常原始的东西是如何定义的，因为我很难在自然语言之外来定义它。
具体来说，我已经看到了这两个公理，并想知道在Coq中如何定义这两个公理：
任何两个不同的点总是确定一条线。
一条线的任意两个不同的点决定了这条线的唯一。
似乎您可以将它们合并到一个定义中，所以我想看看如何在Coq中编写这个定义。
我真的不知道怎么写Coq，只是想看看他们是怎么做的。但如果我试一试的话：
Axiom line : forall ptA
浏览 1提问于2019-03-01得票数 1
回答已采纳
我试图在Coq中证明以下几点：
目标(对于所有x:X，P(x) /\ Q(x)) -> ((对于所有x:X，P (x)) /\ (对于所有x:X，Q(X)。
有人能帮帮忙吗？我不确定是否要拆分，做一个假设等等。
很抱歉我是个彻头彻尾的菜鸟
浏览 0提问于2010-05-05得票数 3
1回答
是否有一个完备的Coq图库来证明简单定理？
我想学习如何证明简单的东西："G1，G2是同构的当且仅当它们的补语是同构的“。
是否有相关的/类似的例子或教程？
浏览 3提问于2014-07-15得票数 10
回答已采纳
我正在研究Coq，并试图证明Martin-Lof的等式与路径归纳法的同构。
我将这两个等式定义如下。
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : forall x y : A, eq A x y -> Prop),
(forall x : A, C x x (refl A x)) ->
forall a b : A, forall
浏览 2提问于2017-08-03得票数 4
回答已采纳
下面是一个更大的证明的简化片段，它捕获了有问题的行为。
Section foo.
Parameter t : Type.
Parameter x : t.
Parameter y : t.
Parameter prop : x = y <-> True.
Parameter prop2 : x = y.
Lemma lemma : forall e : t, x = y.
rewrite prop2.
intro e; trivial.
Qed.
End foo.
当您用rewrite prop替换rewrite prop2时，coq
浏览 0提问于2011-11-17得票数 3
1回答
我有一个归纳定义如下的公式：
Parameter world : Type.
Parameter R : world -> world -> Prop.
Definition Proposition : Type := world -> Prop
(* This says that R has only a finite number of steps it can take *)
Inductive R_ends : world -> Prop :=
| re : forall w, (forall w', R w w' -> R_ends
浏览 5提问于2017-03-24得票数 1
回答已采纳
这应该是一个简单的问题。我是Coq的新手
我想在Coq中定义异或(据我所知，它不是预定义的)。重要的部分是允许多个命题(例如Xor A、B、C、D)。
我还需要这两个属性：
(Xor A1 A2 ... An)/\~A1 -> Xor A2... An
(Xor A1 A2 ... An)/\A1 -> ~A2/\.../\~An
我目前在为未定义数量的变量定义函数时遇到了问题。我试着手动定义两个、三个、四个和五个变量(这就是我需要的数量)。但是，证明这些性质是一件痛苦的事情，而且效率似乎非常低。
浏览 0提问于2011-07-20得票数 5
回答已采纳
这个引理能在Coq中被证明吗？ Lemma liftExists : forall (P : nat -> nat -> Prop),
(forall n:nat, exists p:nat, P n p)
-> exists (f : nat -> nat), forall n:nat, P n (f n). 简单的destruct不能编译，因为我们不能消除sort Prop中的对象exists p:nat, P n p，从而在sort Set中生成函数f。 如果Coq不能证明这个引理，那么forall n:nat, exists p:nat, P n p的
浏览 17提问于2019-03-01得票数 1
回答已采纳
主要的问题是，我不能定义这样一个归纳命题：
Inductive forces : nat -> Prop :=
| KM_cond (n : nat) : ~ forces 0 ->
forces n.
事实上，我正试图定义直觉逻辑的克里普克语义。
Inductive forces (M : Kripke_model) (x : world) : prop -> Prop :=
| KM_cond (A B : prop) : set_In x (worlds M) ->
(forall y, (rel M) x y -> (
浏览 0提问于2020-03-26得票数 3
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
