From d76d81f16ceb21f4e8c8b5b309ba2a5fff01902d Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sat, 4 Nov 2023 13:16:53 +0100 Subject: [PATCH] Clean up exercises01 a bit, add them to _CoqProject --- _CoqProject | 2 +- theories/type_systems/stlc/exercises01.v | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/_CoqProject b/_CoqProject index c052616..f23016d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -19,5 +19,5 @@ theories/type_systems/stlc/notation.v # By removing the # below, you can add the exercise sheets to make theories/type_systems/warmup/warmup.v #theories/type_systems/warmup/warmup_sol.v -#theories/type_systems/stlc/exercises01.v +theories/type_systems/stlc/exercises01.v #theories/type_systems/stlc/exercises01_sol.v diff --git a/theories/type_systems/stlc/exercises01.v b/theories/type_systems/stlc/exercises01.v index eef06d7..d657af5 100644 --- a/theories/type_systems/stlc/exercises01.v +++ b/theories/type_systems/stlc/exercises01.v @@ -68,13 +68,15 @@ Proof. | e_l e_l' e_r H_val H_l_step IH | e_l e_r e_r' H_r_step IH ]; subst. - all: intros e' H_step'; inversion H_step'; subst; try val_no_step. - - reflexivity. - - by rewrite (IH e1'). - - by rewrite (IH e2'). - - reflexivity. - - by rewrite (IH e1'). - - by rewrite (IH e2'). + all: intros e' H_step'; inversion H_step' as [ + | + _tmp e_ind | + _tmp1 _tmp2 e_ind | + | + _tmp e_ind | + _tmp1 _tmp2 e_ind + ]; subst; intuition try val_no_step. + all: by rewrite (IH e_ind). Qed. (** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)