Now reverting hypotheses if substituted variables occur in it.

theories/examples/comparison/mcs_lock.v

@@ -134,13 +134,7 @@ Section spec.
     SPEC {{ R ∗ acquired_node γm γn γe n R ∗ is_lock γm γe R v }}
       release v #n
     {{ RET #(); free_node γm n }}.
-  Proof.
-    iStepsS; last iSmash.
-    iRight.
-    iStepsS; last iSmash.
-    (* need a revert since a detected equality rewrites the context, causing a Mergable instance to be missed *)
-    iReIntro "H6". iSmash.
-  Qed.
+  Proof. iSmash. Qed.
 
   Definition acquired_mutual_exclusion γm γn1 γn2 γe n m R : acquired_node γm γn1 γe n R ∗ acquired_node γm γn2 γe m R ⊢ False
     := verify. (* Cannot do Lemma _ : _ := verify unfortunately. If proper reuse is wanted this should be a Mergable instance *)

theories/examples/wip/logatom/atomic_clhlock.v

@@ -108,7 +108,7 @@ Section spec.
     iStepsS; [iSmash| | iSmash].
     iMod "H5" as (p) "[[Hl >Hp] [_ Hcl]]".
     iReIntro "Hp". rewrite left_id.
-    iMod ("Hcl" with "[Hl H5 H6 H10 H11 H1 H3 H4]") as "HAU"; first (iFrame; iStepsS).
+    iMod ("Hcl" with "[Hl H5 H11 H10 H7 H1 H3 H4]") as "HAU"; first (iFrame; iStepsS).
     iSmash.
   Qed.
 

theories/lib/frac_token.v

@@ -60,7 +60,7 @@ Section fractional_tokenizable.
       split. { apply Qp_div_2. }
       iDestruct "H2" as "[H2 H2']".
       iStepsS.
-    - do 4 iStepS; last lia.
+    - do 4 iStepS.
       apply Qp_lt_sum in H2 as [q ->].
       iExists q.
       iStepS.

theories/steps/introduce_hyp.v

@@ -347,6 +347,98 @@ Section coq_tactics.
 
 End coq_tactics.
 
+
+Fixpoint revert_idents {PROP : bi} (js : list ident) Δ G : option (envs PROP * PROP) :=
+  match js with
+  | [] => Some (Δ, G)
+  | j :: js =>
+    '(Δ', G') ← revert_idents js Δ G;
+    '(p, H) ← envs_lookup j Δ';
+    Some (envs_delete true j p Δ', IntroduceHyp H G')
+  end.
+
+Lemma revert_idents_sound {PROP : bi} (js : list ident) Δ (G : PROP) :
+  match revert_idents js Δ G with
+  | Some (Δ', G') => envs_entails Δ' G'
+  | _ => False
+  end →
+  envs_entails Δ G.
+Proof.
+  rewrite envs_entails_eq.
+  revert Δ G.
+  induction js as [|j js] => //.
+  move => Δ G. cbn.
+  destruct (revert_idents _ _ _) as [[Δ' G']|] eqn:HΔG => //=.
+  destruct (envs_lookup _ _) as [[p P]|] eqn:HjΔ => //=.
+  move => HΔP.
+  apply IHjs. rewrite HΔG.
+  rewrite envs_lookup_sound //.
+  apply bi.wand_elim_r'.
+  rewrite HΔP. unseal_diaframe.
+  by rewrite bi.intuitionistically_if_elim.
+Qed.
+
+(* some ltacs to collect hypotheses which should be reintroduced *)
+Ltac collect_env_occs x Γi acci :=
+  let rec mthd Γ acc :=
+    lazymatch Γ with
+    | Enil => acc
+    | Esnoc ?Γ' ?i ?H =>
+      lazymatch H with
+      | context [x] => 
+        let result := mthd Γ' acc in
+        constr:(i::result)
+      | _ => mthd Γ' acc
+      end
+    end
+  in mthd Γi acci.
+
+Ltac collect_envs_occs x Δ :=
+  let init := constr:(@nil ident) in
+  let Γs := eval cbn in (env_spatial Δ) in
+  let result_s := collect_env_occs x Γs init in
+  let Γp := eval cbn in (env_intuitionistic Δ) in
+  collect_env_occs x Γp result_s.
+
+Ltac my_subst x :=
+  assert_succeeds (subst x);
+  lazymatch goal with
+  | |- envs_entails ?Δ ?G =>
+    let result := collect_envs_occs x Δ in
+    refine (revert_idents_sound result Δ G _); simpl;
+    subst x
+  end.
+
+(* adapted from stdpp's simplify_eq *)
+Tactic Notation "simplify_hyp_eq" :=
+  match goal with
+  | |- ?Htype → ?G => 
+    let H := fresh "H" in
+    intro H;
+    repeat
+    match type of H with
+    | _ ≠ _ => by case H; try clear H
+    | _ = _ → False => by case H; try clear H
+    | ?x = _ => my_subst x
+    | _ = ?x => my_subst x
+    | _ = _ => discriminate H
+    | _ ≡ _ => apply leibniz_equiv in H
+    | ?f _ = ?f _ => apply (inj f) in H
+    | ?f _ _ = ?f _ _ => apply (inj2 f) in H; destruct H
+      (* before [injection] to circumvent bug #2939 in some situations *)
+    | ?f _ = ?f _ => progress injection H as H
+      (* first hyp will be named [H], subsequent hyps will be given fresh names *)
+    | ?f _ _ = ?f _ _ => progress injection H as H
+    | ?f _ _ _ = ?f _ _ _ => progress injection H as H
+    | ?f _ _ _ _ = ?f _ _ _ _ => progress injection H as H
+    | ?f _ _ _ _ _ = ?f _ _ _ _ _ => progress injection H as H
+    | ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ => progress injection H as H
+    | ?x = ?x => clear H
+    | @existT ?A _ _ _ = existT _ _ =>
+       apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (=@{A}))) in H
+    end
+  end.
+
 Ltac simplifySolveSepPureHyp := 
   lazymatch goal with
   | |- ?φ → ?P => 
@@ -356,7 +448,7 @@ Ltac simplifySolveSepPureHyp :=
     | lazymatch φ with
       | True => intros _
       | ?a = ?a => intros _
-      | _ => intros; simplify_eq; subst
+      | _ => simplify_hyp_eq
       end]
   end.
 

theories/steps/introduce_var.v

@@ -35,6 +35,6 @@ End introduce_var.
 
 
 Ltac introduceVarStep :=
-  first
+  first                               (* is this subst necessary? *)
   [apply tac_introduce_vars_teleS; simpl; intros; subst; simpl
   |apply tac_introduce_vars_teleO].
\ No newline at end of file