From a48d85c84c11422339ae610b6e9a7e75b5188f57 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 17 Mar 2018 19:35:43 -0400
Subject: [PATCH] Improve robustness of set simplification

---
 FrapWithoutSets.v | 12 ++++++++++--
 Sets.v            | 12 ++++++++++--
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index 01e29b3..fdad783 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -159,8 +159,16 @@ Ltac removeDups :=
 
 Ltac doSubtract :=
   match goal with
-  | [ |- context[constant ?ls \setminus constant ?ls0] ] =>
-    erewrite (@doSubtract_ok _ ls ls0)
+  | [ |- context[@minus ?A (@constant ?A1 ?ls) (@constant ?A2 ?ls0)] ] =>
+    match A with
+    | A1 => idtac
+    | _ => change (@constant A1 ls) with (@constant A ls)
+    end;
+    match A with
+    | A2 => idtac
+    | _ => change (@constant A2 ls0) with (@constant A ls0)
+    end;
+    erewrite (@doSubtract_ok A ls ls0)
       by repeat (apply DsNil
                  || (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
                  || (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
diff --git a/Sets.v b/Sets.v
index 447751f..8a53bef 100644
--- a/Sets.v
+++ b/Sets.v
@@ -258,8 +258,16 @@ Ltac fancy_neq :=
 
 Ltac doSubtract :=
   match goal with
-  | [ |- context[constant ?ls \setminus constant ?ls0] ] =>
-    erewrite (@doSubtract_ok _ ls ls0)
+  | [ |- context[@minus ?A (@constant ?A1 ?ls) (@constant ?A2 ?ls0)] ] =>
+    match A with
+    | A1 => idtac
+    | _ => change (@constant A1 ls) with (@constant A ls)
+    end;
+    match A with
+    | A2 => idtac
+    | _ => change (@constant A2 ls0) with (@constant A ls0)
+    end;
+    erewrite (@doSubtract_ok A ls ls0)
       by repeat (apply DsNil
                  || (apply DsKeep; [ simpl; intuition (congruence || fancy_neq) | ])
                  || (apply DsDrop; [ simpl; intuition congruence | ]))