Démontrer qu'une séquence d'étapes se termine

Question

J'ai un petit système qui réécrit les termes lambda. Il a les règles de réécriture appel-par-valeur (trois) déterministes habituelles. Je ne les ai pas énumérés ici.

Les réécritures sont modélisées comme Step s d'un Term à un autre. J'ai aussi la relation StarStep entre joignable termes, où ce dernier peut être produit à partir de la première par zéro ou plusieurs étapes de réécriture.

Je veux maintenant montrer que les réécritures se terminent (soit avec une valeur, soit collées). J'ai enlevé les détails, parce que je ne pense pas qu'ils importent ici, mais je peux ajouter plus de détails si nécessaire.

Voici le code (ou here dans CollaCoq dans le navigateur):

Variable Term: Type. 
Variable Step: Term -> Term -> Prop. 
Inductive StarStep: Term -> Term -> Prop := 
| StepNone : forall t, StarStep t t 
| StepOne : forall t t', Step t t' -> forall t'', StarStep t' t'' -> StarStep t t''. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''. 

Je veux montrer

S'il est pas le cas que « de tous accessibles états il est possible une autre étape " ALORS il existe un état t' qui est accessible à partir de t tel qu'il n'est pas possible d'en faire un pas.

Je suis bloqué sur la façon de procéder. Ai-je besoin de plus d'informations, c'est-à-dire d'induction ou de destruction (= analyse de cas) t? Et comment puis-je utiliser l'info dans l'hypothèse quand elle est annulée?

EDIT: Here are more details about Term and Step

Answer 1

Je crois que c'est une instance de raisonnement classique . La déclaration ressemble à la proposition suivante, ce qui est démontrable dans le cadre constructif:

Goal forall (A : Type) (P : A -> Prop), 
    ~ (forall x, P x) -> exists x, ~ P x. 

parce que la connaissance que « il est vrai que forall ... » ne donne pas un objet que vous devez prouver l'existence de quelque chose.

Voici une solution possible en utilisant les lois de la logique classique:

Require Import Coq.Logic.Classical_Pred_Type. 
Require Import Coq.Logic.Classical_Prop. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''. 
Proof. 
    intros t H. 
    apply not_all_ex_not in H. 
    destruct H as [tt H]. 
    apply imply_to_and in H. 
    firstorder. 
Qed. 

En fait, nous ne même pas besoin de savoir quoi que ce soit au sujet StarStep, parce que la version abstraite suivante de la proposition précédente est valable dans le classique la logique (la preuve reste la même):

Goal forall (A : Type) (P Q : A -> Prop), 
    ~ (forall s, Q s -> exists t, P t) -> 
    exists s, Q s /\ forall t, ~ P t.