# Proof request: use of Forall to enumerate and uniformly prove test cases correct

I am formalizing the untyped lambda calculus, and as part of sanity-checking my work as I go I have a number of test cases I like to work with.

``````Goal beta_reduces_to (id \$ id) id.
Proof.
constructor.
Qed.

Goal beta_reduces_to infinite_loop infinite_loop.
Proof.
constructor.
Qed.

Goal beta_reduces_to fork_bomb (fork_bomb \$ fork_bomb).
Proof.
constructor.
Qed.
``````

It occured to me that I could fold these together using `Forall` from the standard library:

``````Goal Forall (fun (t: prod Term Term) => beta_reduces_to (fst t) (snd t)) [
((id \$ id), id);
(infinite_loop, infinite_loop);
(fork_bomb, (fork_bomb \$ fork_bomb))
].
Proof.
apply Forall_forall.
intros.
repeat (induction H; [subst; simpl; constructor | idtac]).
inversion H.
Qed.
``````

Is this the â€śmorally correctâ€ť approach to this? I would have preferred to use reflection to do the iteration within Gallina instead of using `repeat` but Iâ€™m not sure there is a quick and easy way to do that.

There is at least no need to go through `Forall_forall`. You could directly try:

``````Goal Forall (fun '(t1,t2) => beta_reduces_to t1 t2) [
((id \$ id), id);
(infinite_loop, infinite_loop);
(fork_bomb, (fork_bomb \$ fork_bomb))
].
Proof.
repeat constructor.
[...]
Qed.
``````

Only test cases not solved by `constructor` will remain.

2 Likes