Skip to content

Commit

Permalink
squash typing hypothesis in precond
Browse files Browse the repository at this point in the history
  • Loading branch information
@tabareau
tabareau committed Dec 1, 2023
1 parent 6eef155 commit 6c0bcf5
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 181 deletions.
204 changes: 23 additions & 181 deletions erasure-plugin/theories/ErasureCorrectness.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1519,164 +1519,6 @@ Qed.

Arguments PCUICFirstorder.firstorder_ind _ _ : clear implicits.

Section PCUICExpandLets.
Import PCUICAst PCUICAstUtils PCUICFirstorder.
Import PCUICEnvironment.
Import PCUICExpandLets PCUICExpandLetsCorrectness.

Lemma trans_axiom_free Σ : axiom_free Σ -> axiom_free (trans_global_env Σ).
Proof.
intros ax kn decl.
rewrite /trans_global_env /= /PCUICAst.declared_constant /= /trans_global_decls.
intros h; apply PCUICElimination.In_map in h as [[kn' decl'] [hin heq]].
noconf heq. destruct decl'; noconf H.
apply ax in hin.
destruct c as [? [] ? ?] => //.
Qed.

Lemma expand_lets_preserves_fo (Σ : global_env_ext) Γ v :
wf Σ ->
firstorder_value Σ Γ v ->
firstorder_value (trans_global Σ) (trans_local Γ) (trans v).
Proof.
intros wfΣ; move: v; apply: firstorder_value_inds.
intros i n ui u args pandi hty hargs ihargs isp.
rewrite trans_mkApps. econstructor.
apply expand_lets_sound in hty.
rewrite !trans_mkApps in hty. cbn in hty. exact hty.
ELiftSubst.solve_all.
move/negbTE: isp.
rewrite /PCUICFirstorder.isPropositional.
rewrite /lookup_inductive /lookup_inductive_gen /lookup_minductive_gen trans_lookup.
destruct lookup_env => //. destruct g => //. cbn. rewrite nth_error_mapi.
destruct nth_error => //=.
rewrite /PCUICFirstorder.isPropositionalArity.
rewrite (trans_destArity []). destruct destArity => //.
destruct p => //. now intros ->.
Qed.

Lemma forallb_mapi {A B} (f f' : nat -> A -> B) (g g' : B -> bool) l :
(forall n x, nth_error l n = Some x -> g (f n x) = g' (f' n x)) ->
forallb g (mapi f l) = forallb g' (mapi f' l).
Proof.
unfold mapi.
intros.
assert
(forall (n : nat) (x : A), nth_error l n = Some x -> g (f (0 + n) x) = g' (f' (0 + n) x)).
{ intros n x. now apply H. }
clear H.
revert H0.
generalize 0.
induction l; cbn; auto.
intros n hfg. f_equal. specialize (hfg 0). rewrite Nat.add_0_r in hfg. now apply hfg.
eapply IHl. intros. replace (S n + n0) with (n + S n0) by lia. eapply hfg.
now cbn.
Qed.

Lemma forallb_mapi_impl {A B} (f f' : nat -> A -> B) (g g' : B -> bool) l :
(forall n x, nth_error l n = Some x -> g (f n x) -> g' (f' n x)) ->
forallb g (mapi f l) -> forallb g' (mapi f' l).
Proof.
unfold mapi.
intros hfg.
assert
(forall (n : nat) (x : A), nth_error l n = Some x -> g (f (0 + n) x) -> g' (f' (0 + n) x)).
{ intros n x ?. now apply hfg. }
clear hfg.
revert H.
generalize 0.
induction l; cbn; auto.
intros n hfg. move/andP => [] hg hf.
pose proof (hfg 0). rewrite Nat.add_0_r in H. apply H in hg => //. rewrite hg /=.
eapply IHl. intros. replace (S n + n0) with (n + S n0) by lia. eapply hfg. now cbn.
now rewrite Nat.add_succ_r. assumption.
Qed.

