Coinductive Operational Semantics

Proof script adapts a small part of the development underlying:
Xavier Leroy and Herve Grall, Coinductive big-step operational semantics, Information and Computation 207(2):284-304, 2009. Extended version of the paper with the same title published in the proceedings of ESOP 2006.
Copyright 2005, 2006, 2007 Institut National de la Recherche en Informatique et Automatique.
Copyright 2012, Catalin Hritcu. Adapted a small part of the development for presentation in CIS670 at Penn. Changelist:
• added many examples and exercises
• aggressively automated the proofs using Adam's crush and my coind tactic (with help from Antal Spector-Zabusky)
Last updated on 2012-12-23

Require Import Classical. (* some of the proofs need classical axioms *)
Require Import CpdtTactics. (* crush tactic *)
Require Import CoindTactic. (* coind ... using ... tactic *)

Set Implicit Arguments.

Syntax

Call-by-value lambda calculus with nat constants -- the simplest language with stuck terms (e.g. 0 0)

Definition var := nat.

Lemma var_eq : forall (v1 v2: var), {v1=v2} + {v1<>v2}.
Proof. decide equality. Defined.

Inductive term : Set :=
| Var : var -> term
| Const : nat -> term
| Fun : var -> term -> term
| App : term -> term -> term.

We create a separate hint database since the hints in core are harder to apply. See Why does eauto treat "core" differently than the other hint databases? thread on coq-club mailing list (Oct 11, 2012) if interested in details: https://sympa.inria.fr/sympa/arc/coq-club/2012-10/msg00081.html

Create HintDb mydb.
Hint Constructors term : mydb.

Using the same trick as in the SF: this definition of substitution is capture-avoiding only when the substituted term is closed. Since we are in a call-by-value language and we only evaluate closed terms, the substituted terms will always be closed values.

Fixpoint subst (x : var) (b : term) (a : term) {struct a} : term :=
match a with
| Var y => if var_eq x y then b else Var y
| Const n => Const n
| Fun y a1 => Fun y (if var_eq x y then a1 else subst x b a1)
| App a1 a2 => App (subst x b a1) (subst x b a2)
end.

Inductive val : term -> Prop :=
| val_const : forall c, val (Const c)
| val_fun : forall x a, val (Fun x a).

Hint Constructors val : mydb.

Small-step semantics

The one-step reduction relation

Call-by-value left-to-right evaluation strategy

Inductive red1 : term -> term -> Prop :=
| red1_beta : forall x a v,
val v ->
red1 (App (Fun x a) v) (subst x v a)
| red1_app_l : forall a1 a2 b,
red1 a1 a2 ->
red1 (App a1 b) (App a2 b)
| red1_app_r : forall v b1 b2,
val v ->
red1 b1 b2 ->
red1 (App v b1) (App v b2).

Hint Constructors red1 : mydb.

(* The term tomega reduces to itself in one step *)
Definition vx: var := 0.
Definition tdelta := Fun vx (App (Var vx) (Var vx)).
Definition tomega := App tdelta tdelta.

Lemma red1_tomega : red1 tomega tomega.
Proof. constructor; constructor. Qed.

(* irreducible terms *)
Definition irred (a : term) : Prop := forall b, red1 a b -> False.

Lemma value_irred : forall a, val a -> irred a.
Proof. induction 1; intros b Hc; inversion Hc. Qed.

(* stuck terms = irreducible terms that are not values *)
Definition stuck (a : term) : Prop := irred a /\ ~val a.

(* an example stuck term *)
Definition tstuck := App (Const 0) (Const 0).

Lemma stuck_tstuck : stuck tstuck.
Proof.
split. intros b Hc; inversion Hc;
match goal with [ H : red1 (Const _) _ |- _] => inversion H end.
intro Hc; inversion Hc.
Qed.

