Abstract things correctly out

theories/Core/Semantic/EvaluateLemmas.v

@@ -1,62 +1,67 @@
 From Coq Require Import Lia PeanoNat Relations.
 From Mcltt Require Import Base Domain Evaluate LibTactics Syntax System.
 
-#[local]
-Definition functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.
-#[local]
-Definition functional_eval_natrec_prop A MZ MS m p r1 (_ : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}) : Prop := forall r2 (Heval2 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r2 }}), r1 = r2.
-#[local]
-Definition functional_eval_app_prop m n r1 (_ : {{ $| m & n |↘ r1 }}) : Prop := forall r2 (Heval2 : {{ $| m & n |↘ r2 }}), r1 = r2.
-#[local]
-Definition functional_eval_sub_prop σ p p1 (_ : {{ ⟦ σ ⟧s p ↘ p1 }}) : Prop := forall p2 (Heval2 : {{ ⟦ σ ⟧s p ↘ p2 }}), p1 = p2.
-Arguments functional_eval_exp_prop /.
-Arguments functional_eval_natrec_prop /.
-Arguments functional_eval_app_prop /.
-Arguments functional_eval_sub_prop /.
+Section functional_eval.
+  Let functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.
+  Let functional_eval_natrec_prop A MZ MS m p r1 (_ : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}) : Prop := forall r2 (Heval2 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r2 }}), r1 = r2.
+  Let functional_eval_app_prop m n r1 (_ : {{ $| m & n |↘ r1 }}) : Prop := forall r2 (Heval2 : {{ $| m & n |↘ r2 }}), r1 = r2.
+  Let functional_eval_sub_prop σ p p1 (_ : {{ ⟦ σ ⟧s p ↘ p1 }}) : Prop := forall p2 (Heval2 : {{ ⟦ σ ⟧s p ↘ p2 }}), p1 = p2.
 
-Lemma functional_eval_exp : forall {M p m1}, {{ ⟦ M ⟧ p ↘ m1 }} -> forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2
-with functional_eval_natrec : forall {A MZ MS m p r1}, {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }} -> forall r2 (Heval2 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r2 }}), r1 = r2
-with functional_eval_app : forall {m n r1}, {{ $| m & n |↘ r1 }} -> forall r2 (Heval2 : {{ $| m & n |↘ r2 }}), r1 = r2
-with functional_eval_sub : forall {σ p p1}, {{ ⟦ σ ⟧s p ↘ p1 }} -> forall p2 (Heval2 : {{ ⟦ σ ⟧s p ↘ p2 }}), p1 = p2.
-Proof with mauto.
-  all: clear functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub; intros * Heval1.
-  - (* functional_eval_exp *)
+  #[local]
+  Ltac unfold_functional_eval := unfold functional_eval_exp_prop, functional_eval_natrec_prop, functional_eval_app_prop, functional_eval_sub_prop in *.
+
+  Lemma functional_eval_exp : forall M p m1 (Heval1 : {{ ⟦ M ⟧ p ↘ m1 }}), functional_eval_exp_prop M p m1 Heval1.
+  Proof using.
+    intros *.
     induction Heval1
       using eval_exp_mut_ind
       with (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      simpl in *; mauto;
+      unfold_functional_eval; mauto;
       intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
       solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1_1, IHHeval1_2 in *; mauto].
-  - (* functional_eval_natrec *)
+  Qed.
+
+  Lemma functional_eval_natrec : forall A MZ MS m p r1 (Heval1 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}), functional_eval_natrec_prop A MZ MS m p r1 Heval1.
+  Proof using.
+    intros *.
     induction Heval1
       using eval_natrec_mut_ind
       with (P := functional_eval_exp_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      simpl in *; mauto;
+      unfold_functional_eval; mauto;
       intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
       solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto].
-  - (* functional_eval_app *)
+  Qed.
+
+  Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
+  Proof using.
+    intros *.
     induction Heval1
       using eval_app_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P2 := functional_eval_sub_prop);
-      simpl in *; mauto;
+      unfold_functional_eval; mauto;
       intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
       solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto].
-  - (* functional_eval_sub *)
+  Qed.
+
+  Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
+  Proof using.
+    intros *.
     induction Heval1
       using eval_sub_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop);
-      simpl in *; mauto;
+      unfold_functional_eval; mauto;
       intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
       try solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto|erewrite IHHeval1_1 in *; mauto].
-Qed.
+  Qed.
+End functional_eval.
 
 #[export]
 Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.

theories/Core/Semantic/ReadbackLemmas.v

@@ -1,61 +1,65 @@
 From Coq Require Import Lia PeanoNat Relations.
 From Mcltt Require Import Base Domain Evaluate EvaluateLemmas LibTactics Readback Syntax System.
 
