coq - 如何证明偏序归纳谓词的可判定性？

Question

语境

我试图用leCoq 中的关系定义偏序 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.

标签： coqproofdeterministicformal-verificationpartial-ordering

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.