(* reducing a value is a contradiction *)
Ltac red1_val_contra :=
try solve [match goal with
| [Hv : val ?v,
Hr : red1 ?v _ |- _] => destruct (value_irred Hv Hr)
| [Hr : red1 (Fun _ _) _ |- _] => inversion Hr
| [Hr : red1 (Const _) _ |- _] => inversion Hr
end].

(* determinism of one-step reduction *)
Lemma red1_deterministic:
forall a b, red1 a b -> forall c, red1 a c -> c = b.
Proof.
induction 1; inversion 1; crush; red1_val_contra;
(* apply the IH everywhere possible. *)
repeat match goal with
| [IH : forall c, red1 ?a c -> c = ?b,
Hr : red1 ?a ?d |- _] => apply IH in Hr
end; crush.
Qed.

Finite (multi-step) reductions

(* Reflexive-transitive closure of red1 *)
Inductive redfin : term -> term -> Prop :=
| redfin_refl : forall a,
redfin a a
| redfin_step : forall a b c,
red1 a b -> redfin b c -> redfin a c.

Hint Constructors redfin : mydb.

Lemma redfin_one : forall a b, red1 a b -> redfin a b.
Proof. eauto with mydb. Qed.

Lemma redfin_trans : forall a b c,
redfin a b -> redfin b c -> redfin a c.
Proof. induction 1; eauto with mydb. Qed.

Definition goes_wrong a := exists b, redfin a b /\ stuck b.

Definition twrong := App (Fun vx (App (Var vx) (Var vx))) (Const 0).

Lemma goes_wrong_twrong : goes_wrong twrong.
Proof. exists tstuck. eauto using stuck_tstuck with mydb. Qed.

Infinite reductions

CoInductive redinf: term -> Prop :=
| redinf_intro : forall a b,
red1 a b -> redinf b -> redinf a.

Hint Constructors redinf : mydb.

Section redinf_coind.
Variable R : term -> Prop.
Hypothesis H : forall a, R a -> exists b, red1 a b /\ R b.

Definition redinf_coind : forall t, R t -> redinf t.
cofix CIH. intros t Ht.
destruct (H Ht) as [b [Hab Hb]].
eapply redinf_intro. eassumption. apply CIH. eassumption.
Qed.
End redinf_coind.

(* We can very easily prove that omega loops *)

Lemma redinf_tomega : redinf tomega.
Proof. coind using redinf_coind; eauto using red1_tomega. Qed.

Exercise (easy):

Using redinf_tomega we can show that any term that reduces to omega is also non-terminating. For instance, prove that the term tloops below is non-terminating.
(Hint: the simplest solution fits on one line)

Definition tloops := App (Fun vx tomega) (Const 0).

Lemma redinf_tloops : redinf tloops.
Proof.
(* fill this in *)

If one steps through the redinf_tomega proof, though, there is something strange going on. It seems that we were very lucky that tomega immediately reduced to itself, but that won't be the case for many other non-terminating terms. Here is an example where that's not the case:

Definition vy : var := 1.
Definition tdelta' :=
Fun vx (App (Fun vy (App (Var vx) (Var vx))) (Const 0)).
Definition tomega1 := App tdelta' tdelta'.
Definition tomega2 := App (Fun vy (App tdelta' tdelta')) (Const 0).

Lemma red1_tomega1_tomega2 : red1 tomega1 tomega2.
Proof. repeat constructor. Qed.

Lemma red1_tomega2_tomega1 : red1 tomega2 tomega1.
Proof. repeat constructor. Qed.

Lemma redinf_tomega1 : redinf tomega1.
Proof.
coind using redinf_coind. exists tomega2. split.
apply red1_beta. constructor.

(* Left to show that tomega2 = tomega1, which is nonsense.
The syntactically chosen R (fun a => a = tomega1) is not good! *)

Abort.

In this case we need to manually choose a better R, one that contains both tomega1, and all terms that can be reached by taking reduction steps starting from tomega1. Since tomega1 only reduces to tomega2 and tomega2 only back to tomega1, in this case R needs to contain only 2 terms: tomega1 and tomega2.