-#[local]
-Definition functional_read_nf_prop s m M1 (_ : {{ Rnf m in s ↘ M1 }}) : Prop := forall M2 (Hread2: {{ Rnf m in s ↘ M2 }}), M1 = M2.
-#[local]
-Definition functional_read_ne_prop s m M1 (_ : {{ Rne m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rne m in s ↘ M2 }}), M1 = M2.
-#[local]
-Definition functional_read_typ_prop s m M1 (_ : {{ Rtyp m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rtyp m in s ↘ M2 }}), M1 = M2.
-Arguments functional_read_nf_prop /.
-Arguments functional_read_ne_prop /.
-Arguments functional_read_typ_prop /.
+Section functional_read.
+  Let functional_read_nf_prop s m M1 (_ : {{ Rnf m in s ↘ M1 }}) : Prop := forall M2 (Hread2: {{ Rnf m in s ↘ M2 }}), M1 = M2.
+  Let functional_read_ne_prop s m M1 (_ : {{ Rne m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rne m in s ↘ M2 }}), M1 = M2.
+  Let functional_read_typ_prop s m M1 (_ : {{ Rtyp m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rtyp m in s ↘ M2 }}), M1 = M2.
 
-Lemma functional_read_nf : forall {s m M1}, {{ Rnf m in s ↘ M1 }} -> forall M2 (Hread2: {{ Rnf m in s ↘ M2 }}), M1 = M2
-with functional_read_ne : forall {s m M1}, {{ Rne m in s ↘ M1 }} -> forall M2 (Hread2 : {{ Rne m in s ↘ M2 }}), M1 = M2
-with functional_read_typ : forall {s m M1}, {{ Rtyp m in s ↘ M1 }} -> forall M2 (Hread2 : {{ Rtyp m in s ↘ M2 }}), M1 = M2.
-Proof with mauto.
-  all: clear functional_read_nf functional_read_ne functional_read_typ; intros * Hread1.
-  - (* functional_read_nf *)
+  #[local]
+  Ltac unfold_functional_read := unfold functional_read_nf_prop, functional_read_ne_prop, functional_read_typ_prop in *.
+
+  Lemma functional_read_nf : forall s m M1 (Hread1: {{ Rnf m in s ↘ M1 }}), functional_read_nf_prop s m M1 Hread1.
+  Proof using Type with mauto .
+    intros *.
     induction Hread1
       using read_nf_mut_ind
       with (P0 := functional_read_ne_prop)
            (P1 := functional_read_typ_prop);
-      simpl in *; mauto;
+      unfold_functional_read; mauto;
       intros; inversion Hread2; clear Hread2; subst;
       try replace m'0 with m' in * by mauto;
       try replace b0 with b in * by mauto;
       try replace bz0 with bz in * by mauto;
       try replace bs0 with bs in * by mauto;
       try replace ms0 with ms in * by mauto;
       f_equal...
-  - (* functional_read_ne *)
+  Qed.
+
+  Lemma functional_read_ne : forall s m M1 (Hread1 : {{ Rne m in s ↘ M1 }}), functional_read_ne_prop s m M1 Hread1.
+  Proof using Type with mauto.
+    intros *.
     induction Hread1
       using read_ne_mut_ind
       with (P := functional_read_nf_prop)
            (P1 := functional_read_typ_prop);
-      simpl in *; mauto;
+      unfold_functional_read; mauto;
       intros; inversion Hread2; clear Hread2; subst;
       try replace m'0 with m' in * by mauto;
       try replace b0 with b in * by mauto;
       try replace bz0 with bz in * by mauto;
       try replace bs0 with bs in * by mauto;
       try replace ms0 with ms in * by mauto;
       f_equal...
-  - (* functional_read_typ *)
+  Qed.
+
+  Lemma functional_read_typ : forall s m M1 (Hread1 : {{ Rtyp m in s ↘ M1 }}), functional_read_typ_prop s m M1 Hread1.
+  Proof using Type with mauto.
+    intros *.
     induction Hread1
       using read_typ_mut_ind
       with (P := functional_read_nf_prop)
            (P0 := functional_read_ne_prop);
-      simpl in *; mauto;
+      unfold_functional_read; mauto;
       intros; inversion Hread2; clear Hread2; subst;
       try replace m'0 with m' in * by mauto;
       try replace b0 with b in * by mauto;
       try replace bz0 with bz in * by mauto;
       try replace bs0 with bs in * by mauto;
       try replace ms0 with ms in * by mauto;
       f_equal...
-Qed.
+  Qed.
+End functional_read.
 
 #[global]
 Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt.