feat(automation): Solve mask side condition

theories/rust_typing/automation.v

@@ -10,6 +10,40 @@ Set Default Proof Using "Type".
 
 
 (** * Registering extensions to Lithium *)
+(** More automation for sets *)
+Lemma difference_union_subseteq (E F H H': coPset):
+  E ⊆ F →
+  F ∖ H ∪ H' = F →
+  (F ∖ H ∖ E) ∪ H' ∪ E = F.
+Proof.
+  set_unfold.
+  intros ? Hcond x.
+  specialize Hcond with x.
+  split; first intuition.
+  destruct (decide (x ∈ E)); intuition.
+Qed.
+
+Lemma difference_union_subseteq' (E F: coPset):
+  E ⊆ F →
+  F ∖ E ∪ E = F.
+Proof.
+  set_unfold.
+  intros ? x.
+  split; first intuition.
+  destruct (decide (x ∈ E)); intuition.
+Qed.
+
+Lemma difference_union_comm (E E' A B: coPset):
+  A ∪ E' ∪ E = B →
+  A ∪ E ∪ E' = B.
+Proof.
+  set_solver.
+Qed.
+
+Global Hint Resolve difference_union_subseteq' | 30 : ndisj.
+Global Hint Resolve difference_union_subseteq | 50 : ndisj.
+Global Hint Resolve difference_union_comm | 80 : ndisj.
+
 (** More automation for modular arithmetics. *)
 Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 
@@ -905,6 +939,10 @@ Ltac sidecond_hook ::=
       solve_ty_allows
   | |- trait_incl_marker _ =>
       solve_trait_incl
+  | |- _ ## _ =>
+      solve_ndisj
+  | |- _ ∪ _ = _ =>
+      solve_ndisj
   | |- _ =>
       try solve_layout_alg;
       try solve_op_alg;

theories/rust_typing/existentials_na.v

@@ -3,41 +3,6 @@ From refinedrust Require Import uninit int ltype_rules.
 From lrust.lifetime Require Import na_borrow.
 Set Default Proof Using "Type".
 
-Lemma difference_union_subseteq (E F H H': coPset):
-  E ⊆ F →
-  F ∖ H ∪ H' = F →
-  (F ∖ H ∖ E) ∪ H' ∪ E = F.
-Proof.
-  set_unfold.
-
-  intros ? Hcond x.
-  specialize Hcond with x.
-
-  split; first intuition.
-  destruct (decide (x ∈ E)); intuition.
-Qed.
-
-Lemma difference_union_subseteq' (E F: coPset):
-  E ⊆ F →
-  F ∖ E ∪ E = F.
-Proof.
-  set_unfold.
-  intros ? x.
-  split; first intuition.
-  destruct (decide (x ∈ E)); intuition.
-Qed.
-
-Lemma difference_union_comm (E E' A B: coPset):
-  A ∪ E' ∪ E = B →
-  A ∪ E ∪ E' = B.
-Proof.
-  set_solver.
-Qed.
-
-Global Hint Resolve difference_union_subseteq' | 30 : ndisj.
-Global Hint Resolve difference_union_subseteq | 50 : ndisj.
-Global Hint Resolve difference_union_comm | 80 : ndisj.
-
 Record na_ex_inv_def `{!typeGS Σ} (X : Type) (Y : Type) : Type := na_mk_ex_inv_def' {
   na_inv_xr : Type;
   na_inv_xr_inh : Inhabited na_inv_xr;
@@ -1142,7 +1107,6 @@ Section generated_code.
 
       Unshelve. all: sidecond_solver.
       Unshelve. all: sidecond_hammer.
-      Unshelve. all: solve_ndisj.
     Qed.
   End proof.