Lemma redinf_tomega1 : redinf tomega1.
Proof.
apply redinf_coind with
(R := fun a => a = tomega1 \/ a = tomega2); crush;
eauto using red1_tomega1_tomega2, red1_tomega2_tomega1.
Qed.

Instead of phrasing this in terms of choosing a better R, we can also phrase it in terms of generalizing the co-induction hypothesis, and then letting coind choose the R automatically.

Lemma redinf_tomega1_stronger : forall a,
a = tomega1 \/ a = tomega2 ->
redinf a.
Proof.
coind using redinf_coind; crush;
eauto using red1_tomega1_tomega2, red1_tomega2_tomega1.
Qed.

While in this case it sufficed to add one additional term to R to have the co-inductive non-termination proof go through, things are more complicated in general. We can very easily construct terms that loop forever without ever repeating the same term again (e.g. something for the form f 1 -> f 2 -> ... -> f n -> ...). For instance here is a term that grows forever when reduced:

Definition vf : var := 2.

(* A bit of the Y combinator *)
Definition ypart := Fun vx (App (Var vf) (App (Var vx) (Var vx))).

(* Self-application function *)
Definition dup := Fun vx (App (Var vx) (Var vx)).

(* Y combinator instantiated to dup *)
Definition ydup := subst vf dup (App ypart ypart).

(* A term that grows forever when evaluated *)
Definition tgrows := App dup ydup.

We can show that
dup ydup -> dup (dup ydup) -> dup (dup (dup ydup)) -> ...

Lemma red1_tgrows :
red1 tgrows (App dup tgrows).
Proof. repeat constructor. Qed.

(* In order to show redinf tgrows we need to generalize the
co-induction hypothesis as follows: *)

Lemma redinf_tgrows_stronger : forall b, redfin tgrows b -> redinf b.
Proof.
coind using redinf_coind.
Abort.

However, before we can make further progress on this proof we need to directly characterize the shape of all the terms that can be reached by finitely reducing tgrows. We represent the infinite set {dup ydup, dup (dup ydup), dup (dup (dup ydup)), ... } with an inductive definition:

Inductive from_tgrows : term -> Prop :=
| ft_base : from_tgrows tgrows
| ft_step : forall a, from_tgrows a -> from_tgrows (App dup a).

Hint Constructors from_tgrows : mydb.

We relate from_tgrows and redfin tgrows in a series of lemmas. Since we do lots of inversions we define a specialized tactic for that:

Ltac invsc H := inversion H; subst; clear H.

Lemma from_tgrows_red1 : forall a b,
from_tgrows a ->
red1 a b ->
from_tgrows b.
Proof.
intros a b H; induction 1; invsc H;
repeat (compute in *;
(red1_val_contra ||
match goal with
| [Hv : val (App _ _) |- _] => solve [inversion Hv]
| [Hv : val ?v, Hft : from_tgrows ?v |- _] => invsc Hft
| [Hr : red1 (App _ _) _ |- _] => invsc Hr
end)); auto with mydb.
Qed.

Lemma from_tgrows_redfin : forall a b,
from_tgrows a ->
redfin a b ->
from_tgrows b.
Proof. induction 2; eauto using from_tgrows_red1. Qed.

Lemma from_tgrows_sound : forall a,
redfin tgrows a ->
from_tgrows a.
Proof. eauto using from_tgrows_redfin with mydb. Qed.

Lemma red1_App_dup : forall a,
from_tgrows a ->
red1 (App dup a) (App dup (App dup a)).
Proof.
induction 1; eauto using red1_tgrows with mydb.
Qed.

We didn't need this for the proof below, still, here it goes in case your proof needs it.
Lemma from_grows_complete : forall a,
from_tgrows a ->
redfin tgrows a.
Proof.
induction 1;
try match goal with [H : from_tgrows _ |- _] => invsc H end;
eauto using redfin_trans, redfin_one, red1_tgrows, red1_App_dup
with mydb.
Qed.

Exercise (medium):

Use the lemmas above to finish the following co-inductive proof.

