在 Coq 中证明一个定理几乎只用重写——没有“聪明”

Posted

技术标签:

【中文标题】在 Coq 中证明一个定理几乎只用重写——没有“聪明”【英文标题】:Proving a theorem in Coq using almost only rewrites - no "cleverness" 【发布时间】:2016-01-23 18:20:44 【问题描述】:

我正在尝试制定一个问题,以便仅重写就足够了 来证明目标。我想避免“聪明”地使用命题,而是使用 可以由 Coq 计算的布尔值。

我定义了一个布尔测试函数member,如果元素在列表中,则返回真, 和different,如果两个列表中都没有元素,则返回 true。

我想证明我可以仅使用memberdifferent 重写为表达式。

Theorem different_member:  forall xs ys y,
  different xs ys = ((negb (member y ys)) || negb (member y xs)).

(negb X || Y) 形式是布尔含义)。

作为热身和现实检查,我想证明

Theorem diff_mem:
forall xs ys,
   different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

继续的方法是在 xs 上进行归纳,但我一直在搞砸最后一步。

非常感谢您对这两个定理的帮助!这是开发的相关部分。

Require Import Arith.
Require Import List.
Require Import Bool.
Import List.ListNotations.
Open Scope list.
Open Scope bool.

Fixpoint member x ys :=
  match ys with
    | [] => false
    | y :: ys' => (beq_nat x y) || (member x ys')
  end.

Lemma mem1: forall x,     member x []     = false.
Proof. auto. Qed.
Lemma mem2: forall x y l, member x (y::l) = (beq_nat x y) || (member x l).
Proof. auto. Qed.

Fixpoint different xs ys :=
  match xs with
    | [] => true
    | x::xs' => (negb (member x ys)) && (different xs' ys)
  end.

Lemma diff1: forall ys, different [] ys = true.
Proof. auto. Qed.
Lemma diff2: forall x xs ys,
               different (x::xs) ys = (negb (member x ys)) && (different xs ys).
Proof. auto. Qed.


Theorem diff_mem1: forall xs ys, different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

Proof.
Abort.

Theorem different_member:
  forall xs ys y, different xs ys =
                ((negb (member y ys)) || negb (member y xs)).
Proof.
Abort.

编辑:

这是diff_mem1 定理的证明。 (睡在上面,在 ProofGeneral 中开始尝试之前思考有时会有所帮助......)。另一个定理的证明遵循相同的结构。

但是,问题和最终目标仍然是如何通过重写和提示完全解决它,以便(几乎)可以做到induction xs; auto.

Theorem diff_mem1: forall xs ys, 
 different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

Proof.
  induction xs as [|a xs]; intros ys Hdiff y Hxs Hys.
  - inversion Hxs.
  - (* we assume y is a member of ys, and of (a::xs) *)
    (* it is also assumed that (a::xs) is different from ys *)
    (* consider the cases y=a and y<>a *)
    remember (beq_nat y a) as Q; destruct Q.
    + (* this case is absurd since y is a member of both ys and (y::xs) *)
      apply eq_sym in HeqQ; apply beq_nat_true in HeqQ.
      subst a.
      simpl in Hdiff.
      rewrite Hys in Hdiff.
      inversion Hdiff.
    + (* this case is also absurd since y is a member of both ys and xs *)
      simpl in Hdiff, Hxs.
      rewrite <- HeqQ in Hxs.
      simpl in Hxs.
      rewrite Bool.andb_true_iff in Hdiff; destruct Hdiff as [_ Hdiff1].
      destruct (IHxs ys Hdiff1 y Hxs Hys).
Qed.

EDIT2:

我将关闭它,因为@Arthur 给出了关于我为什么在最初尝试中失败的正确答案,但为了完整起见,我想按照我的目标添加一个解决方案。

我写了一个 Ltac 策略 my_simple_rewrite,它执行了许多 try rewrite with lemma_x in *(大约 20 个不同的引理,仅从左到右重写)。它们是关于bools 和上面的mem1mem2diff1diff2 的简单引理。为了证明这个定理,我使用了它,只指定了归纳变量xsbool表达式进行案例分析(使用自制的Ltacbool_destruct),得到以下证明。

Theorem different_member:
  forall xs ys, different xs ys = true ->
                forall y, ((negb (member y ys)) || negb (member y xs)) = true.
Proof.
  induction xs as [| a xs]; intros; my_simple_rewrite.
  - congruence.
  - try
      match goal with
        | [ HH:_ |- _] => (generalize (IHxs ys HH y); intro IH)
      end;
    bool_destruct (member a ys);
    bool_destruct (member y ys);
    bool_destruct (member a xs);
    bool_destruct (member y xs);
    bool_destruct (beq_nat y a);
    my_simple_rewrite;
    congruence.
Qed.

我们的想法是这几乎可以自动化。选择要破坏的术语可以自动进行,并注意它会尝试用任何它可以抛出的东西来实例化归纳假设 - (“如果它有效,很好!否则尝试下一个替代方案......”)。

