TAPL: Normal form implies value

step.v

Inductive term : Set :=
| true : term
| false : term
| ifthenelse : term -> term -> term -> term.

Inductive step : term -> term -> Prop :=
  | iota1 : forall l r, step (ifthenelse true l r) l
  | iota2 : forall l r, step (ifthenelse false l r) r
  | econ1 : forall b c l r, step b c -> step (ifthenelse b l r) (ifthenelse c l r)
  | econ2 : forall b l m r, step l m -> step (ifthenelse b l r) (ifthenelse b m r)
  | econ3 : forall b l r s, step r s -> step (ifthenelse b l r) (ifthenelse b l s).

Definition normal_form (t:term) :=
  ~(exists t',  step t t').

Lemma normal_form_ifthenelse (b l r : term) :
  normal_form (ifthenelse b l r) ->
  normal_form b /\ normal_form l /\ normal_form r.
Proof.
   intros H        (* assumption normal_form (ifthenelse b l r) *)
 ; repeat split    (* split the big conjunction into 3 goals *)
 ; intros [t redt] (* introduce the "exists t',  step t t'" proofs
                      all the goals are now False *)
 ; apply H         (* because we know that "step t t'", we are going to
                      be able to prove that "step (ifthenelse ...) ..."
                      which H says is impossible *)
 ; eexists         (* we let Coq guess which term we are going to step to *)
 ; constructor     (* we pick the appropriate constructor between the econ[1..3] *)
 ; eapply redt.    (* finally we lookup the proof we were given earlier *)
Qed.

Inductive is_value : term -> Prop :=
| vtrue  : is_value true
| vfalse : is_value false.

Lemma normal_form_implies_value : forall t, normal_form t -> is_value t.
Proof.
intro t; induction t; intro ht.
  - constructor.
  - constructor.
  - destruct (normal_form_ifthenelse _ _ _ ht) as [ht1 _].
    apply False_ind, ht; destruct (IHt1 ht1); eexists; constructor.
Qed.