@@ -1328,13 +1328,20 @@ Proof.
13281328 revert HE Hsunny. pattern E, s, v, Heval.
13291329 revert E s v Heval.
13301330 eapply eval_ind; intros; eauto; cbn in *; rtoProp; eauto using Forall.
1331- - do 2 forward X; eauto. inv X.
1332- eapply X1; eauto. econstructor; cbn; eauto.
1331+ - let X := match reverse goal with H : All _ _ -> _ -> _ |- _ => H end in
1332+ do 2 forward X; eauto; inv X.
1333+ let X1 := multimatch goal with H : _ |- _ => H end in
1334+ now eapply X1; eauto; econstructor; cbn; eauto.
13331335 - econstructor; eauto. unfold fresh in H. destruct in_dec; cbn in *; congruence.
1334- - eapply X0. econstructor; cbn; eauto. eauto.
1335- - solve_all. inv X.
1336+ - let X0 := multimatch goal with H : _ |- _ => H end in
1337+ now eapply X0; [ econstructor; cbn; eauto | eauto ].
1338+ - solve_all.
1339+ let X := match goal with H : wf (vConstruct _ _ _) |- _ => H end in
1340+ inv X.
1341+ let X0 := match goal with H : All _ _ -> _ -> _ |- _ => H end in
13361342 eapply X0. eapply wf_add_multiple; eauto.
13371343 len. eapply All2_length in f4. lia.
1344+ let H := match goal with H : All (fun x => is_true (_ && _ && _)) _ |- _ => H end in
13381345 eapply All_nth_error in H. 2: eauto. rtoProp.
13391346 solve_all.
13401347 rewrite map_fst_add_multiple. len.
@@ -1344,15 +1351,18 @@ Proof.
13441351 | nNamed na => [na]
13451352 end) br.1) as -> by eauto.
13461353 clear - f4. induction f4; cbn; f_equal; destruct r, x; cbn; congruence.
1347- - do 2 forward X; eauto. invs X.
1354+ - let X := match goal with H : All _ _ -> _ -> wf (vRecClos _ _ _) |- _ => H end in
1355+ do 2 forward X; eauto; invs X.
1356+ let X0 := match goal with H : All _ (add _ _ _) -> _ -> wf _ |- _ => H end in
13481357 eapply X0.
13491358 + econstructor; cbn; eauto.
13501359 eapply wf_add_multiple; eauto.
13511360 now rewrite map_length fix_env_length.
13521361 eapply wf_fix_env; eauto.
1353- + eapply All_nth_error in X2; eauto. cbn in X2. rtoProp.
1354- rewrite map_fst_add_multiple. now rewrite map_length fix_env_length.
1355- eauto.
1362+ + let X2 := multimatch goal with H : All _ _ |- _ => H end in
1363+ eapply All_nth_error in X2; eauto; cbn in X2; rtoProp;
1364+ rewrite map_fst_add_multiple; first [ now rewrite map_length fix_env_length
1365+ | eauto ].
13561366 - assert (map fst (MCList.map2 (λ (n : ident) (d0 : def term), (n, EAst.dbody d0)) nms mfix) = nms) as EE. {
13571367 clear - f6. induction f6; cbn; f_equal; eauto. }
13581368 econstructor.
@@ -1399,9 +1409,10 @@ Proof.
13991409 destruct r as [[? []]].
14001410 destruct x; cbn in *; subst; eauto.
14011411 + eauto.
1402- - eapply X; eauto. eapply declared_constant_Forall in isdecl.
1412+ - let X := match goal with H : All _ _ -> _ -> wf _ |- _ => H end in
1413+ eapply X; eauto. eapply declared_constant_Forall in isdecl.
14031414 2: eapply Forall_impl. 2: eauto.
1404- 2: { cbn. intros [] ?. cbn in *. exact H. }
1415+ 2: { cbn. intros [] ?. cbn in *. let H := match goal with H : match _ with ConstantDecl _ => _ | _ => _ end |- _ => H end in exact H. }
14051416 cbn in *. destruct decl; cbn in *.
14061417 subst. eauto.
14071418 - solve_all. econstructor.
@@ -1579,7 +1590,8 @@ Proof.
15791590 edestruct s1 as (? & ? & ?); eauto.
15801591 invs Hv1. eexists; split; eauto. econstructor; eauto.
15811592 - invs Hrep.
1582- + invs H3.
1593+ + let H3 := match goal with H : ⊩ _ ~ tApp _ _ |- _ => H end in
1594+ invs H3.
15831595 + cbn in Hsunny. rtoProp.
15841596 edestruct s0 as (v1 & Hv1 & Hv2). 3: eauto. eauto. eauto.
15851597 invs Hv1.
@@ -1603,6 +1615,7 @@ Proof.
16031615 - assert (pars = 0) as ->. {
16041616 unfold constructor_isprop_pars_decl in *.
16051617 destruct lookup_constructor as [[[[] [? ?]] ?] | ] eqn:EE; cbn in *; try congruence.
1618+ let H0 := match goal with H : Some _ = Some _ |- _ => H end in
16061619 invs H0.
16071620 destruct lookup_env eqn:EEE; try congruence.
16081621 eapply lookup_env_wellformed in EEE; eauto.
@@ -1621,7 +1634,8 @@ Proof.
16211634 eapply All2_Set_All2 in H14. eapply All2_nth_error_Some_right in H14 as He2. 2: eauto.
16221635 destruct He2 as (br' & Hnth & nms & Hbrs & Hbr & Hnodup). invs Hv1.
16231636 edestruct s1 as (v2 & Hv1_ & Hv2_).
1624- 1: { eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
1637+ 1: { let H6 := match goal with H : is_true (forallb _ _) |- _ => H end in
1638+ eapply forallb_nth_error in H6; setoid_rewrite Hnth in H6; cbn in H6. rtoProp.
16251639 assert (nms = flat_map (λ x : name, match x with
16261640 | nAnon => []
16271641 | nNamed na => [na]
@@ -1630,6 +1644,9 @@ Proof.
16301644 { rewrite Heqnms flat_map_concat_map.
16311645 intros ? (? & ([] & <- & ?) % in_map_iff & Hd) % in_concat; cbn in *; eauto.
16321646 destruct Hd; subst; eauto.
1647+ let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
1648+ rename H6 into H6_old;
1649+ rename H6' into H6.
16331650 eapply forallb_forall in H6; eauto.
16341651 cbn in H6. unfold fresh in H6. destruct in_dec; cbn in *; congruence. }
16351652 { subst. unfold dupfree in H9. destruct dupfree_dec_ident; cbn in *; congruence. }
@@ -1647,7 +1664,10 @@ Proof.
16471664 eapply All2_Set_All2, All2_length in H10; eauto.
16481665 eapply All2_Set_All2, All2_length in Hbrs; eauto.
16491666 rewrite -> !skipn_length in *. lia.
1650- -- eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
1667+ -- let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
1668+ rename H6 into H6_old;
1669+ rename H6' into H6.
1670+ eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
16511671 enough (nms = flat_map (λ x : name, match x with
16521672 | nAnon => []
16531673 | nNamed na => [na]
@@ -1669,9 +1689,9 @@ Proof.
16691689 rewrite -> !skipn_length in *. lia.
16701690 * solve_all.
16711691 * now rewrite rev_involutive in Hv2_.
1672- - eapply X; eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
1692+ - eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
16731693 - invs Hrep.
1674- + invs H5. invs H6.
1694+ + invs H5.
16751695 + cbn -[substl] in *. rtoProp.
16761696 edestruct s0 as (v & IH1 & IH2). 3, 1, 2: eauto.
16771697 invs IH1.
@@ -1687,6 +1707,10 @@ Proof.
16871707 eapply eval_wf in IH2 as Hwf; eauto.
16881708 invs Hwf.
16891709
1710+ let H12 := match goal with H : NoDup (map fst vfix) |- _ => H end in
1711+ let H16 := match goal with H : forall nm, In nm (map fst vfix) -> ~In nm _ |- _ => H end in
1712+ let X := match goal with H : All (fun t => is_true (sunny _ _)) vfix |- _ => H end in
1713+ let X0 := match goal with H : All (fun v => wf _) _ |- _ => H end in
16901714 rename H12 into dupfree_vfix, H16 into distinct_vfix_E0, X into sunny_in_vfix, X0 into wf_E0.
16911715
16921716 edestruct s2 as (v'' & IH1'' & IH2'').
@@ -1706,7 +1730,7 @@ Proof.
17061730 }
17071731 { intros ? [-> | ?].
17081732 - eapply All_nth_error in sunny_in_vfix; eauto .
1709- cbn in sunny_in_vfix. rtoProp. unfold fresh in H2 .
1733+ cbn in sunny_in_vfix. rtoProp. unfold fresh in * .
17101734 destruct in_dec; cbn in *; eauto .
17111735 rewrite in_app_iff in n. eauto .
17121736 - eapply distinct_vfix_E0; eauto .
@@ -1776,7 +1800,8 @@ Proof.
17761800 edestruct s0 as (v & Hv1 & Hv2). 1: eauto. eauto . econstructor.
17771801 eexists. split. eauto . econstructor; eauto .
17781802 - invs Hrep.
1779- + invs H2.
1803+ + let H2 := multimatch goal with H : _ |- _ => H end in
1804+ now invs H2.
17801805 + cbn in Hsunny. rtoProp.
17811806 eapply eval_to_value in ev as Hval. invs Hval.
17821807 * destruct f'; cbn in *; try congruence.
@@ -1786,19 +1811,30 @@ Proof.
17861811 invs Hv1; destruct args using rev_ind; cbn in *; try congruence.
17871812 all: match goal with [H : _ = mkApps _ _ |- _ ] => now rewrite mkApps_app in H end.
17881813 - invs Hrep.
1789- + invs H2. eexists. split. econstructor. instantiate (1 := vs).
1790- * eapply All2_All2_Set. eapply All2_Set_All2 in H5.
1791- eapply All2_All2_mix in X. 2: eapply X0.
1792- solve_all. eapply All2_trans'. 2: eauto. 2: exact X.
1793- intros. destruct X1, p, a. eapply eval_represents_value; eauto .
1814+ + let H2 := match goal with H : ⊩ _ ~ tConstruct _ _ _ |- _ => H end in
1815+ invs H2. eexists. split. econstructor. instantiate (1 := vs).
1816+ * eapply All2_All2_Set.
1817+ let H5 := multimatch goal with H : _ |- _ => H end in
1818+ eapply All2_Set_All2 in H5.
1819+ let X := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
1820+ eapply All2_All2_mix in X. 2: let X0 := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in exact X0.
1821+ solve_all. eapply All2_trans'. 2: eauto. 2: let X := match goal with H : All2 (fun _ _ => _ * EWcbvEval.eval _ _ _) _ _ |- _ => H end in exact X.
1822+ intros x y z [? [? ?]]. eapply eval_represents_value; eauto .
17941823 * econstructor. eauto .
17951824 + cbn in Hsunny.
17961825 solve_all.
1826+ let H5' := multimatch goal with H : _ |- _ => H end in
1827+ rename H5' into H5.
17971828 eapply All2_Set_All2 in H5.
17981829 eapply All2_All_mix_left in H5. 2: eauto.
1830+ let X' := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
1831+ rename X into X_old;
1832+ rename X' into X.
1833+ let X0' := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in
1834+ rename X0' into X0.
17991835 eapply All2_All2_mix in X. 2: eapply X0.
18001836 cbn in X. eapply All2_trans' in X. 3: eapply H5.
1801- 2:{ intros. destruct X1, p, p0, a .
1837+ 2:{ intros x y z [[? r] [[s0] ?]] .
18021838 eapply s0 in r; eauto . exact r. }
18031839 assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. {
18041840 clear - X. induction X. eexists; econstructor. destruct IHX as [vs Hvs].
0 commit comments