add(tests): bounded conformance suite for the reducer against the relational semantics (golden corpus)

theory/Tests.v

@@ -0,0 +1,77 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction Metatheory.
+
+Definition t_id : trm := App (Lam (BVar 0)) (FVar 1).
+Definition t_dup : trm := App (Lam (App (BVar 0) (BVar 0))) (FVar 1).
+Definition t_dup_es : trm := ESub (App (BVar 0) (BVar 0)) (FVar 1).
+Definition t_gc : trm := ESub (FVar 2) (FVar 1).
+Definition t_nested : trm := ESub (ESub (BVar 0) (FVar 1)) (FVar 2).
+Definition t_capture : trm := App (Lam (Lam (BVar 1))) (FVar 1).
+Definition t_under : trm := ESub (Lam (BVar 1)) (FVar 2).
+
+Definition corpus : list trm :=
+  [t_id; t_dup; t_dup_es; t_gc; t_nested; t_capture; t_under].
+
+Example g_id_beta : has_rule RB (steps t_id) = true.
+Proof. reflexivity. Qed.
+
+Example g_dup_beta : has_rule RB (steps t_dup) = true.
+Proof. reflexivity. Qed.
+
+Example g_dup_es_two_R : count_rule RR (steps t_dup_es) = 2.
+Proof. reflexivity. Qed.
+
+Example g_dup_es_no_Gc : has_rule RGc (steps t_dup_es) = false.
+Proof. reflexivity. Qed.
+
+Example g_gc_gc : has_rule RGc (steps t_gc) = true.
+Proof. reflexivity. Qed.
+
+Example g_gc_no_R : has_rule RR (steps t_gc) = false.
+Proof. reflexivity. Qed.
+
+Example g_nested_gc : has_rule RGc (steps t_nested) = true.
+Proof. reflexivity. Qed.
+
+Example g_under_R : has_rule RR (steps t_under) = true.
+Proof. reflexivity. Qed.
+
+Example g_capture_beta : has_rule RB (steps t_capture) = true.
+Proof. reflexivity. Qed.
+
+Example g_normal_var : normal_form (FVar 5) = true.
+Proof. reflexivity. Qed.
+
+Example g_normal_lam : normal_form (Lam (BVar 0)) = true.
+Proof. reflexivity. Qed.
+
+Example g_capture_avoid_lam : subst 0 (FVar 1) (Lam (Lam (BVar 1))) = Lam (Lam (BVar 1)).
+Proof. reflexivity. Qed.
+
+Example g_capture_avoid_es : subst 0 (FVar 1) (ESub (FVar 0) (FVar 2)) = ESub (FVar 1) (FVar 2).
+Proof. reflexivity. Qed.
+
+Example g_occurs0_lam : occurs0 (Lam (BVar 0)) = false.
+Proof. reflexivity. Qed.
+
+Example g_occurs0_bvar : occurs0 (BVar 0) = true.
+Proof. reflexivity. Qed.
+
+Lemma corpus_sound : forall t p, In t corpus -> In p (steps t) -> red1r (fst p) t (snd p).
+Proof. intros t [r s] _ H. simpl. apply steps_sound. exact H. Qed.
+
+Lemma corpus_complete : forall t r t', In t corpus -> red1r r t t' -> In (r,t') (steps t).
+Proof. intros t r t' _ H. apply steps_complete. exact H. Qed.
+
+Lemma corpus_decides : forall t t', In t corpus -> has_red t t' = true <-> red1 t t'.
+Proof. intros t t' _. apply has_red_spec. Qed.
+
+Lemma corpus_fv_preserved : forall t p, In t corpus -> In p (steps t) ->
+  incl (fvs (snd p)) (fvs t).
+Proof. intros t [r s] _ H. simpl. apply (lemma_2_1_fv_preserved t s). exact (steps_sound_red1 t r s H). Qed.
+
+Print Assumptions corpus_sound.
+Print Assumptions corpus_complete.
+Print Assumptions corpus_decides.
+Print Assumptions corpus_fv_preserved.