From ca0ff639c8783bb1ed1a5063a22ef90719081c24 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 18 Sep 2026 21:46:41 +0200 Subject: [PATCH] Adapt to [big_sepL2_range_Z_l] change. --- rocq-brick-libstdcpp/proof/compare/spec.v | 17 +++++++++++++++++ rocq-brick-libstdcpp/proof/iterator/spec.v | 19 +++++++++++-------- 2 files changed, 28 insertions(+), 8 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/compare/spec.v b/rocq-brick-libstdcpp/proof/compare/spec.v index 7f5e1789..5a30f068 100644 --- a/rocq-brick-libstdcpp/proof/compare/spec.v +++ b/rocq-brick-libstdcpp/proof/compare/spec.v @@ -98,6 +98,7 @@ Section with_cpp. \prepost{q v} this |-> weak_orderingR q v \post{result}[Vptr result] result |-> partial_orderingR 1$m (Some v)). + #[ignore_missing] cpp.spec "std::__cmp_cat::__unspec::__unspec(std::__cmp_cat::__unspec*)" as unspec_ctor from source with ( \this this \arg{p} "" (Vptr p) @@ -109,6 +110,7 @@ Section with_cpp. \pre this |-> unspecR 1$m \post emp). + #[ignore_missing] cpp.spec "std::operator==(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_eq_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -116,6 +118,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Some Eq))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_lt_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -123,6 +126,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Some Lt))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator>(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_gt_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -130,6 +134,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Some Gt))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_cmp_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -137,6 +142,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post{result}[Vptr result] result |-> partial_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_lt_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -144,6 +150,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Lt))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator==(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_eq_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -151,6 +158,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Eq))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator>(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_gt_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -158,6 +166,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Gt))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_cmp_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -165,6 +174,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post{result}[Vptr result] result |-> strong_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator==(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_eq_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -172,6 +182,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Eq))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator>(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_gt_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -179,6 +190,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post[Vbool (bool_decide (lhs_v = Gt))] rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_cmp_unspec from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -186,6 +198,7 @@ Section with_cpp. \pre{q_rhs} rhs |-> unspecR q_rhs \post{result}[Vptr result] result |-> weak_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs). + #[ignore_missing] cpp.spec "std::operator<(std::__cmp_cat::__unspec, std::partial_ordering)" as unspec_lt_partial_ordering from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -193,6 +206,7 @@ Section with_cpp. \prepost{q_rhs rhs_v} rhs |-> partial_orderingR q_rhs rhs_v \post[Vbool (bool_decide (rhs_v = Some Gt))] lhs |-> unspecR q_lhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::partial_ordering)" as unspec_cmp_partial_ordering from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -200,6 +214,7 @@ Section with_cpp. \prepost{q_rhs rhs_v} rhs |-> partial_orderingR q_rhs rhs_v \post{result}[Vptr result] result |-> partial_orderingR 1$m (CompOpp <$> rhs_v) ** lhs |-> unspecR q_lhs). + #[ignore_missing] cpp.spec "std::operator>(std::__cmp_cat::__unspec, std::strong_ordering)" as unspec_gt_strong_ordering from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -207,6 +222,7 @@ Section with_cpp. \prepost{q_rhs rhs_v} rhs |-> strong_orderingR q_rhs rhs_v \post[Vbool (bool_decide (rhs_v = Lt))] lhs |-> unspecR q_lhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::strong_ordering)" as unspec_cmp_strong_ordering from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) @@ -214,6 +230,7 @@ Section with_cpp. \prepost{q_rhs rhs_v} rhs |-> strong_orderingR q_rhs rhs_v \post{result}[Vptr result] result |-> strong_orderingR 1$m (CompOpp rhs_v) ** lhs |-> unspecR q_lhs). + #[ignore_missing] cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::weak_ordering)" as unspec_cmp_weak_ordering from source with ( \arg{lhs} "" (Vptr lhs) \arg{rhs} "" (Vptr rhs) diff --git a/rocq-brick-libstdcpp/proof/iterator/spec.v b/rocq-brick-libstdcpp/proof/iterator/spec.v index 72036bb7..423a70d9 100644 --- a/rocq-brick-libstdcpp/proof/iterator/spec.v +++ b/rocq-brick-libstdcpp/proof/iterator/spec.v @@ -357,9 +357,9 @@ NES.Begin std. iApply (observe with "A"). auto using observe_only_provable_impl, obs_Forall2_big_sepL2. } f_equiv; rewrite !only_provable_True // !left_id; f_equiv. - rewrite big_sepL2_rangeZ_l -Hrng; last first. - { rewrite lengthN_rangeZ. lia. } - apply big_sepL_proper => k y. + rewrite big_sepL2_rangeZ_l -Hrng only_provable_True; last first. + { rewrite lengthN_rangeZ Z2N.id; lia. } + rewrite left_id. apply big_sepL_proper => k y. rewrite lookup_rangeZ => - [_ ->]. by rewrite only_provable_True // left_id. Qed. @@ -531,10 +531,11 @@ NES.Begin std. rewrite o_sub_sub Hi_len. iFrame "#". rewrite [ [| i ≤ j |] ] only_provable_True // left_id. - rewrite !big_sepL2_rangeZ_l //; last first. - { rewrite lengthN_rangeZ. lia. } - rewrite 1!big_opL_fmap. - rewrite (big_opL_rangeZ vs) //. + rewrite !big_sepL2_rangeZ_l 1!big_opL_fmap. + rewrite [ [| lengthZ vs = _ |] ]only_provable_True; last lia. + rewrite left_id. + rewrite (big_opL_rangeZ vs) //. rewrite -bi.sep_assoc. + iSplit. { iPureIntro. rewrite lengthN_rangeZ. lia. } rewrite -big_opL_op. iApply (big_sepL_mono with "SEP") => k x Hx. rewrite only_provable_True // left_id. @@ -551,7 +552,9 @@ NES.Begin std. rewrite length_fmap -lengthZ_correct o_sub_sub. have -> : i + lengthZ vs = j by lia. iFrame "valid". - rewrite !big_sepL2_rangeZ_l // !big_opL_fmap. + rewrite !big_sepL2_rangeZ_l. + rewrite !only_provable_True ?left_id; try lia. + rewrite !big_opL_fmap. rewrite (big_opL_rangeZ vs) //. iCombine "SEP B" as "A". rewrite -big_opL_op.