Lemma redinf_tgrows_stronger : forall b, redfin tgrows b -> redinf b.
Proof.
coind using redinf_coind.
pose proof (from_tgrows_sound H) as H'.
(* finish this proof *)

Lemma redinf_tgrows : redinf tgrows.
Proof. eauto using redinf_tgrows_stronger with mydb. Qed.

You might have noticed that the proof of redinf tgrows was not as simple one might expect.

Coinductive reductions (finite and infinite)

We give a co-inductive interpretation of the rules for reflexive transitive closure. This captures both finite and infinite reductions.
CoInductive cored : term -> term -> Prop :=
| cored_refl : forall a,
cored a a
| cored_step : forall a b c,
red1 a b -> cored b c -> cored a c.

Hint Constructors cored : mydb.

Section cored_coind.
Variable R : term -> term -> Prop.
Hypothesis H : forall a b, R a b ->
a = b \/ exists a', red1 a a' /\ R a' b.

Definition cored_coind : forall a b, R a b -> cored a b.
cofix CIH. intros a b HR.
destruct (H HR) as [Hab | [a' [Haa' Ha'b]]].
subst. constructor.
eapply cored_step. eassumption. apply CIH; assumption.
Qed.
End cored_coind.

We prove that cored is the union of redfin and redinf

Lemma redfin_cored :
forall a b, redfin a b -> cored a b.
Proof. induction 1; eauto with mydb. Qed.

Lemma redinf_cored :
forall a b, redinf a -> cored a b.
Proof.
coind using cored_coind;
match goal with
| [H : redinf _ |- _] => destruct H; eauto
end.
Qed.

Lemma cored_irred_redinf :
forall a b, cored a b -> ~(redfin a b) -> redinf a.
Proof.
coind using redinf_coind;
match goal with
| [ H : cored ?a ?b, H0 : ~ redfin ?a ?b |- _] =>
destruct H; [apply False_ind; eauto with mydb
| eauto 10 with mydb]
end.
Qed.

Theorem cored_red_or_redinf:
forall a b, cored a b <-> redfin a b \/ redinf a.
Proof.
intros a b. split; intro H.
destruct (classic (redfin a b)); eauto using cored_irred_redinf.
destruct H; eauto using redfin_cored, redinf_cored.
Qed.

Big-step semantics

The terminating executions (standard)

Inductive eval : term -> term -> Prop :=
| eval_const : forall c,
eval (Const c) (Const c)
| eval_fun : forall x a,
eval (Fun x a) (Fun x a)
| eval_app : forall a b x c vb v,
eval a (Fun x c) ->
eval b vb ->
eval (subst x vb c) v ->
eval (App a b) v.

Hint Constructors eval : mydb.

Lemma eval_val :
forall a b, eval a b -> val b.
Proof. induction 1; eauto with mydb. Qed.

Lemma eval_deterministic :
forall a v, eval a v -> forall v', eval a v' -> v' = v.
Proof.
induction 1; inversion_clear 1; try reflexivity.
repeat match goal with
| [ IH : forall v', eval ?a v' -> v' = ?v
, Heval : eval ?a _
|- _ ] => apply IH in Heval
end; crush.
Qed.

Lemma not_eval_tomega :
forall v, ~(eval tomega v).
Proof.
assert (forall a v, eval a v -> a <> tomega) as H.
induction 1; unfold tomega; crush;
repeat match goal with
| [Heval : eval tdelta _ |- _] => invsc Heval
end; crush.
crush; eauto.
Qed.

This alone doesn't tell us whether tomega is stuck or diverging; in fact eval alone can't distinguish tstuck from tomega -- this is an important limitation of inductive big-step semantics.

Lemma not_eval_tstuck :
forall v, ~(eval tstuck v).
Proof.
inversion 1; subst;
match goal with
| [H : eval (Const _) (Fun _ _) |- _] => solve [inversion H]
end.
Qed.

The non-terminating executions

CoInductive evalinf: term -> Prop :=
| evalinf_app_l: forall a b,
evalinf a ->
evalinf (App a b)
| evalinf_app_r: forall a b va,
eval a va ->
evalinf b ->
evalinf (App a b)
| evalinf_app_f: forall a b x c vb,
eval a (Fun x c) ->
eval b vb ->
evalinf (subst x vb c) ->
evalinf (App a b).

Hint Constructors evalinf : mydb.

One important thing to note is that evalinf does not hold for stuck terms; i.e. this helps us distinguish between stuckness and divergence.

Lemma not_evalinf_tstuck : ~evalinf tstuck.
Proof.
inversion 1;
match goal with
| [H : evalinf (Const _) |- _] => solve [inversion H]
| [H : eval (Const _) _ |- _] => solve [inversion H]
end.
Qed.

If we use the technique we applied until now, the co-induction principle for evalinf is quite complicated. We need to use disjunction since all the 3 rules have the same conclusion.

Section evalinf_coind.
Variable R : term -> Prop.

Hypothesis H : forall a, R a ->
exists a', exists a'', a = (App a' a'') /\
(R a' \/ (exists va', eval a' va' /\ R a'')
\/ (exists x, exists c, eval a' (Fun x c)
/\ exists va'', eval a'' va''
/\ R (subst x va'' c))).

