Terminaison implique l'existence de la forme normale

Question

Je voudrais prouver que la résiliation implique l'existence de la forme normale. Ce sont mes définitions:

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. 

Je voudrais prouver:

Lemma terminating_impl_normalizing (T : terminating): 
    normalizing. 

Je suis frappais ma tête contre le mur pendant quelques heures maintenant, et je l'ai fait presque aucun progrès . Je peux montrer:

Lemma terminating_not_inf_forall (T : terminating) : 
    forall f : nat -> A, ~ (forall n, R (f n) (f (S n))). 

qui je crois devrait aider (ceci est également vrai sans classique).

Answer 1

Voici une preuve utilisant le milieu exclu. J'ai reformulé le problème pour remplacer les définitions personnalisées par des définitions standard (notez d'ailleurs que dans votre définition de la fermeture, le rtc_into est redondant avec les autres). J'ai également reformulé terminating en utilisant 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. 

La preuve est pas très compliqué, mais voici les principales idées:

• utilisation induction fondée
• grâce au principe du tiers exclu, séparer le cas où x n'est pas en forme normale et le cas où il est
• si x n'est pas dans la forme normale, utiliser l'hypothèse de récurrence et utiliser la transitivité de la fermeture pour conclure
• si x est déjà dans la forme normale, nous avons terminé