@@ -1327,13 +1327,20 @@ Proof.
13271327 revert HE Hsunny. pattern E, s, v, Heval.
13281328 revert E s v Heval.
13291329 eapply eval_ind; intros; eauto; cbn in *; rtoProp; eauto using Forall.
1330- - do 2 forward X; eauto. inv X.
1331- eapply X1; eauto. econstructor; cbn; eauto.
1330+ - let X := match reverse goal with H : All _ _ -> _ -> _ |- _ => H end in
1331+ do 2 forward X; eauto; inv X.
1332+ let X1 := multimatch goal with H : _ |- _ => H end in
1333+ now eapply X1; eauto; econstructor; cbn; eauto.
13321334 - econstructor; eauto. unfold fresh in H. destruct in_dec; cbn in *; congruence.
1333- - eapply X0. econstructor; cbn; eauto. eauto.
1334- - solve_all. inv X.
1335+ - let X0 := multimatch goal with H : _ |- _ => H end in
1336+ now eapply X0; [ econstructor; cbn; eauto | eauto ].
1337+ - solve_all.
1338+ let X := match goal with H : wf (vConstruct _ _ _) |- _ => H end in
1339+ inv X.
1340+ let X0 := match goal with H : All _ _ -> _ -> _ |- _ => H end in
13351341 eapply X0. eapply wf_add_multiple; eauto.
13361342 len. eapply All2_length in f4. lia.
1343+ let H := match goal with H : All (fun x => is_true (_ && _ && _)) _ |- _ => H end in
13371344 eapply All_nth_error in H. 2: eauto. rtoProp.
13381345 solve_all.
13391346 rewrite map_fst_add_multiple. len.
@@ -1343,15 +1350,18 @@ Proof.
13431350 | nNamed na => [na]
13441351 end) br.1) as -> by eauto.
13451352 clear - f4. induction f4; cbn; f_equal; destruct r, x; cbn; congruence.
1346- - do 2 forward X; eauto. invs X.
1353+ - let X := match goal with H : All _ _ -> _ -> wf (vRecClos _ _ _) |- _ => H end in
1354+ do 2 forward X; eauto; invs X.
1355+ let X0 := match goal with H : All _ (add _ _ _) -> _ -> wf _ |- _ => H end in
13471356 eapply X0.
13481357 + econstructor; cbn; eauto.
13491358 eapply wf_add_multiple; eauto.
13501359 now rewrite map_length fix_env_length.
13511360 eapply wf_fix_env; eauto.
1352- + eapply All_nth_error in X2; eauto. cbn in X2. rtoProp.
1353- rewrite map_fst_add_multiple. now rewrite map_length fix_env_length.
1354- eauto.
1361+ + let X2 := multimatch goal with H : All _ _ |- _ => H end in
1362+ eapply All_nth_error in X2; eauto; cbn in X2; rtoProp;
1363+ rewrite map_fst_add_multiple; first [ now rewrite map_length fix_env_length
1364+ | eauto ].
13551365 - assert (map fst (MCList.map2 (λ (n : ident) (d0 : def term), (n, EAst.dbody d0)) nms mfix) = nms) as EE. {
13561366 clear - f6. induction f6; cbn; f_equal; eauto. }
13571367 econstructor.
@@ -1398,9 +1408,10 @@ Proof.
13981408 destruct r as [[? []]].
13991409 destruct x; cbn in *; subst; eauto.
14001410 + eauto.
1401- - eapply X; eauto. eapply declared_constant_Forall in isdecl.
1411+ - let X := match goal with H : All _ _ -> _ -> wf _ |- _ => H end in
1412+ eapply X; eauto. eapply declared_constant_Forall in isdecl.
14021413 2: eapply Forall_impl. 2: eauto.
1403- 2: { cbn. intros [] ?. cbn in *. exact H. }
1414+ 2: { cbn. intros [] ?. cbn in *. let H := match goal with H : match _ with ConstantDecl _ => _ | _ => _ end |- _ => H end in exact H. }
14041415 cbn in *. destruct decl; cbn in *.
14051416 subst. eauto.
14061417 - solve_all. econstructor.
@@ -1578,7 +1589,8 @@ Proof.
15781589 edestruct s1 as (? & ? & ?); eauto.
15791590 invs Hv1. eexists; split; eauto. econstructor; eauto.
15801591 - invs Hrep.
1581- + invs H3.
1592+ + let H3 := match goal with H : ⊩ _ ~ tApp _ _ |- _ => H end in
1593+ invs H3.
15821594 + cbn in Hsunny. rtoProp.
15831595 edestruct s0 as (v1 & Hv1 & Hv2). 3: eauto. eauto. eauto.
15841596 invs Hv1.
@@ -1602,6 +1614,7 @@ Proof.
16021614 - assert (pars = 0) as ->. {
16031615 unfold constructor_isprop_pars_decl in *.
16041616 destruct lookup_constructor as [[[[] [? ?]] ?] | ] eqn:EE; cbn in *; try congruence.
1617+ let H0 := match goal with H : Some _ = Some _ |- _ => H end in
16051618 invs H0.
16061619 destruct lookup_env eqn:EEE; try congruence.
16071620 eapply lookup_env_wellformed in EEE; eauto.
@@ -1620,7 +1633,8 @@ Proof.
16201633 eapply All2_Set_All2 in H14. eapply All2_nth_error_Some_right in H14 as He2. 2: eauto.
16211634 destruct He2 as (br' & Hnth & nms & Hbrs & Hbr & Hnodup). invs Hv1.
16221635 edestruct s1 as (v2 & Hv1_ & Hv2_).
1623- 1: { eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
1636+ 1: { let H6 := match goal with H : is_true (forallb _ _) |- _ => H end in
1637+ eapply forallb_nth_error in H6; setoid_rewrite Hnth in H6; cbn in H6. rtoProp.
16241638 assert (nms = flat_map (λ x : name, match x with
16251639 | nAnon => []
16261640 | nNamed na => [na]
@@ -1629,6 +1643,9 @@ Proof.
16291643 { rewrite Heqnms flat_map_concat_map.
16301644 intros ? (? & ([] & <- & ?) % in_map_iff & Hd) % in_concat; cbn in *; eauto.
16311645 destruct Hd; subst; eauto.
1646+ let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
1647+ rename H6 into H6_old;
1648+ rename H6' into H6.
16321649 eapply forallb_forall in H6; eauto.
16331650 cbn in H6. unfold fresh in H6. destruct in_dec; cbn in *; congruence. }
16341651 { subst. unfold dupfree in H9. destruct dupfree_dec_ident; cbn in *; congruence. }
@@ -1646,7 +1663,10 @@ Proof.
16461663 eapply All2_Set_All2, All2_length in H10; eauto.
16471664 eapply All2_Set_All2, All2_length in Hbrs; eauto.
16481665 rewrite -> !skipn_length in *. lia.
1649- -- eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
1666+ -- let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
1667+ rename H6 into H6_old;
1668+ rename H6' into H6.
1669+ eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
16501670 enough (nms = flat_map (λ x : name, match x with
16511671 | nAnon => []
16521672 | nNamed na => [na]
@@ -1668,9 +1688,9 @@ Proof.
16681688 rewrite -> !skipn_length in *. lia.
16691689 * solve_all.
16701690 * now rewrite rev_involutive in Hv2_.
1671- - eapply X; eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
1691+ - eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
16721692 - invs Hrep.
1673- + invs H5. invs H6.
1693+ + invs H5.
16741694 + cbn -[substl] in *. rtoProp.
16751695 edestruct s0 as (v & IH1 & IH2). 3, 1, 2: eauto.
16761696 invs IH1.
@@ -1686,6 +1706,10 @@ Proof.
16861706 eapply eval_wf in IH2 as Hwf; eauto.
16871707 invs Hwf.
16881708
1709+ let H12 := match goal with H : NoDup (map fst vfix) |- _ => H end in
1710+ let H16 := match goal with H : forall nm, In nm (map fst vfix) -> ~In nm _ |- _ => H end in
1711+ let X := match goal with H : All (fun t => is_true (sunny _ _)) vfix |- _ => H end in
1712+ let X0 := match goal with H : All (fun v => wf _) _ |- _ => H end in
16891713 rename H12 into dupfree_vfix, H16 into distinct_vfix_E0, X into sunny_in_vfix, X0 into wf_E0.
16901714
16911715 edestruct s2 as (v'' & IH1'' & IH2'').
@@ -1705,7 +1729,7 @@ Proof.
17051729 }
17061730 { intros ? [-> | ?].
17071731 - eapply All_nth_error in sunny_in_vfix; eauto .
1708- cbn in sunny_in_vfix. rtoProp. unfold fresh in H2 .
1732+ cbn in sunny_in_vfix. rtoProp. unfold fresh in * .
17091733 destruct in_dec; cbn in *; eauto .
17101734 rewrite in_app_iff in n. eauto .
17111735 - eapply distinct_vfix_E0; eauto .
@@ -1775,7 +1799,8 @@ Proof.
17751799 edestruct s0 as (v & Hv1 & Hv2). 1: eauto. eauto . econstructor.
17761800 eexists. split. eauto . econstructor; eauto .
17771801 - invs Hrep.
1778- + invs H2.
1802+ + let H2 := multimatch goal with H : _ |- _ => H end in
1803+ now invs H2.
17791804 + cbn in Hsunny. rtoProp.
17801805 eapply eval_to_value in ev as Hval. invs Hval.
17811806 * destruct f'; cbn in *; try congruence.
@@ -1785,19 +1810,30 @@ Proof.
17851810 invs Hv1; destruct args using rev_ind; cbn in *; try congruence.
17861811 all: match goal with [H : _ = mkApps _ _ |- _ ] => now rewrite mkApps_app in H end.
17871812 - invs Hrep.
1788- + invs H2. eexists. split. econstructor. instantiate (1 := vs).
1789- * eapply All2_All2_Set. eapply All2_Set_All2 in H5.
1790- eapply All2_All2_mix in X. 2: eapply X0.
1791- solve_all. eapply All2_trans'. 2: eauto. 2: exact X.
1792- intros. destruct X1, p, a. eapply eval_represents_value; eauto .
1813+ + let H2 := match goal with H : ⊩ _ ~ tConstruct _ _ _ |- _ => H end in
1814+ invs H2. eexists. split. econstructor. instantiate (1 := vs).
1815+ * eapply All2_All2_Set.
1816+ let H5 := multimatch goal with H : _ |- _ => H end in
1817+ eapply All2_Set_All2 in H5.
1818+ let X := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
1819+ eapply All2_All2_mix in X. 2: let X0 := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in exact X0.
1820+ solve_all. eapply All2_trans'. 2: eauto. 2: let X := match goal with H : All2 (fun _ _ => _ * EWcbvEval.eval _ _ _) _ _ |- _ => H end in exact X.
1821+ intros x y z [? [? ?]]. eapply eval_represents_value; eauto .
17931822 * econstructor. eauto .
17941823 + cbn in Hsunny.
17951824 solve_all.
1825+ let H5' := multimatch goal with H : _ |- _ => H end in
1826+ rename H5' into H5.
17961827 eapply All2_Set_All2 in H5.
17971828 eapply All2_All_mix_left in H5. 2: eauto.
1829+ let X' := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
1830+ rename X into X_old;
1831+ rename X' into X.
1832+ let X0' := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in
1833+ rename X0' into X0.
17981834 eapply All2_All2_mix in X. 2: eapply X0.
17991835 cbn in X. eapply All2_trans' in X. 3: eapply H5.
1800- 2:{ intros. destruct X1, p, p0, a .
1836+ 2:{ intros x y z [[? r] [[s0] ?]] .
18011837 eapply s0 in r; eauto . exact r. }
18021838 assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. {
18031839 clear - X. induction X. eexists; econstructor. destruct IHX as [vs Hvs].
0 commit comments