Skip to content

Commit

Permalink
Fix some naming
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Apr 6, 2023
1 parent 8a5e984 commit 1404833
Show file tree
Hide file tree
Showing 7 changed files with 90 additions and 39 deletions.
13 changes: 9 additions & 4 deletions erasure/theories/EConstructorsAsBlocks.v
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ Section transform_blocks.
Qed.

Lemma chop_eq {A} n (l : list A) l1 l2 : chop n l = (l1, l2) -> l = l1 ++ l2.
Proof.
Proof using Type.
rewrite chop_firstn_skipn. intros [= <- <-].
now rewrite firstn_skipn.
Qed.
Expand Down Expand Up @@ -188,7 +188,7 @@ Section transform_blocks.
| view_other fn nconstr =>
mkApps (transform_blocks fn) (map transform_blocks args)
end.
Proof.
Proof using Type.
destruct (decompose_app f) eqn:da.
rewrite (decompose_app_inv da). rewrite transform_blocks_mkApps.
now eapply decompose_app_notApp.
Expand All @@ -210,7 +210,7 @@ Section transform_blocks.
P (mkApps (transform_blocks fn) (map transform_blocks args))
end) ->
P (transform_blocks (mkApps fn args)).
Proof.
Proof using Type.
intros napp.
move/isEtaExp_mkApps.
rewrite decompose_app_mkApps //.
Expand All @@ -228,7 +228,7 @@ Section transform_blocks.

