Fix naming

Author: JasonGross

erasure/theories/EWcbvEvalNamed.v

@@ -1589,7 +1589,8 @@ Proof.
       edestruct s1 as (? & ? & ?); eauto.
       invs Hv1. eexists; split; eauto. econstructor; eauto.
   - invs Hrep.
-    + invs H3.
+    + let H3 := match goal with H : ⊩ _ ~ tApp _ _ |- _ => H end in
+      invs H3.
     + cbn in Hsunny. rtoProp.
       edestruct s0 as (v1 & Hv1 & Hv2). 3: eauto. eauto. eauto.
       invs Hv1.
@@ -1613,6 +1614,7 @@ Proof.
   - assert (pars = 0) as ->. {
       unfold constructor_isprop_pars_decl in *.
       destruct lookup_constructor as [[[[] [? ?]] ?] | ] eqn:EE; cbn in *; try congruence.
+      let H0 := match goal with H : Some _ = Some _ |- _ => H end in
       invs H0.
       destruct lookup_env eqn:EEE; try congruence.
       eapply lookup_env_wellformed in EEE; eauto.
@@ -1631,7 +1633,8 @@ Proof.
       eapply All2_Set_All2 in H14. eapply All2_nth_error_Some_right in H14 as He2. 2: eauto.
       destruct He2 as (br' & Hnth & nms & Hbrs & Hbr & Hnodup). invs Hv1.
       edestruct s1 as (v2 & Hv1_ & Hv2_).
-      1: { eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
+      1: { let H6 := match goal with H : is_true (forallb _ _) |- _ => H end in
+        eapply forallb_nth_error in H6; setoid_rewrite Hnth in H6; cbn in H6. rtoProp.
            assert (nms = flat_map (λ x : name, match x with
                | nAnon => []
                | nNamed na => [na]
@@ -1640,6 +1643,9 @@ Proof.
            { rewrite Heqnms flat_map_concat_map.
              intros ? (? & ([] & <- & ?) % in_map_iff & Hd) % in_concat; cbn in *; eauto.
             destruct Hd; subst; eauto.
+            let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
+            rename H6 into H6_old;
+            rename H6' into H6.
             eapply forallb_forall in H6; eauto.
             cbn in H6. unfold fresh in H6. destruct in_dec; cbn in *; congruence. }
             { subst. unfold dupfree in H9. destruct dupfree_dec_ident; cbn in *; congruence. }
@@ -1657,7 +1663,10 @@ Proof.
            eapply All2_Set_All2, All2_length in H10; eauto.
            eapply All2_Set_All2, All2_length in Hbrs; eauto.
            rewrite -> !skipn_length in *. lia.
-        -- eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
+        -- let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
+           rename H6 into H6_old;
+           rename H6' into H6.
+           eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
            enough (nms = flat_map (λ x : name, match x with
            | nAnon => []
            | nNamed na => [na]
@@ -1679,9 +1688,9 @@ Proof.
         rewrite -> !skipn_length in *. lia.
       * solve_all.
       * now rewrite rev_involutive in Hv2_.
-  - eapply X; eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
+  - eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
   - invs Hrep.
-    + invs H5. invs H6.
+    + invs H5.
     + cbn -[substl] in *. rtoProp.
       edestruct s0 as (v & IH1 & IH2). 3, 1, 2: eauto.
       invs IH1.
@@ -1697,6 +1706,10 @@ Proof.
       eapply eval_wf in IH2 as Hwf; eauto.
       invs Hwf.
 
+      let H12 := match goal with H : NoDup (map fst vfix) |- _ => H end in
+      let H16 := match goal with H : forall nm, In nm (map fst vfix) -> ~In nm _ |- _ => H end in
+      let X := match goal with H : All (fun t => is_true (sunny _ _)) vfix |- _ => H end in
+      let X0 := match goal with H : All (fun v => wf _) _ |- _ => H end in
       rename H12 into dupfree_vfix, H16 into distinct_vfix_E0, X into sunny_in_vfix, X0 into wf_E0.
 
       edestruct s2 as (v'' & IH1'' & IH2'').
@@ -1716,7 +1729,7 @@ Proof.
       }
       { intros ? [-> | ?].
         - eapply All_nth_error in sunny_in_vfix; eauto.
-          cbn in sunny_in_vfix. rtoProp. unfold fresh in H2.
+          cbn in sunny_in_vfix. rtoProp. unfold fresh in *.
           destruct in_dec; cbn in *; eauto.
           rewrite in_app_iff in n. eauto.
         - eapply distinct_vfix_E0; eauto.
@@ -1786,7 +1799,8 @@ Proof.
       edestruct s0 as (v & Hv1 & Hv2). 1: eauto. eauto. econstructor.
       eexists. split. eauto. econstructor; eauto.
   - invs Hrep.
-    + invs H2.
+    + let H2 := multimatch goal with H : _ |- _ => H end in
+      now invs H2.
     + cbn in Hsunny. rtoProp.
       eapply eval_to_value in ev as Hval. invs Hval.
       * destruct f'; cbn in *; try congruence.
@@ -1796,19 +1810,30 @@ Proof.
         invs Hv1; destruct args using rev_ind; cbn in *; try congruence.
         all: match goal with [H : _ = mkApps _ _ |- _ ] => now rewrite mkApps_app in H end.
   - invs Hrep.
-    + invs H2. eexists. split. econstructor.  instantiate (1 := vs).
-      * eapply All2_All2_Set. eapply All2_Set_All2 in H5.
-        eapply All2_All2_mix in X. 2: eapply X0.
-        solve_all. eapply All2_trans'. 2: eauto. 2: exact X.
-        intros. destruct X1, p, a. eapply eval_represents_value; eauto.
+    + let H2 := match goal with H : ⊩ _ ~ tConstruct _ _ _ |- _ => H end in
+      invs H2. eexists. split. econstructor.  instantiate (1 := vs).
+      * eapply All2_All2_Set.
+        let H5 := multimatch goal with H : _ |- _ => H end in
+        eapply All2_Set_All2 in H5.
+        let X := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
+        eapply All2_All2_mix in X. 2: let X0 := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in exact X0.
+        solve_all. eapply All2_trans'. 2: eauto. 2: let X := match goal with H : All2 (fun _ _ => _ * EWcbvEval.eval _ _ _) _ _ |- _ => H end in exact X.
+        intros x y z [? [? ?]]. eapply eval_represents_value; eauto.
       * econstructor. eauto.
     + cbn in Hsunny.
       solve_all.
+      let H5' := multimatch goal with H : _ |- _ => H end in
+      rename H5' into H5.
       eapply All2_Set_All2 in H5.
       eapply All2_All_mix_left in H5. 2: eauto.
+       let X' := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
+       rename X into X_old;
+       rename X' into X.
+       let X0' := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in
+       rename X0' into X0.
        eapply All2_All2_mix in X. 2: eapply X0.
        cbn in X. eapply All2_trans' in X. 3: eapply H5.
-       2:{ intros. destruct X1, p, p0, a.
+       2:{ intros x y z [[? r] [[s0] ?]].
            eapply s0 in r; eauto. exact r. }
        assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. {
          clear - X. induction X. eexists; econstructor. destruct IHX as [vs Hvs].