CODEWITHSUNDEEP
coqlambda-calculus
larsr
larsr

Reputation: 5811

Prove that a sequence of steps terminates

I have a small system that rewrites lambda terms. It has the usual (three) deterministic call-by-value rewrite rules. I have not listed them here.

The rewrites are modelled as Steps from one Term to another. I have also the StarStep relation between reachable terms, where the latter can be produced from the first by zero or more rewrite steps.

I now want to show that the rewrites terminate (either with a value, or stuck). I have stripped out the details, because I don't think they matter here, but I can add more details if needed.

Here is the code (or here in CollaCoq in the browser):

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

So I want to show

IF it is NOT the case that "from all reachable states it is possible another step" THEN there exists a state t' that is reachable from t such that it is not possible to take a step from it.

I am stuck on how to proceed. Do I need more info, i.e. induction or destructing (= case analysis of) t? And how can I use the info in the hypothesis when it is negated?

EDIT: Here are more details about Term and Step

Upvotes: 1

Views: 90

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

I believe this is an instance of classical reasoning. The statement resembles the following proposition, which is not provable in the constructive setting:

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

because the knowledge that "it is not true that forall ..." doesn't yield an object which you need to prove the existence of something.

Here is a possible solution using the laws of classical logic:

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.

Actually, we don't even need to know anything about StarStep, because the following abstract version of the previous proposition is valid in classical logic (the proof remains the same):

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

Upvotes: 4

Related Questions