供以后参考,完整的开发在https://gist.github.com/larsr/10b6f4817b5117b335cc

【问题讨论】:

你使用的是什么版本的 Coq?我有 8.4pl6,它抱怨 Import List.ListNotations.,没有找到该模块(也有几个变体,如添加 Require 或删除 List. 前缀等)删除该行并添加 Notation "[]" := nil. 使该示例对我有用.我会尝试一下,看看能不能帮上忙…… 试试Import ListNotations 尝试了几件事后,我想我会放弃。我倾向于遇到各种情况,我得到… = false,然后你仍然必须以非显而易见的方式在bools 周围洗牌才能得到true = false,而使用Props 你' d 那时有False 并且可以将其杀死。使用… = true -&gt; … … = false -&gt; … 的辅助引理来处理各种事情,这可能会更容易,但这将是很多工作。拥有Prop 并来回反映(至少对于获得基本帮助引理)的“标准”方法(?)可能更简单。为什么不试试呢? 【参考方案1】:

你的结果的问题是它不成立。例如,尝试

Compute different [2] [1; 2]. (* false *)
Compute (negb (member 1 [2]) || negb (member 1 [1; 2])). (* true *)

发生这种情况是因为,为了获得相反的结果,我们需要右手边对所有y 都有效。正确的形式是:

forall xs ys,
  different xs ys = true <-> 
  (forall y, negb (member y xs) || negb (member x xs)).

尽管如此,您是对的,将某些结果指定为布尔方程会使它们在许多情况下使用起来更方便。这种风格被大量使用,例如,在Ssreflect 库中,他们在其中编写了如下定理:

eqn_leq : forall m n, (m == n) = (m <= n) && (n <= m)

这里,==&lt;= 运算符是布尔函数,用于测试自然数的相等性和顺序。第一个是通用的,适用于使用布尔相等函数声明的任何类型,在 Ssreflect 中称为 eqType

这是使用 Ssreflect 的定理版本:

Require Import Ssreflect.s-s-reflect Ssreflect.s-s-rfun Ssreflect.s-s-rbool.
Require Import Ssreflect.s-s-rnat Ssreflect.eqtype Ssreflect.seq.

Section Different.

Variable T : eqType.
Implicit Types xs ys : seq T.

Fixpoint disjoint xs ys :=
  match xs with
  | [::]     => true
  | x :: xs' => (x \notin ys) && disjoint xs' ys
  end.

Lemma disjointP xs ys :
  reflect (forall x, x \in xs -> x \notin ys)
          (disjoint xs ys).
Proof.
elim: xs=> [|x xs IH] /=; first exact: ReflectT.
apply/(iffP andP)=> [[x_nin /IH IH IH] x'|xsP].
  by rewrite inE=> /orP [/eqP ->|] //; auto.
apply/andP; rewrite xsP /= ?inE ?eqxx //.
apply/IH=> x' x'_in; apply: xsP.
by rewrite inE x'_in orbT.
Qed.

End Different.

我已将different 重命名为disjoint,并使用了Ssreflect 列表成员运算符\in\notin,可用于包含任何eqType 中的元素的列表。请注意disjointP 的语句有一个从boolProp 的隐式转换(将b 映射到b = true),并且它是用reflect 谓词声明的,您可以将其视为就像“当且仅当”连接词,但将Propbool 相关联。

Ssreflect 广泛使用reflect 谓词和view 机制(您在证明脚本上看到的/ 符号)在同一事实的布尔语句和命题语句之间进行转换。因此,虽然我们不能用简单的布尔相等来说明等价,但我们可以使用reflect 谓词来保持大部分便利。例如:

Goal forall n, n \in [:: 1; 2; 3] -> n \notin [:: 4; 5; 6].
Proof. by apply/disjointP. Qed.

这里发生的事情是 Coq 使用 disjointP 将上述目标转换为 disjoint [:: 1; 2; 3] [:: 4; 5; 6][:: ... ] 只是列表的 Ssreflect 表示法),并且可以通过计算发现该目标是正确的。

【讨论】:

谢谢!是的,我想要像 Ssreflect 之类的东西(我必须承认,我还不太了解),因为我希望能够使用计算来为我做证明。背景是这个定理(正确的形式,forall y 在正确的位置)是用 HOL 中的单行证明证明的。除了简单的重写之外,它几乎什么都不做。我认为这很简洁,并想在 Coq 中复制它。 (而且disjointall_different 是比different 更好的名称——但我只是从HOL 代码中复制了名称...)

以上是关于在 Coq 中证明一个定理几乎只用重写——没有“聪明”的主要内容,如果未能解决你的问题,请参考以下文章

如何证明排中在 Coq 中是无可辩驳的?

Z3和coq的区别

引入先前证明的定理作为假设

使用 Coq 证明存在量词

在 Coq 证明语言中,“没有更多的子目标,但存在未实例化的存在变量”?

具有存在目标的普遍假设中的 Coq 箭头类型