Докажите, что последовательность шагов завершается

Question

У меня есть небольшая система, которая переписывает лямбда-термины. Он имеет обычные (три) детерминированные правила переписывания по значению. Я не перечислил их здесь.

Перезаписи моделируются как Step s от одного Term к другому. У меня также есть отношение StarStep между достижимыми терминами, где последний может быть произведен с первого на ноль или более шагов перезаписи.

Теперь я хочу показать, что перезаписывание завершается (либо со значением, либо застревает). Я убрал детали, потому что я не думаю, что они имеют значение здесь, но я могу добавить больше деталей, если это необходимо.

Вот код (или here в CollaCoq в браузере):

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

Так что я хочу, чтобы показать

, если это не так, что «от всех достижимы состояний можно еще один шаг " THEN существует состояние t', которое доступно от t таким образом, чтобы оно невозможно сделать шаг от него.

Я застрял на том, как действовать. Нужна ли мне дополнительная информация, то есть индукция или деструкция (= анализ случая) t? И как я могу использовать информацию в гипотезе, когда она отрицается?

EDIT: Here are more details about Term and Step

Answer 1

Я считаю, что это пример классического рассуждения. утверждения напоминает следующее предложение, которое не доказуемо в конструктивной настройке:

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

, поскольку известно, что «это не правда, что FORALL ...» не дает объект, который вы должны доказать существование чего-то.

Вот возможное решение с использованием законов классической логики:

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. 

На самом деле, мы даже не нужно ничего знать о StarStep, потому что следующий абстрактный вариант предыдущего предложения действительны в классическом логика (доказательство остается прежняя):

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