如何证明偏序归纳谓词的可决定性？

Question

背景

我正在尝试使用Coq中的关系le定义偏序A≤B≤C，并证明它是可判定的：forall x y，{le x y} + {~ le x y}。

我成功地通过一个等价的布尔函数leb来实现了这一点，但无法找到直接证明它（或者le_antisym）的方法。我在以下情况下遇到困难：

1 subgoal
H : le C A
______________________________________(1/1)
False

问题

1. 如何证明 le C A 是错误的前提?
2. 是否有其他的证明策略我应该使用?
3. 我应该怎样定义我的谓词 le ?

最小可执行示例

Require Import Setoid.

Ltac inv H := inversion H; clear H; subst.

Inductive t : Set := A | B | C.

Ltac destruct_ts :=
  repeat match goal with
  | [ x : t |- _ ] => destruct x
  end.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Definition leb (x y : t) : bool :=
  match x, y with
  | A, _ => true
  | _, C => true
  | B, B => true
  | _, _ => false
  end.

Theorem le_iff_leb : forall x y,
  le x y <-> leb x y = true.
Proof.
  intros x y. split; intro H.
  - induction H; destruct_ts; simpl in *; congruence.
  - destruct_ts; eauto using le; simpl in *; congruence.
Qed.

Theorem le_antisym : forall x y,
  le x y -> le y x -> x = y.
Proof.
  intros x y H1 H2.
  rewrite le_iff_leb in *. (* How to prove that without using [leb]? *)
  destruct x, y; simpl in *; congruence.
Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
  intros x y.
  destruct x, y; eauto using le.
  - apply right.
    intros H. (* Stuck here *)
    inv H.
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
  - apply right.
    intros H; inv H. (* Same thing *)
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
  - apply right.
    intros H; inv H. (* Same thing *)
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
Qed.

- authchir

---

为什么称之为部分排序？这里有三个元素 A | B | C，它们是完全有序的。 - Tej Chajed

这是我能想到的最简单的例子，但我正在处理的关系不是全序关系，因此我不希望有人根据全序关系得出答案。 - authchir

Answer 1

le存在的问题在于它的传递构造方法。在对le x y的证明进行倒置或归纳时，我们并不了解传递性情况下中间点的具体情况，这往往导致证明失败。你可以使用另一种（但仍是归纳的）关系特征来证明结果：

Require Import Setoid.

Ltac inv H := inversion H; clear H; subst.

Inductive t : Set := A | B | C.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Inductive le' : t -> t -> Prop :=
  | le'_refl : forall x, le' x x
  | le'_A_B  : le' A B
  | le'_B_C  : le' B C
  | le'_A_C  : le' A C.

Lemma le_le' x y : le x y <-> le' x y.
Proof.
  split.
  - intros H.
    induction H as [x|x y z xy IHxy yz IHyz| | ]; try now constructor.
    inv IHxy; inv IHyz; constructor.
  - intros H; inv H; eauto using le.
Qed.

Theorem le_antisym : forall x y,
  le x y -> le y x -> x = y.
Proof.
  intros x y.
  rewrite 2!le_le'.
  intros []; trivial; intros H; inv H.
Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
  intros x y.
  destruct x, y; eauto using le; right; rewrite le_le';
  intros H; inv H.
Qed.

在这种情况下，我认为使用归纳特征的 le 不是一个好主意，因为布尔版本更有用。当然，有时您可能希望有两个关系的特征：例如，有时您可能需要对类型进行相等的布尔测试，但想使用 = 进行重写。 ssreflect证明语言 可以轻松地在这种风格中工作。例如，以下是您第一次尝试证明的另一个版本。（reflect P b 谓词意味着命题 P 等价于断言 b = true。）

From mathcomp Require Import ssreflect ssrfun ssrbool.

Inductive t : Set := A | B | C.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Definition leb (x y : t) : bool :=
  match x, y with
  | A, _ => true
  | _, C => true
  | B, B => true
  | _, _ => false
  end.

Theorem leP x y : reflect (le x y) (leb x y).
Proof.
apply/(iffP idP); first by case: x; case y=> //=; eauto using le.
by elim=> [[]| | |] //= [] [] [].
Qed.

