Skip to content

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection) #837

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
andrew-appel merged 1 commit into from
Sep 22, 2025
Merged

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection) #837

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 10 additions & 9 deletions floyd/Component.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -771,40 +771,41 @@ Proof.
+ rewrite semax_prog.make_tycontext_g_G_None in Heqq by trivial.
rewrite semax_prog.make_tycontext_g_G_None; trivial.
apply find_id_None_iff. apply find_id_None_iff in Heqw. intros N; apply Heqw.
rewrite map_app in *. rewrite HI1 in N. trivial. }
eapply Build_Component; subst; try solve [apply c].
rewrite map_app in *. rewrite HI1 in N. trivial. }
(* after Rocq 9.2, "apply c" automatically tries "apply (Comp_MkInitPred c)"
(before 9.2 it is supposed to try it but is bugged, cf rocq-prover/rocq#21036) *)
eapply Build_Component; subst; try solve [apply c | apply (Comp_MkInitPred c)].
+ rewrite HI1; apply c.
+ rewrite map_app, HI1, <- map_app; apply c.
+ intros. specialize (Comp_G_justified c i _ _ H H0); intros. destruct fd.
- eapply InternalInfo_subsumption. apply AUX2. apply AUX1. apply Comp_ctx_LNR. apply H1.
- auto.
+ apply (Comp_MkInitPred c).
Qed.

(*Together with Lemma Comp_Exports_suboption, this lemma means we can abstract or hide exports*)
Lemma Comp_Exports_sub1 Exports' (HE1: map fst Exports' = map fst Exports)
(HE2: Forall2 funspec_sub (map snd Exports) (map snd Exports')):
@Component Espec V E Imports p Exports' GP G.
Proof.
eapply Build_Component; try apply c.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
eapply Build_Component; try apply c; try apply (Comp_MkInitPred c).
+ rewrite HE1; apply c.
+ intros i phi Hi. rename phi into phi'.
assert (X: exists phi, find_id i Exports = Some phi /\ funspec_sub phi phi').
{ clear - HE1 HE2 Hi. eapply find_funspec_sub; eassumption. }
destruct X as [phi [Phi PHI]].
destruct (Comp_G_Exports c _ _ Phi) as [psi [Psi PSI]].
exists psi; split; [ trivial | eapply funspec_sub_trans; eassumption ].
+ apply (Comp_MkInitPred c).
Qed.

Lemma Comp_Exports_sub2 Exports' (LNR: list_norepet (map fst Exports'))
(HE2: forall i, sub_option (find_id i Exports') (find_id i Exports)):
@Component Espec V E Imports p Exports' GP G.
Proof.
eapply Build_Component; try apply c; trivial.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
eapply Build_Component; try apply c; try apply (Comp_MkInitPred c); trivial.
+ intros i phi' Hi. specialize (HE2 i). rewrite Hi in HE2; simpl in HE2.
apply c; trivial.
+apply (Comp_MkInitPred c).
Qed.

Definition funspecs_sqsub Exp Exp' :=
Expand Down Expand Up @@ -874,11 +875,11 @@ Lemma Comp_Exports_sub Exports' (LNR: list_norepet (map fst Exports'))
(HE2: funspecs_sqsub Exports Exports'):
@Component Espec V E Imports p Exports' GP G.
Proof.
eapply Build_Component; try apply c; trivial.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
eapply Build_Component; try apply c; try apply (Comp_MkInitPred c); trivial.
intros i phi' Hi. destruct (HE2 _ _ Hi) as [phi [H1 H2]].
apply (Comp_G_Exports c) in H1; destruct H1 as [psi [H3 H4]].
exists psi; split; trivial. eapply funspec_sub_trans; eassumption.
apply (Comp_MkInitPred c).
Qed.

End Component.
Expand Down
38 changes: 19 additions & 19 deletions floyd/VSU.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1280,21 +1280,21 @@ Proof.
intros.
destruct v as [G c].
exists G.
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try apply c; auto.
+ intros.
rewrite Forall_forall in H0.
apply find_id_e in E0.
apply H0 in E0.
red in E0.
simpl in E0.
destruct (find_id i Exports) eqn:?H; try contradiction.
apply (Comp_G_Exports c) in H1.
destruct H1 as [phi' [? ?]].
exists phi'.
split; auto.
eapply funspec_sub_trans; eauto.
+ intros. apply (Comp_MkInitPred c); auto.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try first [apply c | apply (Comp_MkInitPred c)]; auto.
intros.
rewrite Forall_forall in H0.
apply find_id_e in E0.
apply H0 in E0.
red in E0.
simpl in E0.
destruct (find_id i Exports) eqn:?H; try contradiction.
apply (Comp_G_Exports c) in H1.
destruct H1 as [phi' [? ?]].

exists phi'.
split; auto.
eapply funspec_sub_trans; eauto.
Qed.

Ltac prove_restrictExports :=
Expand All @@ -1319,13 +1319,13 @@ Proof.
intros.
destruct v as [G c].
exists G.
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try apply c; auto.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try first [apply c | apply (Comp_MkInitPred c)]; auto.
+ rewrite H. apply c.
+ intros. destruct (find_funspec_sub Exports' Exports H H0 _ _ E0) as [psi [Psi PSI]].
apply (Comp_G_Exports c) in Psi.
destruct Psi as [tau [Tau TAU]].
exists tau; split; trivial. eapply funspec_sub_trans; eassumption.
+ apply (Comp_MkInitPred c).
Qed.

Ltac prove_restrictExports2 :=
Expand Down Expand Up @@ -1481,7 +1481,8 @@ destruct v as [G c].
assert (LNR1: list_norepet (map fst (QPvarspecs p) ++ map fst (G ++ Imports'))).
{ rewrite map_app, <- H, <- map_app. apply c. }
exists G.
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try apply c; auto.
(* after Rocq 9.2 the second apply is subsumed by the first, cf rocq-prover/rocq#21036 *)
apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try first [apply c | apply (Comp_MkInitPred c)]; auto.
+ rewrite <- H. apply c.
+ intros.
assert (LNR2: list_norepet (map fst (QPvarspecs p) ++ map fst (Imports' ++ G))).
Expand Down Expand Up @@ -1510,7 +1511,6 @@ apply (@Build_Component _ _ _ _ _ _ _ _ (Comp_prog_OK c)); try apply c; auto.
rewrite Psi. eexists; split. reflexivity. apply (funspec_sub_sub_si _ _ PSI).
* apply find_id_None_iff in Heqq. rewrite H in Heqq. apply find_id_None_iff in Heqq. rewrite Heqq, Heqw.
eexists; split. reflexivity. apply funspec_sub_si_refl.
+ apply (Comp_MkInitPred c).
Qed.

Lemma replace_spec_Forall2_funspec_sub2 p phi: forall (l : funspecs)
Expand Down
Loading