如何证明偏序归纳谓词的可判定性？
How to prove decidability of a partial order inductive predicate?
上下文
我试图用 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
问题
- 如何证明
le C A 是错误前提？
- 我应该使用其他证明策略吗？
- 我应该以不同的方式定义谓词
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.
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 proof language 使这种风格的工作变得容易。例如，这是您第一次证明尝试的另一个版本。 （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 的解决方案。但让我演示另一种方法。
首先，我们需要一些支持引理：
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)) *)
请注意，您可以使用 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.
上下文
我试图用 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
问题
- 如何证明
le C A是错误前提？ - 我应该使用其他证明策略吗？
- 我应该以不同的方式定义谓词
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.
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 proof language 使这种风格的工作变得容易。例如，这是您第一次证明尝试的另一个版本。 （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 的解决方案。但让我演示另一种方法。
首先，我们需要一些支持引理：
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)) *)
请注意，您可以使用 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.