Theorem le_antisym x y : le x y -> le y x -> x = y.
Proof. by case: x; case: y; move=> /leP ? /leP ?. Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
Proof. by move=> x y; case: (leP x y); eauto. Qed.

- Arthur Azevedo De Amorim

---

抢先一步，使用完全相同的“了”。 - Tej Chajed

@Yves 刚刚在这里和那里完成了它。 - Arthur Azevedo De Amorim

那么 le' 基本上是枚举了 leb 中模式匹配处理的情况？这样会导致在元素数量 n 的情况下，出现 O(n) 种情况吗？我希望通过摆脱 leb 来避免这种情况... - authchir

@authchir 是的，这就是它所做的。我认为你无法避免这种增长；如果你要泛化le，你仍然需要至少一次提到每个构造函数。 - Arthur Azevedo De Amorim

Answer 2

我建议采用Arthur的解决方案。但是我想演示另一种方法。

首先，我们需要几个支持引理：

Lemma not_leXA x : x <> A -> ~ le x A.
Proof. remember A; intros; induction 1; subst; firstorder congruence. Qed.

Lemma not_leCX x : x <> C -> ~ le C x.
Proof. remember C; intros; induction 1; subst; firstorder congruence. Qed.

现在我们可以定义le_dec:

Definition le_dec x y : { le x y } + { ~le x y }.
Proof.
  destruct x, y; try (left; abstract constructor).
  - left; abstract (eapply le_trans; constructor).
  - right; abstract now apply not_leXA.
  - right; abstract now apply not_leCX.
  - right; abstract now apply not_leCX.
Defined.

请注意，我使用了Defined而不是Qed--现在您可以使用le_dec进行计算，这通常是使用sumbool类型的关键所在。

我还使用abstract来隐藏评估器中的证明项。例如，假设我定义了一个le_dec'函数，它与le_dec相同，但删除了所有abstract，那么在尝试计算le_dec B A/le_dec' B A时，我们将得到以下结果：

Compute le_dec B A.
(* ==> right le_dec_subproof5 *) 

并且

Compute le_dec' B A.
(* ==> right
     (not_leXA B
        (fun x : B = A =>
         match x in (_ = x0) return (x0 = A -> False) with
         | eq_refl =>
             fun x0 : B = A =>
             match
               match
                 x0 in (_ = x1)
                 return match x1 with
                        | B => True
                        | _ => False
                        end
               with
               | eq_refl => I
               end return False
             with
             end
         end eq_refl)) *)

- Anton Trunov

Answer 3

请注意，您可以利用Relations中的定义来定义您的顺序关系。例如，它包含了一个名为clos_refl_trans的自反和传递闭包的定义。由此得出的证明与基于您的定义的证明类似（参见@Anton的答案）。

Require Import Relations.

Inductive t : Set := A | B | C.

Inductive le : t -> t -> Prop :=
  | le_A_B : le A B
  | le_B_C : le B C.

Definition le' := clos_refl_trans _ le.

Lemma A_minimal : forall x, x <> A -> ~ le' x A.
Proof.
  intros. intros contra. remember A as a. induction contra; subst.
  - inversion H0.
  - contradiction.
  - destruct y; apply IHcontra2 + apply IHcontra1; congruence.
Qed.

Lemma C_maximal : forall x, x <> C -> ~ le' C x.
Proof.
  intros. intros contra. remember C as c. induction contra; subst.
  - inversion H0.
  - contradiction.
  - destruct y; apply IHcontra2 + apply IHcontra1; congruence.
Qed.

Lemma le'_antisym : forall x y,
  le' x y -> le' y x -> x = y.
Proof.
  intros. induction H.
  - destruct H.
    + apply A_minimal in H0; try discriminate. contradiction.
    + apply C_maximal in H0; try discriminate. contradiction.
  - reflexivity.
  - fold le' in *. rewrite IHclos_refl_trans1 by (eapply rt_trans; eassumption).
    apply IHclos_refl_trans2; (eapply rt_trans; eassumption).
Qed.

- eponier