标签: theorem-proving

我正在使用组合逻辑进行定理验证的一些实验,这看起来很有希望,但是有一个绊脚石:已经指出在组合逻辑中,确实例如I = SKK但这不是一个定理,它必须添加为公理.有谁知道需要添加的公理的完整列表？

编辑:您当然可以手工证明我= SKK,但除非我遗漏了某些东西,否则它不是具有相等性的组合逻辑系统中的定理.话虽如此,你可以将我扩展到SKK ......但我仍然缺少一些重要的东西.取一组子句p(X)和~p(X),这很容易解决普通一阶逻辑中的矛盾,并将它们转换为SK,执行替换并评估S和K的所有调用,我的程序生成以下(我使用'用于Unlambda的反击):

''eq''s'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''' 'k true'k true

看起来我可能需要的是一套适当的规则来处理部分调用'k和',我只是没有看到这些规则应该是什么,我在这个领域找到的所有文献都是为数学家的目标受众而不是程序员.我怀疑一旦你明白答案可能很简单.

我有一些混淆使用通用量词和declare-const而不使用forall

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

我可以这样写:

(declare-const x Int)
(assert  (>= (f x x) (+ x a))))

在这两种情况下,使用Z3将探索Int类型的所有可能值.那有什么区别？我真的可以使用declare-const来消除forall量词吗？

我有一个简单的定理,我想通过案例证明.下面给出一个例子.

Goal forall a b : Set, a = b \/ a <> b.
Proof
  intros a b.
  ...

我将如何解决这个问题.而且,我究竟如何使用两个可能的相等值(True或False)来定义证明？

任何帮助,将不胜感激.谢谢,

Isabelle中的“商型模式”是什么？

我在互联网上找不到任何解释。

有没有办法在Coq中承认断言？

假设我有一个这样的定理：

Theorem test : forall m n : nat,
    m * n = n * m.
Proof.
  intros n m.
  assert (H1: m + m * n = m * S n). { Admitted. }
Abort.

上面的断言似乎对我不起作用。

我收到的错误是：

Error: No focused proof (No proof-editing in progress).

我想要的是undefinedHaskell中的东西。Baiscally，我稍后会再次证明这一点。在Coq中有类似的东西可以实现吗？

我想编写一个函数,它接受两个自然参数,并返回一个可能的相等证明.

我正在尝试

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal a b = case (a == b) of
    True => Just Refl
    False => Nothing

但是我收到以下错误

When checking argument x to constructor Prelude.Maybe.Just:
        Type mismatch between
                True = True (Type of Refl)
        and
                Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a
                                                                                   b =
                True (Expected type)

        Specifically:
                Type mismatch between
                        True
                and
                        Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a
                                                                                           b

这是正确的方法吗？

而且,作为奖金问题,如果我这样做

equal : …

所以,我有一个看起来像这样的证据:

induction t; intros; inversion H ; crush.

它解决了我的所有目标,但是当我这样做时Qed,我收到以下错误:

Cannot guess decreasing argument of fix.

因此,在生成的证明术语的某处,存在非有根据的递归.问题是,我不知道在哪里.

有没有办法调试这种错误,或者看到战术脚本生成的(可能是非暂停的)证明术语？

我已经证明是等效的and_distributes_over_or：

Theorem and_distributes_over_or : forall P Q R : Prop,
  P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).

在其他地方，我的目标是

exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 xs)

（有关背景，我通过工作逻辑基础 ;我上了In_map_iff建设性的逻辑章的练习，请不要告诉我解决了运动虽然。！）

我试图用rewrite and_distributes_over_or自己的目标来获得exists x0 : A, (f x0 = y /\ x = x0) \/ (f x0 = y /\ In x0 xs)。我收到一个错误：

Found no subterm matching "?P …

我试图证明基于以下定义的引理。

Section lemma.

Variable A : Type.
Variable P : A -> Prop.

Variable P_dec : forall x, {P x}+{~P x}.

Inductive vector : nat -> Type :=
  | Vnil : vector O
  | Vcons : forall {n}, A -> vector n -> vector (S n).

  Arguments Vcons {_} _ _.

Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') …

Type和SetCoq 之间是否存在平等或不平等关系？

我正在学习Coq的类型系统，并了解Setis Type@{Set+1}的类型和Type@{k}is 的类型Type@{k+1}。我试图证明Type = Set，然后试图证明 Type <> Set，但是在两种情况下都失败了。

我开始

Lemma set_is_type :  Type = Set.
Proof.
reflexivity.

这将显示一条错误消息，指出无法将“ Set”与“ Type@{Top.74}”统一。

然后我尝试

Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.

此时，我不知道如何进行。这个策略discriminate没有用，也没有用inversion contra。

可以证明上述两个引理中的哪一个？