如何证明交换参数的关系的可判定性?
How to prove decidability of a relation swaping its parameters?
我有一种情况,我定义了一个归纳数据类型 t
和一个偏序 le
(c.f. le_refl
, le_trans
,和 le_antisym
)。该顺序在 le_C
情况下具有这种特殊性,即参数的顺序在归纳假设中被交换。
因此,我没有成功证明这个顺序关系是确定性的(c.f。le_dec
)。有问题的子目标如下。
1 subgoal
t1 : t
IHt1 : forall t2 : t, {le t1 t2} + {~ le t1 t2}
t2 : t
______________________________________(1/1)
{le (C t1) (C t2)} + {~ le (C t1) (C t2)}
归纳假设是指le t1 t2
而我需要le t2 t1
.
当我想到这一点时,它是有道理的,这个二元函数既不是对第一个参数也不是第二个参数进行原始递归,而是对两个参数对进行递归。我的印象是我应该以某种方式同时对两个参数进行归纳,但看不出如何去做。
我确实设法定义了一个布尔函数 leb
并用它来证明 le_dec
,但我想知道,从学习的角度来看,如何直接用归纳法进行证明.
问题
- 如何根据
le
的定义直接证明le_dec
(即不先定义等价的布尔函数)?
最小可执行示例
主要定义
Inductive t : Set :=
| A : t
| B : t -> t
| C : t -> t
.
Inductive le : t -> t -> Prop :=
| le_A :
le A A
| le_B : forall x y,
le x y -> le (B x) (B y)
| le_C : forall x y,
le y x -> le (C x) (C y)
| le_trans : forall t1 t2 t3,
le t1 t2 -> le t2 t3 -> le t1 t3
.
辅助引理
Require Import Coq.Program.Equality.
Lemma le_canonical_form_A_left (t1 : t) :
le A t1 -> t1 = A.
Proof.
intros LE. dependent induction LE; auto.
Qed.
Lemma le_canonical_form_B_left (t1 t2 : t) :
le (B t1) t2 -> exists t3, t2 = B t3.
Proof.
intros LE. dependent induction LE.
- eauto.
- destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.
Lemma le_canonical_form_C_left (t1 t2 : t) :
le (C t1) t2 -> exists t3, t2 = C t3.
Proof.
intros LE. dependent induction LE.
- eauto.
- destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.
Lemma le_inversion_B (t1 t2 : t) :
le (B t1) (B t2) -> le t1 t2.
Proof.
intros LE.
dependent induction LE.
- assumption.
- apply le_canonical_form_B_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.
Lemma le_inversion_C (t1 t2 : t) :
le (C t1) (C t2) -> le t2 t1.
Proof.
intros LE.
dependent induction LE.
- assumption.
- apply le_canonical_form_C_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.
Lemma le_inversion (t1 t2 : t) :
le t1 t2 ->
t1 = A /\ t2 = A \/
(exists t1' t2', t1 = B t1' /\ t2 = B t2') \/
(exists t1' t2', t1 = C t1' /\ t2 = C t2').
Proof.
intros LE.
destruct t1.
- apply le_canonical_form_A_left in LE; subst. auto.
- apply le_canonical_form_B_left in LE as [? ?]; subst. eauto 6.
- apply le_canonical_form_C_left in LE as [? ?]; subst. eauto 6.
Qed.
偏序证明
Lemma le_refl (x : t) :
le x x.
Proof.
induction x; eauto using le.
Qed.
Lemma le_antisym (t1 t2 : t) :
le t1 t2 -> le t2 t1 -> t1 = t2.
Proof.
induction 1; intros LE.
- auto.
- apply le_inversion_B in LE. f_equal; auto.
- apply le_inversion_C in LE. f_equal; auto using eq_sym.
- rewrite IHle1; eauto using le_trans.
Qed.
等价的布尔函数
Fixpoint height (x : t) : nat :=
match x with
| A => 1
| B x' => 1 + height x'
| C x' => 1 + height x'
end.
Definition height_pair (p : t * t) : nat :=
let (t1, t2) := p in height t1 + height t2.
Require Import Recdef.
Require Import Omega.
Function leb (p : t * t) { measure height_pair p } : bool :=
match p with
| (A, A) => true
| (B x', B y') => leb (x', y')
| (C x', C y') => leb (y', x')
| _ => false
end.
- intros. subst. simpl. omega.
- intros. subst. simpl. omega.
Defined.
Ltac inv H := inversion H; clear H; subst.
Lemma le_to_leb (t1 t2 : t) :
le t1 t2 -> leb (t1, t2) = true.
Proof.
remember (t1, t2) as p eqn:Heqn.
revert Heqn.
revert t1 t2.
functional induction (leb p); intros t1 t2 Heqn LE; inv Heqn.
- trivial.
- apply IHb with x' y'; trivial.
now apply le_inversion_B in LE.
- apply IHb with y' x'; trivial.
now apply le_inversion_C in LE.
- exfalso. apply le_inversion in LE.
intuition; subst.
+ easy.
+ destruct H0.
destruct H.
now (intuition; subst).
+ destruct H0.
destruct H.
now (intuition; subst).
Qed.
Lemma leb_to_le (t1 t2 : t) :
leb (t1, t2) = true -> le t1 t2.
Proof.
remember (t1, t2) as p eqn:Heqn.
revert Heqn.
revert t1 t2.
functional induction (leb p); intros t1 t2 Heqn LEB; inv Heqn.
- eauto using le.
- eauto using le.
- eauto using le.
- discriminate LEB.
Qed.
Corollary le_iff_leb (t1 t2 : t) :
le t1 t2 <-> leb (t1, t2) = true.
Proof.
split.
- apply le_to_leb.
- apply leb_to_le.
Qed.
我其实想证明什么
Lemma le_dec (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
revert t2.
induction t1; intros t2.
- destruct t2.
+ eauto using le.
+ right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
- destruct t2.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
+ destruct IHt1 with t2.
* eauto using le.
* right. intro contra. apply le_inversion_B in contra. contradiction.
+ right; intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
- destruct t2.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
+ destruct IHt1 with t2.
* admit. (* Wrong assumption *)
* admit. (* Wrong assumption *)
Restart.
destruct (leb (t1, t2)) eqn:Heqn.
- apply leb_to_le in Heqn. auto.
- right. intro contra. apply le_to_leb in contra.
rewrite Heqn in contra. discriminate.
Qed.
解决方案基于
Ltac destruct_exs_conjs :=
repeat match goal with
| H : exists _, _ |- _ => destruct H
| H : _ /\ _ |- _ => destruct H
end; subst.
Lemma le_dec_aux (t1 t2 : t) (n : nat) :
height t1 + height t2 <= n ->
{le t1 t2} + {~le t1 t2}.
Proof.
revert t1 t2.
induction n as [| n IH]; intros t1 t2 H.
- destruct t1; simpl in H; omega.
- destruct t1, t2.
+ eauto using le.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
+ simpl in H.
destruct (IH t1 t2); try omega.
* eauto using le.
* right. intro contra. apply le_inversion_B in contra. contradiction.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
+ simpl in H.
destruct (IH t2 t1); try omega.
* eauto using le.
* right. intro contra. apply le_inversion_C in contra. contradiction.
Qed.
Lemma le_dec' (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
destruct (le_dec_aux t1 t2 (height t1 + height t2)); auto.
Qed.
类似于你定义leb
函数的方法,你需要通过对元素高度的归纳来证明le_dec
:
Lemma le_dec_aux t1 t2 n : height t1 + height t2 <= n -> {le t1 t2} + {~le t1 t2}.
Proof.
revert t1 t2.
induction n as [|n IH].
(* ... *)
话虽如此,我认为使用布尔函数来证明可判定性是完全可以的。 Mathematical Components 库广泛使用此模式,使用专门的 reflect
谓词将一般命题连接到布尔计算,而不是 sumbool
类型 {A} + {B}
。
我尝试了@Arthur 建议的版本,使用有根据的递归。
这确实提供了一个很好的提取。
Definition rel p1 p2 := height_pair p1 < height_pair p2.
Lemma rel_wf : well_founded rel.
Proof.
apply well_founded_ltof.
Qed.
Lemma le_dec (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
induction t1, t2 as [t1 t2]
using (fun P => well_founded_induction_type_2 P rel_wf).
destruct t1, t2;
try (right; intros contra;
(apply le_canonical_form_A_left in contra)
|| (apply le_canonical_form_B_left in contra; destruct contra)
|| (apply le_canonical_form_C_left in contra; destruct contra);
discriminate).
- left. apply le_A.
- destruct (H t1 t2).
+ unfold rel, height_pair; simpl. omega.
+ left. apply le_B. assumption.
+ right. intros contra. apply le_inversion_B in contra. contradiction.
- destruct (H t2 t1).
+ unfold rel, height_pair; simpl. omega.
+ left. apply le_C. assumption.
+ right. intros contra. apply le_inversion_C in contra. contradiction.
Qed.
Extraction Inline well_founded_induction_type_2 Fix_F_2.
(* to have a nice extraction *)
Extraction le_dec.
但是请注意,您定义的顺序关系实际上只是相等关系,但也许您描述了对初始用例的简化。
Lemma le_is_eq : forall t1 t2, le t1 t2 -> t1 = t2.
Proof.
intros.
induction t1, t2 as [t1 t2]
using (fun P => well_founded_induction_type_2 P rel_wf).
destruct t1, t2;
try ((apply le_canonical_form_A_left in H)
|| (apply le_canonical_form_B_left in H; destruct H)
|| (apply le_canonical_form_C_left in H; destruct H);
discriminate).
- reflexivity.
- apply le_inversion_B in H.
apply H0 in H.
+ congruence.
+ unfold rel, height_pair. simpl. omega.
- apply le_inversion_C in H.
apply H0 in H.
+ congruence.
+ unfold rel, height_pair. simpl. omega.
Qed.
我有一种情况,我定义了一个归纳数据类型 t
和一个偏序 le
(c.f. le_refl
, le_trans
,和 le_antisym
)。该顺序在 le_C
情况下具有这种特殊性,即参数的顺序在归纳假设中被交换。
因此,我没有成功证明这个顺序关系是确定性的(c.f。le_dec
)。有问题的子目标如下。
1 subgoal
t1 : t
IHt1 : forall t2 : t, {le t1 t2} + {~ le t1 t2}
t2 : t
______________________________________(1/1)
{le (C t1) (C t2)} + {~ le (C t1) (C t2)}
归纳假设是指le t1 t2
而我需要le t2 t1
.
当我想到这一点时,它是有道理的,这个二元函数既不是对第一个参数也不是第二个参数进行原始递归,而是对两个参数对进行递归。我的印象是我应该以某种方式同时对两个参数进行归纳,但看不出如何去做。
我确实设法定义了一个布尔函数 leb
并用它来证明 le_dec
,但我想知道,从学习的角度来看,如何直接用归纳法进行证明.
问题
- 如何根据
le
的定义直接证明le_dec
(即不先定义等价的布尔函数)?
最小可执行示例
主要定义
Inductive t : Set :=
| A : t
| B : t -> t
| C : t -> t
.
Inductive le : t -> t -> Prop :=
| le_A :
le A A
| le_B : forall x y,
le x y -> le (B x) (B y)
| le_C : forall x y,
le y x -> le (C x) (C y)
| le_trans : forall t1 t2 t3,
le t1 t2 -> le t2 t3 -> le t1 t3
.
辅助引理
Require Import Coq.Program.Equality.
Lemma le_canonical_form_A_left (t1 : t) :
le A t1 -> t1 = A.
Proof.
intros LE. dependent induction LE; auto.
Qed.
Lemma le_canonical_form_B_left (t1 t2 : t) :
le (B t1) t2 -> exists t3, t2 = B t3.
Proof.
intros LE. dependent induction LE.
- eauto.
- destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.
Lemma le_canonical_form_C_left (t1 t2 : t) :
le (C t1) t2 -> exists t3, t2 = C t3.
Proof.
intros LE. dependent induction LE.
- eauto.
- destruct IHLE1 with t1 as [t4 ?]; clear IHLE1; trivial; subst.
destruct IHLE2 with t4 as [t4' ?]; clear IHLE2; trivial; subst. eauto.
Qed.
Lemma le_inversion_B (t1 t2 : t) :
le (B t1) (B t2) -> le t1 t2.
Proof.
intros LE.
dependent induction LE.
- assumption.
- apply le_canonical_form_B_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.
Lemma le_inversion_C (t1 t2 : t) :
le (C t1) (C t2) -> le t2 t1.
Proof.
intros LE.
dependent induction LE.
- assumption.
- apply le_canonical_form_C_left in LE1 as [t3 ?]; subst. eauto using le_trans.
Qed.
Lemma le_inversion (t1 t2 : t) :
le t1 t2 ->
t1 = A /\ t2 = A \/
(exists t1' t2', t1 = B t1' /\ t2 = B t2') \/
(exists t1' t2', t1 = C t1' /\ t2 = C t2').
Proof.
intros LE.
destruct t1.
- apply le_canonical_form_A_left in LE; subst. auto.
- apply le_canonical_form_B_left in LE as [? ?]; subst. eauto 6.
- apply le_canonical_form_C_left in LE as [? ?]; subst. eauto 6.
Qed.
偏序证明
Lemma le_refl (x : t) :
le x x.
Proof.
induction x; eauto using le.
Qed.
Lemma le_antisym (t1 t2 : t) :
le t1 t2 -> le t2 t1 -> t1 = t2.
Proof.
induction 1; intros LE.
- auto.
- apply le_inversion_B in LE. f_equal; auto.
- apply le_inversion_C in LE. f_equal; auto using eq_sym.
- rewrite IHle1; eauto using le_trans.
Qed.
等价的布尔函数
Fixpoint height (x : t) : nat :=
match x with
| A => 1
| B x' => 1 + height x'
| C x' => 1 + height x'
end.
Definition height_pair (p : t * t) : nat :=
let (t1, t2) := p in height t1 + height t2.
Require Import Recdef.
Require Import Omega.
Function leb (p : t * t) { measure height_pair p } : bool :=
match p with
| (A, A) => true
| (B x', B y') => leb (x', y')
| (C x', C y') => leb (y', x')
| _ => false
end.
- intros. subst. simpl. omega.
- intros. subst. simpl. omega.
Defined.
Ltac inv H := inversion H; clear H; subst.
Lemma le_to_leb (t1 t2 : t) :
le t1 t2 -> leb (t1, t2) = true.
Proof.
remember (t1, t2) as p eqn:Heqn.
revert Heqn.
revert t1 t2.
functional induction (leb p); intros t1 t2 Heqn LE; inv Heqn.
- trivial.
- apply IHb with x' y'; trivial.
now apply le_inversion_B in LE.
- apply IHb with y' x'; trivial.
now apply le_inversion_C in LE.
- exfalso. apply le_inversion in LE.
intuition; subst.
+ easy.
+ destruct H0.
destruct H.
now (intuition; subst).
+ destruct H0.
destruct H.
now (intuition; subst).
Qed.
Lemma leb_to_le (t1 t2 : t) :
leb (t1, t2) = true -> le t1 t2.
Proof.
remember (t1, t2) as p eqn:Heqn.
revert Heqn.
revert t1 t2.
functional induction (leb p); intros t1 t2 Heqn LEB; inv Heqn.
- eauto using le.
- eauto using le.
- eauto using le.
- discriminate LEB.
Qed.
Corollary le_iff_leb (t1 t2 : t) :
le t1 t2 <-> leb (t1, t2) = true.
Proof.
split.
- apply le_to_leb.
- apply leb_to_le.
Qed.
我其实想证明什么
Lemma le_dec (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
revert t2.
induction t1; intros t2.
- destruct t2.
+ eauto using le.
+ right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
- destruct t2.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
+ destruct IHt1 with t2.
* eauto using le.
* right. intro contra. apply le_inversion_B in contra. contradiction.
+ right; intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_B_left in contra1 as [? ?]; subst. eauto.
- destruct t2.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
+ right. intro contra. clear IHt1. dependent induction contra.
apply le_canonical_form_C_left in contra1 as [? ?]; subst. eauto.
+ destruct IHt1 with t2.
* admit. (* Wrong assumption *)
* admit. (* Wrong assumption *)
Restart.
destruct (leb (t1, t2)) eqn:Heqn.
- apply leb_to_le in Heqn. auto.
- right. intro contra. apply le_to_leb in contra.
rewrite Heqn in contra. discriminate.
Qed.
解决方案基于
Ltac destruct_exs_conjs :=
repeat match goal with
| H : exists _, _ |- _ => destruct H
| H : _ /\ _ |- _ => destruct H
end; subst.
Lemma le_dec_aux (t1 t2 : t) (n : nat) :
height t1 + height t2 <= n ->
{le t1 t2} + {~le t1 t2}.
Proof.
revert t1 t2.
induction n as [| n IH]; intros t1 t2 H.
- destruct t1; simpl in H; omega.
- destruct t1, t2.
+ eauto using le.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_A_left in contra1; subst. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
+ simpl in H.
destruct (IH t1 t2); try omega.
* eauto using le.
* right. intro contra. apply le_inversion_B in contra. contradiction.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_B_left in contra1; destruct_exs_conjs. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
+ clear. right. intro contra. dependent induction contra.
apply le_canonical_form_C_left in contra1; destruct_exs_conjs. eauto.
+ simpl in H.
destruct (IH t2 t1); try omega.
* eauto using le.
* right. intro contra. apply le_inversion_C in contra. contradiction.
Qed.
Lemma le_dec' (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
destruct (le_dec_aux t1 t2 (height t1 + height t2)); auto.
Qed.
类似于你定义leb
函数的方法,你需要通过对元素高度的归纳来证明le_dec
:
Lemma le_dec_aux t1 t2 n : height t1 + height t2 <= n -> {le t1 t2} + {~le t1 t2}.
Proof.
revert t1 t2.
induction n as [|n IH].
(* ... *)
话虽如此,我认为使用布尔函数来证明可判定性是完全可以的。 Mathematical Components 库广泛使用此模式,使用专门的 reflect
谓词将一般命题连接到布尔计算,而不是 sumbool
类型 {A} + {B}
。
我尝试了@Arthur 建议的版本,使用有根据的递归。 这确实提供了一个很好的提取。
Definition rel p1 p2 := height_pair p1 < height_pair p2.
Lemma rel_wf : well_founded rel.
Proof.
apply well_founded_ltof.
Qed.
Lemma le_dec (t1 t2 : t) :
{ le t1 t2 } + { ~le t1 t2 }.
Proof.
induction t1, t2 as [t1 t2]
using (fun P => well_founded_induction_type_2 P rel_wf).
destruct t1, t2;
try (right; intros contra;
(apply le_canonical_form_A_left in contra)
|| (apply le_canonical_form_B_left in contra; destruct contra)
|| (apply le_canonical_form_C_left in contra; destruct contra);
discriminate).
- left. apply le_A.
- destruct (H t1 t2).
+ unfold rel, height_pair; simpl. omega.
+ left. apply le_B. assumption.
+ right. intros contra. apply le_inversion_B in contra. contradiction.
- destruct (H t2 t1).
+ unfold rel, height_pair; simpl. omega.
+ left. apply le_C. assumption.
+ right. intros contra. apply le_inversion_C in contra. contradiction.
Qed.
Extraction Inline well_founded_induction_type_2 Fix_F_2.
(* to have a nice extraction *)
Extraction le_dec.
但是请注意,您定义的顺序关系实际上只是相等关系,但也许您描述了对初始用例的简化。
Lemma le_is_eq : forall t1 t2, le t1 t2 -> t1 = t2.
Proof.
intros.
induction t1, t2 as [t1 t2]
using (fun P => well_founded_induction_type_2 P rel_wf).
destruct t1, t2;
try ((apply le_canonical_form_A_left in H)
|| (apply le_canonical_form_B_left in H; destruct H)
|| (apply le_canonical_form_C_left in H; destruct H);
discriminate).
- reflexivity.
- apply le_inversion_B in H.
apply H0 in H.
+ congruence.
+ unfold rel, height_pair. simpl. omega.
- apply le_inversion_C in H.
apply H0 in H.
+ congruence.
+ unfold rel, height_pair. simpl. omega.
Qed.