@@ -35,6 +35,9 @@ Hint Resolve assumption_context_subst
3535 assumption_context_map_vass
3636 PCUICSigmaCalculus.context_assumptions_context : hints.
3737
38+ #[local]
39+ Arguments monad_utils.bind /.
40+
3841(** Soundness (In the paper: Theorem 1) *)
3942Theorem expr_to_term_sound (n : nat) (ρ : env val) Σ1 Σ2
4043 (e1 e2 : expr) (v : val) :
9295 assert (ty_expr_env_ok (exprs ρ # [e ~> of_val_i v0]) 0 e1_2).
9396 { change (exprs ρ # [e ~> of_val_i v0]) with (exprs (ρ # [e ~> v0])).
9497 eapply eval_ty_expr_env_ok; eauto with hints. simpl.
95- replace #|ρ| with (#|exprs ρ|) by apply map_length .
98+ replace #|ρ| with (#|exprs ρ|) by apply length_map .
9699 eapply subst_env_iclosed_n_inv with (n := 1); eauto with hints. }
97100
98101 assert (val_ok Σ1 v0) by (eapply eval_val_ok; eauto with hints).
@@ -132,7 +135,7 @@ Proof.
132135 now rewrite Hres. }
133136 rewrite Hc.
134137 eapply IHn; eauto with hints.
135- repeat rewrite map_length . unfold PcbvCurr.cstr_arity. propify. lia.
138+ repeat rewrite length_map . unfold PcbvCurr.cstr_arity. propify. lia.
136139 * destruct c.
137140 ** (* the closure corresponds to lambda *)
138141 simpl in *. rename e0 into n0.
@@ -297,7 +300,7 @@ Proof.
297300 destruct (resolve_inductive _ _) eqn:HresI; tryfalse.
298301 destruct (lookup_with_ind _ _) eqn:Hfind_i; tryfalse.
299302 destruct p as [nparams cs]. destruct p0 as [i ci]. simpl in *.
300- rewrite map_length .
303+ rewrite length_map .
301304 destruct_match eqn:Hnparams; tryfalse.
302305 assert (HresC: resolve_constr Σ1 i0 e = Some (nparams,i, ci)).
303306 { unfold resolve_constr. rewrite HresI. rewrite Hfind_i. reflexivity. }
@@ -327,7 +330,7 @@ Proof.
327330 destruct H2 as [Hdctor?].
328331 eapply PcbvCurr.eval_iota; eauto.
329332 * now eapply map_nth_error.
330- * cbn. rewrite map_length . unfold PcbvCurr.cstr_arity. propify. lia.
333+ * cbn. rewrite length_map . unfold PcbvCurr.cstr_arity. propify. lia.
331334 * cbn.
332335 unfold etrans_branch.
333336 unfold fun_prod,id; cbn.
@@ -340,8 +343,8 @@ Proof.
340343 rewrite Heq; cbn.
341344 assert (Hvass : forall xs, context_assumptions (map (fun '(nm, ty) => vass (aRelevant (nNamed (TCString.of_string nm))) ty) xs) = #|xs|).
342345 { intros; rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
343- now rewrite map_length . }
344- rewrite Hvass. rewrite combine_length, map_length .
346+ now rewrite length_map . }
347+ rewrite Hvass. rewrite length_combine, length_map .
345348 lia.
346349 * unfold iota_red in *. simpl in *.
347350 unfold expand_lets,expand_lets_k,inst_case_branch_context,inst_case_context; cbn.
@@ -355,7 +358,7 @@ Proof.
355358 inversion Hnth_eq; subst; clear Hnth_eq.
356359 assert (Heq : (#|pVars v2.1| =? #|remove_proj c|)%nat) by (propify; lia).
357360 rewrite Heq; cbn.
358- repeat rewrite map_length . rewrite combine_length,map_length .
361+ repeat rewrite length_map . rewrite length_combine,length_map .
359362 replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
360363 rewrite <- map_skipn.
361364 rewrite <- map_rev.
@@ -398,12 +401,12 @@ Proof.
398401 specialize (find_forallb_map _ Hfnd HH) as Hclosed_t2; cbn in Hclosed_t2.
399402
400403 erewrite PCUICInstConv.subst_id with (s := rev (_)); eauto.
401- 2: { rewrite rev_length . rewrite to_extended_list_k_length. rewrite Hvass_eq.
402- subst g. repeat rewrite map_length . rewrite combine_length .
404+ 2: { rewrite length_rev . rewrite to_extended_list_k_length. rewrite Hvass_eq.
405+ subst g. repeat rewrite length_map . rewrite length_combine .
403406 replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
404407 rewrite PCUICSigmaCalculus.context_assumptions_context.
405408 * rewrite subst_context_length.
406- repeat rewrite map_length . rewrite combine_length,map_length .
409+ repeat rewrite length_map . rewrite length_combine,length_map .
407410 replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
408411 replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
409412 rewrite <- Hf.
@@ -416,11 +419,11 @@ Proof.
416419 (subst_context (rev (map (fun x : type => T⟦ subst_env_i_ty 0 (exprs ρ) x ⟧) l0)) 0 g)) = #|pVars v2.1|).
417420 { rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
418421 rewrite subst_context_length. subst g.
419- repeat rewrite map_length . rewrite combine_length .
422+ repeat rewrite length_map . rewrite length_combine .
420423 replace #|remove_proj c| with #|pVars v2.1| by (propify; lia).
421424 now replace (min #|pVars v2.1| #|pVars v2.1|) with #|pVars v2.1| by lia.
422425 }
423- assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite skipn_length ; lia).
426+ assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite length_skipn ; lia).
424427
425428 rewrite Hvass_eq1.
426429
@@ -442,7 +445,7 @@ Proof.
442445 rewrite <- map_map with (g := (expr_to_term Σ1) ∘ of_val_i)
443446 (f := snd).
444447 rewrite map_combine_snd. now subst.
445- now repeat rewrite rev_length . }
448+ now repeat rewrite length_rev . }
446449 rewrite Hmap. subst h te3.
447450 replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
448451 apply Nat.eqb_eq in Hnparams.
@@ -455,9 +458,9 @@ Proof.
455458 rewrite map_app.
456459 remember (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) as l_rev.
457460 assert (Hlrev : #|pVars v2.1| = #|exprs l_rev|).
458- { subst. rewrite map_length .
459- rewrite rev_length . rewrite combine_length .
460- rewrite skipn_length ; lia. }
461+ { subst. rewrite length_map .
462+ rewrite length_rev . rewrite length_combine .
463+ rewrite length_skipn ; lia. }
461464 rewrite Hlrev.
462465 symmetry. eapply subst_env_swap_app with (n := 0);
463466 eauto with hints.
@@ -471,55 +474,55 @@ Proof.
471474 eapply subst_env_iclosed_0; eauto with hints.
472475 remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
473476 assert (Hlen : #|l_comb| = #|pVars v2.1|).
474- { subst. rewrite combine_length . rewrite map_length .
475- repeat rewrite rev_length . rewrite skipn_length ; lia. }
477+ { subst. rewrite length_combine . rewrite length_map .
478+ repeat rewrite length_rev . rewrite length_skipn ; lia. }
476479 rewrite <- Hlen.
477480 eapply ty_expr_env_ok_subst_env with (k := 0).
478481 assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) = l_comb).
479482 { subst. repeat rewrite map_rev. rewrite combine_rev.
480483 apply f_equal. now rewrite map_combine_snd_funprod.
481- rewrite map_length . rewrite skipn_length ; lia. }
484+ rewrite length_map . rewrite length_skipn ; lia. }
482485 rewrite <- Hcomb. rewrite <- map_app.
483486 eapply eval_ty_expr_env_ok; eauto with hints.
484- rewrite app_length .
487+ rewrite length_app .
485488 replace (#|rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))|) with #|pVars v2.1| by
486- (rewrite rev_length, combine_length, skipn_length ; lia).
487- replace #|ρ| with #|exprs ρ| by apply map_length . eauto with hints.
489+ (rewrite length_rev, length_combine, length_skipn ; lia).
490+ replace #|ρ| with #|exprs ρ| by apply length_map . eauto with hints.
488491
489492 eapply closed_exprs; eauto.
490493
491494 eapply All_snd_combine with (p := iclosed_n 0); eauto with hints.
492495 apply All_map. apply All_rev.
493496 eapply All_expr_iclosed_of_val; eauto using All_skipn.
494497
495- rewrite combine_length . rewrite map_length .
496- repeat rewrite rev_length . rewrite skipn_length by lia.
498+ rewrite length_combine . rewrite length_map .
499+ repeat rewrite length_rev . rewrite length_skipn by lia.
497500 replace (min #|pVars v2.1| (#|l2| - ind_npars mib)) with #|pVars v2.1| by lia.
498501 eauto with hints.
499502
500503 ** rewrite <- combine_rev by auto.
501504 rewrite map_combine_snd_funprod.
502505 remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
503506 assert (Hlen : #|l_comb| = #|pVars v2.1|).
504- { subst. rewrite combine_length . rewrite map_length .
505- repeat rewrite rev_length . rewrite skipn_length ; lia. }
507+ { subst. rewrite length_combine . rewrite length_map .
508+ repeat rewrite length_rev . rewrite length_skipn ; lia. }
506509 rewrite <- Hlen.
507510 eapply ty_expr_env_ok_subst_env with (k := 0).
508511 remember (ind_npars mib) as nparams.
509512 assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn nparams l2))) = l_comb).
510513 { subst. repeat rewrite map_rev. rewrite combine_rev.
511514 apply f_equal. now rewrite map_combine_snd_funprod.
512- rewrite map_length . rewrite skipn_length ; lia. }
515+ rewrite length_map . rewrite length_skipn ; lia. }
513516 rewrite <- Hcomb. rewrite <- map_app.
514517 subst nparams. eapply eval_ty_expr_env_ok; eauto with hints.
515- rewrite app_length .
518+ rewrite length_app .
516519 replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
517- (rewrite rev_length, combine_length, skipn_length ; lia).
518- replace #|ρ| with #|exprs ρ| by apply map_length . eauto with hints.
520+ (rewrite length_rev, length_combine, length_skipn ; lia).
521+ replace #|ρ| with #|exprs ρ| by apply length_map . eauto with hints.
519522 eapply closed_exprs; eauto.
520- ** rewrite map_length .
523+ ** rewrite length_map .
521524 replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
522- (rewrite rev_length, combine_length, skipn_length ; lia).
525+ (rewrite length_rev, length_combine, length_skipn ; lia).
523526 eauto with hints.
524527 ** apply All_map. subst.
525528 apply All_rev. unfold compose. simpl.
0 commit comments