Lemma expand_firstorder_type Σ n k t :
(forall nm, plookup_env (firstorder_env' Σ) nm = Some true ->
plookup_env (firstorder_env' (trans_global_decls Σ)) nm = Some true) ->
@PCUICFirstorder.firstorder_type (firstorder_env' Σ) n k t ->
@PCUICFirstorder.firstorder_type (firstorder_env' (trans_global_decls Σ)) n k (trans t).
Proof.
rewrite /PCUICFirstorder.firstorder_type /PCUICFirstorder.firstorder_env.
pose proof (trans_decompose_app t).
destruct decompose_app. rewrite {}H. cbn.
case: t0 => //=.
- intros n' hn. destruct l => //.
- case => /= kn _ _ hd. destruct l => //.
destruct plookup_env eqn:hp => //.
destruct b => //.
eapply hd in hp. rewrite hp //.
Qed.

Lemma trans_firstorder_mutind Σ m :
(forall nm, plookup_env (firstorder_env' Σ) nm = Some true ->
plookup_env (firstorder_env' (trans_global_decls Σ)) nm = Some true) ->
@firstorder_mutind (firstorder_env' Σ) m ->
@firstorder_mutind (firstorder_env' (trans_global_decls Σ)) (trans_minductive_body m).
Proof.
intros he.
rewrite /firstorder_mutind. f_equal.
rewrite /trans_minductive_body /=.
rewrite -{1}[ind_bodies m]map_id. rewrite -mapi_cst_map.
move/andP => [] -> /=.
eapply forallb_mapi_impl.
intros n x hnth.
rewrite /firstorder_oneind. destruct x; cbn.
move/andP => [] hc ->; rewrite andb_true_r.
rewrite forallb_map. solve_all.
move: H; rewrite /firstorder_con /=.
rewrite !rev_app_distr !alli_app.
move/andP => [hp ha]. apply/andP; split.
- len. rewrite /trans_local -map_rev alli_map.
eapply alli_impl; tea. intros i []. cbn.
now eapply expand_firstorder_type.
- len. len in ha. clear -ha he.
move: ha; generalize (cstr_args x) as args.
induction args => ha; cbn => //.
destruct a as [na [] ?] => /=. eapply IHargs. cbn in ha.
rewrite alli_app in ha. move/andP: ha => [] //.
cbn. rewrite PCUICSigmaCalculus.smash_context_acc /=.
cbn in ha. rewrite alli_app in ha. move/andP: ha => [] // hc hd.
rewrite alli_app. apply/andP. split. apply IHargs => //.
len. cbn. rewrite andb_true_r. cbn in hd. rewrite andb_true_r in hd. len in hd.
clear -he hd. move: hd. rewrite /firstorder_type.
destruct (decompose_app decl_type) eqn:e. cbn.
destruct t0 => //; apply decompose_app_inv in e; rewrite e.
destruct l => //.
{ move/andP => [] /Nat.leb_le hn /Nat.ltb_lt hn'.
rewrite trans_mkApps PCUICLiftSubst.lift_mkApps PCUICLiftSubst.subst_mkApps
decompose_app_mkApps //=.
{ destruct nth_error eqn:hnth.
pose proof (nth_error_Some_length hnth).
move: hnth H.
destruct (Nat.leb_spec #|args| n). len. lia. len. lia. now cbn. }
destruct nth_error eqn:hnth.
move/nth_error_Some_length: hnth. len. destruct (Nat.leb_spec #|args| n). lia. lia. len.
destruct (Nat.leb_spec #|args| n). apply/andP. split.
eapply Nat.leb_le. lia. apply Nat.ltb_lt. lia.
apply/andP; split. apply Nat.leb_le. lia. apply Nat.ltb_lt. lia. }
{ rewrite trans_mkApps PCUICLiftSubst.lift_mkApps PCUICLiftSubst.subst_mkApps
decompose_app_mkApps //=.
destruct ind, l => //=. destruct plookup_env eqn:hp => //.
destruct b => //. apply he in hp. rewrite hp //. }
Qed.

Lemma trans_firstorder_env Σ :
(forall nm, plookup_env (firstorder_env' Σ) nm = Some true ->
plookup_env (firstorder_env' (trans_global_decls Σ)) nm = Some true).
Proof.
induction Σ; cbn => //.
destruct a. destruct g => //=.
intros nm.
destruct eqb => //. now apply IHΣ.
intros nm. destruct eqb => //.
intros [=]. f_equal.
now eapply trans_firstorder_mutind. apply IHΣ.
Qed.

End PCUICExpandLets.

Section pipeline_cond.

Instance cf : checker_flags := extraction_checker_flags.
Expand All @@ -1690,13 +1532,13 @@ Section pipeline_cond.
Variable expΣ : PCUICEtaExpand.expanded_global_env Σ.1.
Variable expt : PCUICEtaExpand.expanded Σ.1 [] t.

Variable typing : PCUICTyping.typing Σ [] t T.
Variable typing : ∥PCUICTyping.typing Σ [] t T∥.

Variable Normalisation : (forall Σ, wf_ext Σ -> PCUICSN.NormalizationIn Σ).

Lemma precond : pre verified_erasure_pipeline (Σ, t).
Proof.
hnf. repeat eapply conj; sq; cbn; eauto.
hnf. destruct typing. repeat eapply conj; sq; cbn; eauto.
- red. cbn. eauto.
- intros. red. intros. now eapply Normalisation.
Qed.
Expand All @@ -1707,7 +1549,7 @@ Section pipeline_cond.

Lemma precond2 : pre verified_erasure_pipeline (Σ, v).
Proof.
cbn. destruct Heval. repeat eapply conj; sq; cbn; eauto.
cbn. destruct typing, Heval. repeat eapply conj; sq; cbn; eauto.
- red. cbn. split; eauto.
eexists.
eapply PCUICClassification.subject_reduction_eval; eauto.
Expand Down Expand Up @@ -1737,7 +1579,7 @@ Section pipeline_theorem.
Variable u : Universes.Instance.t.
Variable args : list PCUICAst.term.

Variable typing : PCUICTyping.typing Σ [] t (PCUICAst.mkApps (PCUICAst.tInd i u) args).
Variable typing : ∥PCUICTyping.typing Σ [] t (PCUICAst.mkApps (PCUICAst.tInd i u) args)∥.

Variable fo : @PCUICFirstorder.firstorder_ind Σ (PCUICFirstorder.firstorder_env Σ) i.

Expand All @@ -1752,7 +1594,7 @@ Section pipeline_theorem.

Lemma fo_v : PCUICFirstorder.firstorder_value Σ [] v.
Proof.
destruct Heval. sq.
destruct typing, Heval. sq.
eapply PCUICFirstorder.firstorder_value_spec; eauto.
- eapply PCUICClassification.subject_reduction_eval; eauto.
- eapply PCUICWcbvEval.eval_to_value; eauto.
Expand All @@ -1770,7 +1612,7 @@ Section pipeline_theorem.
cbn [fst snd].
intros h.
destruct_compose.
destruct Heval.
destruct typing as [typing'], Heval.
assert (eqtr : PCUICExpandLets.trans v = v).
{ clear -hv.
move: v hv.
Expand Down Expand Up @@ -1800,7 +1642,7 @@ Section pipeline_theorem.
apply HΣ. apply PCUICExpandLetsCorrectness.trans_wf, HΣ.
2:{ eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in X. }
eapply PCUICWcbvEval.eval_closed; tea. apply HΣ.
unshelve apply (PCUICClosedTyp.subject_closed typing). }
unshelve apply (PCUICClosedTyp.subject_closed typing'). }
specialize (H0 _ eq_refl).
rewrite /p.
rewrite erase_transform_fo //.
Expand Down Expand Up @@ -1900,7 +1742,7 @@ Section pipeline_theorem.
cbn [transform pcuic_expand_lets_transform].
intros pre1. destruct_compose. intros pre2.
destruct lambdabox_pres_fo as [fn [tr hfn]].
destruct tr. pose proof (Heval' := Heval). sq. rewrite transform_fo.
destruct tr. destruct typing as [typing']. pose proof (Heval' := Heval). sq. rewrite transform_fo.
{ intro. eapply preserves_fo. }
assert (eqtr : PCUICExpandLets.trans v = v).
{ clear -hv.
Expand All @@ -1910,7 +1752,7 @@ Section pipeline_theorem.
rewrite PCUICExpandLetsCorrectness.trans_mkApps /=.
f_equal. ELiftSubst.solve_all. }
assert (PCUICFirstorder.firstorder_value (PCUICExpandLets.trans_global_env Σ.1, Σ.2) [] v).
{ eapply expand_lets_preserves_fo in hv; eauto. now rewrite eqtr in hv. }
{ eapply PCUICExpandLetsCorrectness.expand_lets_preserves_fo in hv; eauto. now rewrite eqtr in hv. }
assert (Normalisation': PCUICSN.NormalizationIn (PCUICExpandLets.trans_global Σ)).
{ destruct pre1 as [[] ?]. apply a. cbn. apply w. }
set (Σ' := build_global_env_map (PCUICExpandLets.trans_global_env Σ.1)).
Expand All @@ -1921,19 +1763,19 @@ Section pipeline_theorem.
eapply (PCUICClassification.subject_reduction_eval (Σ := Σ)) in Heval'; tea.
eapply PCUICExpandLetsCorrectness.expand_lets_sound in Heval'.
now rewrite PCUICExpandLetsCorrectness.trans_mkApps /= in Heval'. }
forward H0. { cbn. now eapply trans_axiom_free. }
forward H0. { now eapply PCUICExpandLetsCorrectness.trans_axiom_free. }
forward H0.
{ cbn. clear -HΣ fo.
move: fo.
rewrite /PCUICFirstorder.firstorder_ind /= PCUICExpandLetsCorrectness.trans_lookup /=.
destruct PCUICAst.PCUICEnvironment.lookup_env => //. destruct g => //=.
eapply trans_firstorder_mutind. eapply trans_firstorder_env. }
eapply PCUICExpandLetsCorrectness.trans_firstorder_mutind. eapply PCUICExpandLetsCorrectness.trans_firstorder_env. }
forward H0. { cbn. rewrite -eqtr.
unshelve eapply (PCUICExpandLetsCorrectness.trans_wcbveval (Σ := Σ)); tea. exact extraction_checker_flags.
apply HΣ. apply PCUICExpandLetsCorrectness.trans_wf, HΣ.
2:{ rewrite eqtr. eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in Heval'. }
eapply PCUICWcbvEval.eval_closed; tea. apply HΣ.
unshelve apply (PCUICClosedTyp.subject_closed typing). now rewrite eqtr. }
unshelve apply (PCUICClosedTyp.subject_closed typing'). now rewrite eqtr. }
specialize (H0 _ eq_refl).
rewrite /p.
rewrite erase_transform_fo //. { cbn. rewrite eqtr. exact H. }
Expand All @@ -1947,26 +1789,26 @@ Section pipeline_theorem.
EGlobalEnv.extends Σ_v Σ_t.
Proof.
unfold Σ_v, Σ_t. unfold verified_erasure_pipeline.
repeat (destruct_compose; intro). destruct Heval.
repeat (destruct_compose; intro). destruct typing as [typing'], Heval.
cbn [transform compose pcuic_expand_lets_transform] in *.
unfold run, time.
cbn [transform erase_transform] in *.
set (erase_program _ _). set (erase_program _ _).
eapply verified_lambdabox_pipeline_extends.
eapply extends_erase_pcuic_program; eauto; cbn.
eapply extends_erase_pcuic_program; eauto.
unshelve eapply (PCUICExpandLetsCorrectness.trans_wcbveval (cf := extraction_checker_flags) (Σ := (Σ.1, Σ.2))).
{ now eapply PCUICExpandLetsCorrectness.trans_wf. }
{ clear -HΣ typing. now eapply PCUICClosedTyp.subject_closed in typing. }
{ clear -HΣ typing'. now eapply PCUICClosedTyp.subject_closed in typing'. }
assumption.
now eapply trans_axiom_free.
pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing).
now eapply PCUICExpandLetsCorrectness.trans_axiom_free.
pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing').
rewrite PCUICExpandLetsCorrectness.trans_mkApps in X. eapply X.
move: fo. clear.
{ rewrite /PCUICFirstorder.firstorder_ind /=.
rewrite PCUICExpandLetsCorrectness.trans_lookup.
destruct PCUICAst.PCUICEnvironment.lookup_env => //.
destruct g => //=.
eapply trans_firstorder_mutind. eapply trans_firstorder_env. }
eapply PCUICExpandLetsCorrectness.trans_firstorder_mutind. eapply PCUICExpandLetsCorrectness.trans_firstorder_env. }
Qed.

Lemma verified_erasure_pipeline_theorem :
Expand Down Expand Up @@ -2016,7 +1858,7 @@ Section pipeline_theorem.
cbn [transform compose pcuic_expand_lets_transform] in *.
cbn [transform erase_transform] in *.
destruct Heval.
pose proof typing as typing'.
pose proof typing as [typing']. pose proof typing as [typing''].
eapply PCUICClassification.subject_reduction_eval in typing'; tea.
eapply PCUICExpandLetsCorrectness.pcuic_expand_lets in typing'.
rewrite PCUICExpandLetsCorrectness.trans_mkApps /= in typing'.
Expand All @@ -2032,15 +1874,15 @@ Section pipeline_theorem.
eapply (ErasureFunctionProperties.firstorder_erases_deterministic optimized_abstract_env_impl wfe Σ.2) in b0. 3:tea.
2:{ cbn. reflexivity. }
2:{ eapply PCUICExpandLetsCorrectness.trans_wcbveval. eapply PCUICWcbvEval.eval_closed; tea. apply HΣ.
clear -typing HΣ; now eapply PCUICClosedTyp.subject_closed in typing.
clear -typing'' HΣ. now eapply PCUICClosedTyp.subject_closed in typing''.
eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in X0. }
(* 2:{ clear -fo. cbn. now eapply (PCUICExpandLetsCorrectness.trans_firstorder_ind Σ). }
eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in X. } *)
2:{ clear -fo. revert fo. rewrite /PCUICFirstorder.firstorder_ind /=.
rewrite PCUICExpandLetsCorrectness.trans_lookup.
destruct PCUICAst.PCUICEnvironment.lookup_env => //.
destruct g => //=.
eapply trans_firstorder_mutind. eapply trans_firstorder_env. }
eapply PCUICExpandLetsCorrectness.trans_firstorder_mutind. eapply PCUICExpandLetsCorrectness.trans_firstorder_env. }
2:{ apply HΣ. }
2:{ apply PCUICExpandLetsCorrectness.trans_wf, HΣ. }
rewrite b0. intros obs. constructor.
Expand All @@ -2053,10 +1895,10 @@ Section pipeline_theorem.
eapply extends_erase_pcuic_program. cbn.
unshelve eapply (PCUICExpandLetsCorrectness.trans_wcbveval (cf := extraction_checker_flags) (Σ := (Σ.1, Σ.2))).
{ now eapply PCUICExpandLetsCorrectness.trans_wf. }
{ clear -HΣ typing. now eapply PCUICClosedTyp.subject_closed in typing. }
{ clear -HΣ typing''. now eapply PCUICClosedTyp.subject_closed in typing''. }
cbn. 2:cbn. 3:cbn. exact X0.
now eapply (PCUICExpandLetsCorrectness.trans_axiom_free Σ).
pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing).
pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing'').
rewrite PCUICExpandLetsCorrectness.trans_mkApps in X1. eapply X1.
cbn. eapply (PCUICExpandLetsCorrectness.trans_firstorder_ind Σ); eauto.
Qed.
Expand Down
5 changes: 5 additions & 0 deletions utils/theories/MCList.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1475,3 +1475,8 @@ Proof.
{ move => [->|[n H]]; [ exists 0 | exists (S n) ];
rewrite ?skipn_0 ?skipn_S => //=. }
Qed.

Lemma nth_error_firstn A n m (l:list A) x : nth_error (firstn n l) m = Some x -> nth_error l m = Some x.
Proof.
revert n l. induction m; intros n l H; destruct n, l; cbn in *; try solve [inversion H]; eauto.
Qed.

0 comments on commit 6c0bcf5

Please sign in to comment.