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

Question

我试图提出一个问题，以便仅重写就足以证明目标。我想避免使用“聪明”的命题，而是使用可以由Coq计算的布尔值。

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

我想证明我different只能使用重写为表达式member。

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.

编辑2：

我将在@Arthur给出我为什么在初次尝试中失败时给出正确答案的结束语，但是为了完整起见，我想按照我的目标添加解决方案。

我写了一份Ltac战术my_simple_rewrite，该战术可以执行多种操作try rewrite with lemma_x in *（大约20种不同的引理，这些引理只能从左到右重写）。他们对简单的引理boolS和mem1，mem2，diff1，和diff2从上面。为了证明该定理，我仅使用了归纳变量xs和要对哪些bool表达式进行案例分析（使用自制Ltac bool_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

Answer 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)

在这里，==和<=运算符是booelan函数，用于测试自然数是否相等和有序。第一个是通用的，适用于使用布尔相等函数声明的任何类型，该函数eqType在Ssreflect中称为。

这是使用Ssreflect的定理的一个版本：

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat 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具有从bool到的隐式转换Prop（映射b到b = true），并用reflect谓词声明，您可以将其视为类似于“ if and only if”的连接词，但将a Prop与a 关联bool。

Ssreflect广泛使用reflect谓词和视图机制（在/证明脚本上看到的符号）在同一事实的布尔语句和命题语句之间进行转换。因此，尽管我们不能用简单的布尔等式声明等价性，但是我们可以在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表示法），并且仅通过计算就可以发现该目标是正确的。