Lemma transform_blocks_mkApps_eta_fn f args : isEtaExp Σ f ->
transform_blocks (mkApps f args) = mkApps (transform_blocks f) (map (transform_blocks) args).
Proof.
Proof using Type.
intros ef.
destruct (decompose_app f) eqn:df.
rewrite (decompose_app_inv df) in ef |- *.
Expand Down Expand Up @@ -1147,13 +1147,18 @@ Proof.
destruct nth_error; try now inv Heq.
destruct nth_error; invs Heq.
rewrite /wf_minductive in E. rtoProp.
let H4' := match goal with H : context[has_cstr_params] |- _ => H end in
rename H4 into H4_old;
rename H4' into H4.
rewrite haspars /= in H4.
cbn in H4. eapply eqb_eq in H4.
unfold cstr_arity in H0.
rewrite -> H4 in *. cbn in H0.
revert E1 E2.
rewrite <- H0.
rewrite !chop_firstn_skipn !firstn_all. intros [= <- <-] [= <- <-].
let X0' := match goal with H : All2 _ _ _ |- _ => H end in
rename X0' into X0.
eapply All2_length in X0 as Hlen.
cbn.
rewrite !skipn_all Hlen skipn_all firstn_all. cbn.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EEtaExpanded.v
Original file line number Diff line number Diff line change
Expand Up @@ -662,6 +662,7 @@ Proof.
destruct (isConstruct f) eqn:eqc.
destruct f => //.
- depelim H; try solve_discr_args => //.
let H3 := match goal with H : tConstruct _ _ _ = tConstruct _ _ _ |- _ => H end in
noconf H3.
eapply expanded_tConstruct_app; tea. cbn in H0. lia. solve_all.
- destruct args using rev_ind; cbn => //.
Expand Down
6 changes: 3 additions & 3 deletions erasure/theories/EEtaExpandedFix.v
Original file line number Diff line number Diff line change
Expand Up @@ -1570,7 +1570,7 @@ Lemma eval_app_cong_tApp' fl Σ t arg arg' res :
@eval (switch_unguarded_fix fl) Σ (tApp t arg') res ->
@eval (switch_unguarded_fix fl) Σ (tApp t arg) res.
Proof.
intros. depind H0.
intros X H H0. depind H0.
- eapply eval_app_cong_tApp; tea. econstructor. constructor. constructor. exact H.
- pose proof (eval_trans' H H0_0). subst a'. econstructor; tea.
- pose proof (eval_trans' H H0_0). subst av. eapply eval_fix; tea.
Expand Down Expand Up @@ -1612,7 +1612,7 @@ Lemma eval_app_cong_mkApps {fl} {Σ} {f f' res : EAst.term} {args args'} :
@eval (switch_unguarded_fix fl) Σ (mkApps f args) res.
Proof.
revert args' res; induction args using rev_ind.
- cbn. intros. eapply eval_trans. tea. now depelim X.
- cbn. intros args' res ? X ?. eapply eval_trans. tea. now depelim X.
- intros args' res evf evargs evf'.
rewrite !mkApps_app. cbn.
eapply All2_app_inv_l in evargs as [r1 [r2 [? []]]]. depelim a0. depelim a0. subst args'.
Expand Down Expand Up @@ -1737,7 +1737,7 @@ Proof.
rewrite -[tApp _ _](mkApps_app _ _ [av]) in IHeval3.
forward_keep IHeval2.
{ rewrite ha. now eapply forallb_last. }
unshelve epose proof (eval_mkApps_tFix_inv_size _ _ _ _ _ _ H') => //; auto.
unshelve epose proof (eval_mkApps_tFix_inv_size _ _ _ _ _ _ H') as X => //; auto.
intros hev.
destruct X as [[args' [hargs heq]]|].
{ solve_discr. noconf H5.
Expand Down
11 changes: 6 additions & 5 deletions erasure/theories/EWcbvEval.v
Original file line number Diff line number Diff line change
Expand Up @@ -899,7 +899,7 @@ Section Wcbv.

Lemma value_app_inv L : value (mkApps tBox L) -> L = nil.
Proof.
intros. depelim X.
intro X. depelim X.
- destruct L using rev_ind.
reflexivity.
rewrite mkApps_app in i. inv i.
Expand Down Expand Up @@ -1059,7 +1059,8 @@ Section Wcbv.
{ clear -X; induction X; constructor; auto. }
econstructor; tea; auto.
- assert (All2 eval args args).
{ clear -X0; induction X0; constructor; auto. }
{ let X0 := match goal with H : All (fun t => eval t t) _ |- _ => H end in
clear -X0; induction X0; constructor; auto. }
eapply eval_mkApps_cong => //. now eapply value_head_final.
Qed.

Expand Down Expand Up @@ -1294,7 +1295,7 @@ Section Wcbv.
All2 eval t v' ->
v = v'.
Proof.
induction 1 in v' |- *; intros H; depelim H; auto. f_equal; eauto.
induction 1 in v' |- *; intros H'; depelim H'; auto. f_equal; eauto.
now eapply eval_deterministic.
Qed.

Expand Down Expand Up @@ -2037,9 +2038,9 @@ Lemma eval_box_apps {wfl : WcbvFlags}:
eval Σ' e tBox -> eval Σ' (mkApps e x) tBox.
Proof.
intros Σ' e x H2.
revert e H2; induction x using rev_ind; cbn; intros; eauto.
revert e H2; induction x using rev_ind; cbn; intros e ? X ?; eauto.
eapply All2_app_inv_l in X as (l1' & l2' & -> & H' & H2).
depelim H2.
specialize (IHx e _ H'). simpl.
rewrite mkApps_app. simpl. econstructor; eauto.
Qed.
Qed.
3 changes: 3 additions & 0 deletions erasure/theories/EWcbvEvalEtaInd.v
Original file line number Diff line number Diff line change
Expand Up @@ -765,7 +765,10 @@ Proof.
all:intuition auto.
- eapply eval_wellformed; tea => //.
- rewrite isEtaExp_Constructor => //.
let X0 := multimatch goal with H : All2 _ _ _ |- _ => H end in
let H1 := multimatch goal with H : _ = _ |- _ => H end in
rewrite -(All2_length X0) H1. cbn. rtoProp; intuition eauto.
match goal with H : ?f ?n |- ?f ?n' => replace n' with n by congruence; exact H end.
cbn; eapply All_forallb. eapply All2_All_right; tea.
cbn. intros x y []; auto.
Qed.
82 changes: 59 additions & 23 deletions erasure/theories/EWcbvEvalNamed.v
Original file line number Diff line number Diff line change
Expand Up @@ -1328,13 +1328,20 @@ Proof.
revert HE Hsunny. pattern E, s, v, Heval.
revert E s v Heval.
eapply eval_ind; intros; eauto; cbn in *; rtoProp; eauto using Forall.
- do 2 forward X; eauto. inv X.
eapply X1; eauto. econstructor; cbn; eauto.
- let X := match reverse goal with H : All _ _ -> _ -> _ |- _ => H end in
do 2 forward X; eauto; inv X.
let X1 := multimatch goal with H : _ |- _ => H end in
now eapply X1; eauto; econstructor; cbn; eauto.
- econstructor; eauto. unfold fresh in H. destruct in_dec; cbn in *; congruence.
- eapply X0. econstructor; cbn; eauto. eauto.
- solve_all. inv X.
- let X0 := multimatch goal with H : _ |- _ => H end in
now eapply X0; [ econstructor; cbn; eauto | eauto ].
- solve_all.
let X := match goal with H : wf (vConstruct _ _ _) |- _ => H end in
inv X.
let X0 := match goal with H : All _ _ -> _ -> _ |- _ => H end in
eapply X0. eapply wf_add_multiple; eauto.
len. eapply All2_length in f4. lia.
let H := match goal with H : All (fun x => is_true (_ && _ && _)) _ |- _ => H end in
eapply All_nth_error in H. 2: eauto. rtoProp.
solve_all.
rewrite map_fst_add_multiple. len.
Expand All @@ -1344,15 +1351,18 @@ Proof.
| nNamed na => [na]
end) br.1) as -> by eauto.
clear - f4. induction f4; cbn; f_equal; destruct r, x; cbn; congruence.
- do 2 forward X; eauto. invs X.
- let X := match goal with H : All _ _ -> _ -> wf (vRecClos _ _ _) |- _ => H end in
do 2 forward X; eauto; invs X.
let X0 := match goal with H : All _ (add _ _ _) -> _ -> wf _ |- _ => H end in
eapply X0.
+ econstructor; cbn; eauto.
eapply wf_add_multiple; eauto.
now rewrite map_length fix_env_length.
eapply wf_fix_env; eauto.
+ eapply All_nth_error in X2; eauto. cbn in X2. rtoProp.
rewrite map_fst_add_multiple. now rewrite map_length fix_env_length.
eauto.
+ let X2 := multimatch goal with H : All _ _ |- _ => H end in
eapply All_nth_error in X2; eauto; cbn in X2; rtoProp;
rewrite map_fst_add_multiple; first [ now rewrite map_length fix_env_length
| eauto ].
- assert (map fst (MCList.map2 (λ (n : ident) (d0 : def term), (n, EAst.dbody d0)) nms mfix) = nms) as EE. {
clear - f6. induction f6; cbn; f_equal; eauto. }
econstructor.
Expand Down Expand Up @@ -1399,9 +1409,10 @@ Proof.
destruct r as [[? []]].
destruct x; cbn in *; subst; eauto.
+ eauto.
- eapply X; eauto. eapply declared_constant_Forall in isdecl.
- let X := match goal with H : All _ _ -> _ -> wf _ |- _ => H end in
eapply X; eauto. eapply declared_constant_Forall in isdecl.
2: eapply Forall_impl. 2: eauto.
2: { cbn. intros [] ?. cbn in *. exact H. }
2: { cbn. intros [] ?. cbn in *. let H := match goal with H : match _ with ConstantDecl _ => _ | _ => _ end |- _ => H end in exact H. }
cbn in *. destruct decl; cbn in *.
subst. eauto.
- solve_all. econstructor.
Expand Down Expand Up @@ -1579,7 +1590,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.
Expand All @@ -1603,6 +1615,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.
Expand All @@ -1621,7 +1634,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]
Expand All @@ -1630,6 +1644,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. }
Expand All @@ -1647,7 +1664,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]
Expand All @@ -1669,9 +1689,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.
Expand All @@ -1687,6 +1707,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'').
Expand All @@ -1706,7 +1730,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.
Expand Down Expand Up @@ -1776,7 +1800,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.
Expand All @@ -1786,19 +1811,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].
Expand Down
13 changes: 9 additions & 4 deletions erasure/theories/ErasureCorrectness.v
Original file line number Diff line number Diff line change
Expand Up @@ -264,6 +264,7 @@ Proof.
2:{
exists x2. split; eauto. constructor. eapply eval_iota_sing => //.
pose proof (Ee.eval_to_value _ _ He_v').
let X0 := match goal with H : Ee.value _ (EAst.mkApps _ _) |- _ => H end in
eapply value_app_inv in X0. subst. eassumption.
depelim H2.
eapply isErasable_Propositional in X0; eauto.
Expand Down Expand Up @@ -417,7 +418,11 @@ Proof.
eapply declared_constructor_from_gen in d.
eapply (declared_constructor_assumption_context d).
destruct s3 as [? [? [eqp _]]].
rewrite lenppars (firstn_app_left) // in eqp. congruence.
rewrite lenppars (firstn_app_left) // in eqp.
match goal with
| [ H : ?f (firstn ?n ?ls) ?p |- ?f (firstn ?n' ?ls) ?p ]
=> replace n' with n; first [ exact H | congruence ]
end.
move: wf_brs. now rewrite /wf_branches hctors => h; depelim h.
rewrite -eq_npars. exact s1.
- eapply All2_rev. cbn.
Expand All @@ -438,7 +443,7 @@ Proof.
constructor.
destruct x1 as [n br'].
eapply eval_iota_sing => //.
pose proof (Ee.eval_to_value _ _ He_v').
pose proof (Ee.eval_to_value _ _ He_v') as X0.
apply value_app_inv in X0; subst x0.
apply He_v'.
now rewrite -eq_npars.
Expand Down Expand Up @@ -509,7 +514,7 @@ Proof.
eapply isErasable_Proof. constructor. eauto.

eapply eval_proj_prop => //.
pose proof (Ee.eval_to_value _ _ Hty_vc').
pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
eapply value_app_inv in X0. subst. eassumption.
now rewrite -eqpars.
* rename H3 into Hinf.
Expand Down Expand Up @@ -549,7 +554,7 @@ Proof.
eassumption.
eapply isErasable_Proof.
constructor. eapply eval_proj_prop => //.
pose proof (Ee.eval_to_value _ _ Hty_vc').
pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
eapply value_app_inv in X0. subst. eassumption.
now rewrite -eqpars.
-- eapply erases_deps_eval in Hty_vc'; [|now eauto].
Expand Down

0 comments on commit 1404833

Please sign in to comment.