Move NatSet-related lemma to the appropriate file

coq/AffineValidation.v

@@ -465,25 +465,6 @@ Proof.
     lra.
 Qed.
 
-Lemma subset_union s1 s2 s3:
-  NatSet.Subset (s1 -- s3) s2 ->
-  NatSet.Subset s1 (NatSet.union s2 s3).
-Proof.
-  intros diff.
-  hnf in diff |-*.
-  intros a Hin1.
-  specialize (diff a).
-  destruct (NatSet.mem a s3) eqn: Hmem.
-  - rewrite NatSet.mem_spec in Hmem.
-    rewrite NatSet.union_spec.
-    now right.
-  - apply not_in_not_mem in Hmem.
-    rewrite NatSet.union_spec.
-    left.
-    apply diff.
-    set_tac.
-Qed.
-
 Definition affine_dVars_range_valid (dVars: NatSet.t) (E: env) (A: analysisResult) noise exprAfs map1: Prop :=
   forall v, NatSet.In v dVars ->
        exists af vR iv err,
@@ -1086,7 +1067,7 @@ Proof.
           intuition.
           + rewrite usedVars_eq_compat; eauto.
             simpl in varsDisjoint |-*; auto.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + erewrite FloverMapFacts.P.F.find_o; eauto.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
@@ -1156,7 +1137,7 @@ Proof.
           repeat split; auto.
           + rewrite usedVars_eq_compat; eauto.
             simpl.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
             constructor; try rewrite Rabs_R0; simpl; auto; [lra |].
@@ -1302,7 +1283,7 @@ Proof.
           exists (AffineArithQ.plus_aff af1 af2), (perturb (evalBinop Plus vR1 vR2) REAL 0)%R, aiv, aerr.
           intuition; eauto using fresh_monotonic, af_evals_map_extension, AffineArithQ.plus_aff_preserves_fresh.
           + rewrite usedVars_eq_compat; eauto; simpl.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + erewrite FloverMapFacts.P.F.find_o; eauto.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
@@ -1389,7 +1370,7 @@ Proof.
           exists (AffineArithQ.subtract_aff af1 af2), (perturb (evalBinop Sub vR1 vR2) REAL 0)%R, aiv, aerr.
           intuition; eauto using fresh_monotonic, af_evals_map_extension, AffineArithQ.plus_aff_preserves_fresh.
           + rewrite usedVars_eq_compat; eauto; simpl.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + erewrite FloverMapFacts.P.F.find_o; eauto.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
@@ -1492,7 +1473,7 @@ Proof.
           (perturb (evalBinop Mult vR1 vR2) REAL 0)%R, aiv, aerr.
           intuition; eauto using fresh_monotonic, af_evals_map_extension.
           + rewrite usedVars_eq_compat; eauto; simpl.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + erewrite FloverMapFacts.P.F.find_o; eauto.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
@@ -1646,7 +1627,7 @@ Proof.
           (perturb (evalBinop Div vR1 vR2) REAL 0)%R, aiv, aerr.
           repeat split; eauto using fresh_monotonic, af_evals_map_extension.
           + rewrite usedVars_eq_compat; eauto; simpl.
-            now apply subset_union.
+            now apply subset_diff_to_subset_union.
           + erewrite FloverMapFacts.P.F.find_o; eauto.
           + rewrite FloverMapFacts.P.F.add_eq_o; auto.
           + erewrite expr_compare_eq_eval_compat; eauto.
@@ -1924,7 +1905,7 @@ Proof.
         (perturb (evalFma vR1 vR2 vR3) REAL 0)%R, aiv, aerr.
         repeat split; eauto using fresh_monotonic, af_evals_map_extension.
         + rewrite usedVars_eq_compat; eauto; simpl.
-          now apply subset_union.
+          now apply subset_diff_to_subset_union.
         + erewrite FloverMapFacts.P.F.find_o; eauto.
         + rewrite FloverMapFacts.P.F.add_eq_o; auto.
         + erewrite expr_compare_eq_eval_compat; eauto.
@@ -2098,7 +2079,7 @@ Proof.
       exists afS, (perturb vR REAL 0)%R, aiv, aerr.
       intuition.
       * rewrite usedVars_eq_compat; eauto; simpl.
-        now apply subset_union.
+        now apply subset_diff_to_subset_union.
       * erewrite FloverMapFacts.P.F.find_o; eauto.
       * rewrite FloverMapFacts.P.F.add_eq_o; auto.
       * erewrite expr_compare_eq_eval_compat; try exact H0.

coq/Infra/NatSet.v

@@ -70,6 +70,25 @@ Proof.
     destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto.
 Qed.
 
+Lemma subset_diff_to_subset_union s1 s2 s3:
+  NatSet.Subset (s1 -- s3) s2 ->
+  NatSet.Subset s1 (NatSet.union s2 s3).
+Proof.
+  intros diff.
+  hnf in diff |-*.
+  intros a Hin1.
+  specialize (diff a).
+  destruct (NatSet.mem a s3) eqn: Hmem.
+  - rewrite NatSet.mem_spec in Hmem.
+    rewrite NatSet.union_spec.
+    now right.
+  - apply not_in_not_mem in Hmem.
+    rewrite NatSet.union_spec.
+    left.
+    apply diff.
+    apply NatSetProps.Dec.F.diff_3; auto.
+Qed.
+
 Ltac set_bool_to_prop :=
   match goal with
   | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H