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

Using Coq
1

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.

2

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