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

Author: SkySkimmer

floyd/Component.v

@@ -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' :=
@@ -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.

floyd/VSU.v

@@ -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 :=
@@ -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 :=
@@ -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))).
@@ -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)