Definition evalinf_coind : forall t, R t -> evalinf t.
cofix CIH. intros t Ht.
destruct (H Ht) as
[? [? [? [? | [[? [? ?]] | [? [? [? [? [? ?]]]]]]]]]]; subst.
apply evalinf_app_l. apply CIH; assumption.
eapply evalinf_app_r. eassumption. apply CIH; assumption.
eapply evalinf_app_f. eassumption. eassumption.
apply CIH; assumption.
Qed.
End evalinf_coind.

Here is an alternative way of writing this co-induction principle: we first define a "generator function" for evalinf; i.e. evalinf_gen is a non-recursive variant of evalinf abstracted over itself.

Inductive evalinf_gen R : term -> Prop :=
| evalinf_gen_app_l: forall a b,
R a ->
evalinf_gen R (App a b)
| evalinf_gen_app_r: forall a b va,
eval a va ->
R b ->
evalinf_gen R (App a b)
| evalinf_gen_app_f: forall a b x c vb,
eval a (Fun x c) ->
eval b vb ->
R (subst x vb c) ->
evalinf_gen R (App a b).

Hint Constructors evalinf_gen : mydb.

Using evalinf_gen we can define a simpler co-inductive principle:

Section evalinf_coind'.
Variable R : term -> Prop.

Hypothesis H : forall a, R a -> evalinf_gen R a.

Definition evalinf_coind' : forall a, R a -> evalinf a.
cofix CIH. intros a Ha.
pose proof (H Ha) as Heg.
invsc Heg.
(* the rest of the proof is exactly as before *)
apply evalinf_app_l. apply CIH; assumption.
eapply evalinf_app_r. eassumption. apply CIH; assumption.
eapply evalinf_app_f. eassumption. eassumption.
apply CIH; assumption.
Qed.
End evalinf_coind'.

Exercise (medium):

Prove that this alternative way to state the co-inductive principle is in fact equivalent with the original one.

Section evalinf_coind_equiv.
Variable R : term -> Prop.
Variable a : term.
Hypothesis H : R a.

Lemma evalinf_coind_equiv :
evalinf_gen R a <->
(exists a', exists a'', a = (App a' a'') /\
(R a' \/ (exists va', eval a' va' /\ R a'')
\/ (exists x, exists c, eval a' (Fun x c)
/\ exists va'', eval a'' va''
/\ R (subst x va'' c)))).
Proof.
(* fill this in *)
End evalinf_coind_equiv.

Exercise (medium, optional):

