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.