终止意味着存在正常形式
Termination implies existence of normal form
我想证明终止意味着存在范式。这些是我的定义:
Section Forms.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Context {A : Type}
Variable R : A -> A -> Prop.
Definition Inverse (Rel : A -> A -> Prop) := fun x y => Rel y x.
Inductive ReflexiveTransitiveClosure : Relation A A :=
| rtc_into (x y : A) : R x y -> ReflexiveTransitiveClosure x y
| rtc_trans (x y z : A) : R x y -> ReflexiveTransitiveClosure y z ->
ReflexiveTransitiveClosure x z
| rtc_refl (x y : A) : x = y -> ReflexiveTransitiveClosure x y.
Definition redc (x : A) := exists y, R x y.
Definition nf (x : A) := ~(redc x).
Definition nfo (x y : A) := ReflexiveTransitiveClosure R x y /\ nf y.
Definition terminating := forall x, Acc (Inverse R) x.
Definition normalizing := forall x, (exists y, nfo x y).
End Forms.
我想证明:
Lemma terminating_impl_normalizing (T : terminating):
normalizing.
我已经用头撞墙几个小时了,几乎没有任何进展。我可以显示:
Lemma terminating_not_inf_forall (T : terminating) :
forall f : nat -> A, ~ (forall n, R (f n) (f (S n))).
我认为这应该有所帮助(没有经典也是如此)。
这是一个使用排中的证明。我重新表述了问题,以用标准定义替换自定义定义(顺便注意,在闭包的定义中,rtc_into
与其他定义是多余的)。我还使用 well_founded
.
重新表述了 terminating
Require Import Classical_Prop.
Require Import Relations.
Section Forms.
Context {A : Type} (R:relation A).
Definition inverse := fun x y => R y x.
Definition redc (x : A) := exists y, R x y.
Definition nf (x : A) := ~(redc x).
Definition nfo (x y : A) := clos_refl_trans _ R x y /\ nf y.
Definition terminating := well_founded inverse. (* forall x, Acc inverse x. *)
Definition normalizing := forall x, (exists y, nfo x y).
Lemma terminating_impl_normalizing (T : terminating):
normalizing.
Proof.
unfold normalizing.
apply (well_founded_ind T). intros.
destruct (classic (redc x)).
- destruct H0 as [y H0]. pose proof (H _ H0).
destruct H1 as [y' H1]. exists y'. unfold nfo.
destruct H1.
split.
+ apply rt_trans with (y:=y). apply rt_step. assumption. assumption.
+ assumption.
- exists x. unfold nfo. split. apply rt_refl. assumption.
Qed.
End Forms.
证明不是很复杂,但主要思想如下:
- 使用有根据的归纳法
- 由于排中原则,将
x
不属于范式的情况与 不属于范式的情况分开
- 如果
x
不是范式,使用归纳假设并使用闭包的传递性来得出结论
- 如果
x
已经是正常形式,我们就完成了
我想证明终止意味着存在范式。这些是我的定义:
Section Forms.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Context {A : Type}
Variable R : A -> A -> Prop.
Definition Inverse (Rel : A -> A -> Prop) := fun x y => Rel y x.
Inductive ReflexiveTransitiveClosure : Relation A A :=
| rtc_into (x y : A) : R x y -> ReflexiveTransitiveClosure x y
| rtc_trans (x y z : A) : R x y -> ReflexiveTransitiveClosure y z ->
ReflexiveTransitiveClosure x z
| rtc_refl (x y : A) : x = y -> ReflexiveTransitiveClosure x y.
Definition redc (x : A) := exists y, R x y.
Definition nf (x : A) := ~(redc x).
Definition nfo (x y : A) := ReflexiveTransitiveClosure R x y /\ nf y.
Definition terminating := forall x, Acc (Inverse R) x.
Definition normalizing := forall x, (exists y, nfo x y).
End Forms.
我想证明:
Lemma terminating_impl_normalizing (T : terminating):
normalizing.
我已经用头撞墙几个小时了,几乎没有任何进展。我可以显示:
Lemma terminating_not_inf_forall (T : terminating) :
forall f : nat -> A, ~ (forall n, R (f n) (f (S n))).
我认为这应该有所帮助(没有经典也是如此)。
这是一个使用排中的证明。我重新表述了问题,以用标准定义替换自定义定义(顺便注意,在闭包的定义中,rtc_into
与其他定义是多余的)。我还使用 well_founded
.
terminating
Require Import Classical_Prop.
Require Import Relations.
Section Forms.
Context {A : Type} (R:relation A).
Definition inverse := fun x y => R y x.
Definition redc (x : A) := exists y, R x y.
Definition nf (x : A) := ~(redc x).
Definition nfo (x y : A) := clos_refl_trans _ R x y /\ nf y.
Definition terminating := well_founded inverse. (* forall x, Acc inverse x. *)
Definition normalizing := forall x, (exists y, nfo x y).
Lemma terminating_impl_normalizing (T : terminating):
normalizing.
Proof.
unfold normalizing.
apply (well_founded_ind T). intros.
destruct (classic (redc x)).
- destruct H0 as [y H0]. pose proof (H _ H0).
destruct H1 as [y' H1]. exists y'. unfold nfo.
destruct H1.
split.
+ apply rt_trans with (y:=y). apply rt_step. assumption. assumption.
+ assumption.
- exists x. unfold nfo. split. apply rt_refl. assumption.
Qed.
End Forms.
证明不是很复杂,但主要思想如下:
- 使用有根据的归纳法
- 由于排中原则,将
x
不属于范式的情况与 不属于范式的情况分开
- 如果
x
不是范式,使用归纳假设并使用闭包的传递性来得出结论 - 如果
x
已经是正常形式,我们就完成了