One can take this idea one step further and define evalinf using evalinf_gen. While this might seem a bit odd, it has the advantage of removing the duplication between evalinf and evalinf_gen. (As e.g. done in Paco: http://plv.mpi-sws.org/paco/tutorial.html )

CoInductive evalinf' : term -> Prop :=
| evalinf_fold : forall a, evalinf_gen evalinf' a -> evalinf' a.

Hint Constructors evalinf' : mydb.

Show that evalinf and evalinf' are equivalent

Lemma evalinf_equiv_evalinf' : forall a, evalinf' a <-> evalinf a.
Proof.
(* fill in here *)

(* Now let's prove that tomega is non-terminating using
evalinf. We do it with each of the induction principles. *)

Lemma evalinf_tomega : evalinf tomega.
Proof.
coind using evalinf_coind; unfold tomega, tdelta; eauto 11 with mydb.
Qed.

Lemma evalinf_tomega' : evalinf tomega.
Proof.
coind using evalinf_coind'; unfold tomega; eauto with mydb.
Qed.

Exercise (easy):

Show that tloops is in evalinf.
(Hint: the simplest solution fits on one line)

Lemma evalinf_tloops : evalinf tloops.
Proof.
(* fill in here *)

Exercise (medium):

Show that tomega1 is in evalinf.
(Hint: if you find yourself stuck have a look at redinf_tomega1)

Lemma evalinf_tomega1 : evalinf tomega1.
Proof.
(* fill in here *)

Exercise (medium):

Show that tgrows is in evalinf.
(Hint: although this might seem surprising given redinf_tgrows, the correct R here has cardinality 2!)

Lemma evalinf_tgrows : evalinf tloops.
Proof.
(* fill in here *)

Relating the big-step and small-step semantics

The finite part (standard, easy)

Lemma redfin_app_l :
forall a1 a2 b, redfin a1 a2 -> redfin (App a1 b) (App a2 b).
Proof. induction 1; eauto with mydb. Qed.

Lemma redfin_app_r : forall v a1 a2,
val v -> redfin a1 a2 -> redfin (App v a1) (App v a2).
Proof. induction 2; eauto with mydb. Qed.

Theorem eval_redfin:
forall a v, eval a v -> redfin a v.
Proof.
induction 1; trivial with mydb.
match goal with
[Ha : redfin ?a ?va, Hb : redfin ?b ?vb |- redfin (App ?a ?b) _] =>
eapply redfin_trans;
[exact (redfin_app_l _ Ha) |
eapply redfin_trans;
[solve [apply redfin_app_r; eauto with mydb] |
solve [eauto using eval_val with mydb]]]
end.
Qed.

Lemma val_eval :
forall v, val v -> eval v v.
Proof. induction 1; auto with mydb. Qed.

Lemma red1_eval :
forall a b, red1 a b -> forall v, eval b v -> eval a v.
Proof.
induction 1; intros;
eauto using val_eval with mydb;
match goal with [H : eval _ _ |- _] => inversion H; eauto with mydb end.
Qed.

Theorem redfin_eval:
forall a v, redfin a v -> val v -> eval a v.
Proof. induction 1; eauto using val_eval, red1_eval. Qed.

The infinite part (more interesting)

We show that evalinf and redinf are equivalent; first the -> direction.

Lemma infinite_progress_redinf: forall a,
(forall b, redfin a b -> exists c, red1 b c) ->
redinf a.
Proof.
coind using redinf_coind;
match goal with
| [a : term |- _] =>
assert (exists b, red1 a b) as [b J] by auto with mydb;
eauto 10 with mydb
end.
Qed.

Lemma redfin_or_redinf: forall a,
(exists b, redfin a b /\ irred b) \/ redinf a.
Proof.
intro a. destruct (classic (redinf a)); [solve [tauto] | left].
assert (H' : ~forall b, redfin a b -> exists c, red1 b c)
by eauto using infinite_progress_redinf.
destruct (not_all_ex_not _ _ H') as [b H''].
destruct (imply_to_and _ _ H'').
unfold irred; eauto.
Qed.

Lemma evalinf_red1:
forall a, evalinf a -> exists b, red1 a b /\ evalinf b.
Proof.
induction a; inversion 1;
repeat match goal with
| [H : eval _ _ |- _] => generalize (eval_redfin H); inversion 1;
generalize dependent H (* prevents looping *)
end;
crush; eauto 7 using redfin_eval, eval_val with mydb.
Qed.

Theorem evalinf_redinf:
forall a, evalinf a -> redinf a.
Proof.
coind using redinf_coind; eauto using evalinf_red1.
Qed.

As a corrolary we can prove that stuck terms don't loop forever.

Lemma not_evalinf_stuck : forall a, stuck a -> ~evalinf a.
Proof.
intros a [Hi Hnv] He; generalize (evalinf_redinf He); inversion 1; eauto.
Qed.

Second, we show that redinf implies evalinf

Lemma redinf_app_l:
forall a a', redfin a a' ->
forall b, redinf (App a b) -> redinf (App a' b).
Proof.
induction 1; [solve[auto]|].
intros b' Hb'; invsc Hb'. apply IHredfin.
match goal with
| [H : red1 ?a ?b, H' : red1 (App ?a ?b') ?b0 |- redinf (App ?b ?b') ] =>
replace (App b b') with b0; eauto using red1_deterministic with mydb
end.
Qed.

Lemma redinf_app_r:
forall b b', redfin b b' ->
forall a, val a -> redinf (App a b) -> redinf (App a b').
Proof.
induction 1; [solve[auto]|].
intros b' Hv Hb'; invsc Hb'. apply IHredfin; [assumption|].
match goal with
| [H : red1 ?a ?b, H' : red1 (App ?b' ?a) ?b0 |- redinf (App ?b' ?b) ] =>
replace (App b' b) with b0; eauto using red1_deterministic with mydb
end.
Qed.

A couple of tactics by Antal Spector-Zabusky
Solve a goal where we know both that a term is irreducible but also that it can reduce in one step to something.
match goal with
[Hirr : irred ?x, Hr1 : red1 ?x _ |- _] => solve [destruct (Hirr _ Hr1)]
end.

Invert both a `redinf` term and the initial `red1` it contains.
Ltac invert_redinf_red1 H :=
let H' := fresh "H" in inversion H as [? ? H' ?]; inversion H'.

A terms either reduces finitely or infinitely. This tactic quickly discharges the case where the given term `a` reduces infinitely, and shows that if a term reduces finitely, then (a) the (irreducible) term `x` that `a` finally reduces to is a value, and (b) `app x` reduces infinitely.
Ltac when_finite_is_val a app :=
destruct (redfin_or_redinf a); crush;
eauto using redfin_eval with mydb;
match goal with
[Hfin : redfin a ?x |- _ ] =>
let Hinf' := fresh "Hinf"
in assert (redinf (app x)) as Hinf'
by eauto using redinf_app_l, redinf_app_r with mydb;
assert (val x)
by (invert_redinf_red1 Hinf'; subst; auto with mydb;
end;
simpl in *.

Theorem redinf_evalinf:
forall a, redinf a -> evalinf a.
Proof.
intros a H; coind using evalinf_coind'.
(* Only applications can reduce infinitely *)
destruct a; try solve [invert_redinf_red1 H].
(* We can easily discharge the cases where one of the terms in the
application reduces infinitely; the case where both reduce
finitely but their *application* reduces infinitely is more
interesting. *)

match goal with
| [_ : redinf (App a1 a2) |- _] =>
when_finite_is_val a1 (fun x => App x a2);
match goal with
[_ : val ?x |- _] => when_finite_is_val a2 (fun y => App x y)
end
end.
(* Since applying a value to a value reduces infinitely, we know that the
former value is a function.  This allows us to discharge our final proof
obligations. *)

match goal with
[Hinf : redinf (App ?x ?y), _ : val ?x, _ : val ?y |- _] =>
invert_redinf_red1 Hinf; subst
end;
first [irred_contradict | eauto using redfin_eval with mydb].
Qed.