Терминация подразумевает существование нормальной формы

Question

Я хотел бы доказать, что окончание подразумевает существование нормальной формы. Это мои определения:

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))). 

, который, я считаю, должен помочь (это также верно без классики).

Answer 1

Это доказательство использования исключенного среднего. Я переформулировал проблему, чтобы заменить пользовательские определения стандартными (обратите внимание, что в вашем определении закрытия rtc_into избыточен с другими). Я также переформулировал terminating, используя well_founded.

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 уже в нормальной форме, мы делаем