From a583e1d0d45b48b73c4c46c4bb6f8e58cfd5386b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 23 Feb 2016 18:59:50 -0500 Subject: [PATCH] Fancier set simplification --- Frap.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/Frap.v b/Frap.v index 6cf6b39..96b1d87 100644 --- a/Frap.v +++ b/Frap.v @@ -43,6 +43,34 @@ Ltac invert0 e := invert e; fail. Ltac invert1 e := invert0 e || (invert e; []). Ltac invert2 e := invert1 e || (invert e; [|]). +Ltac maps_neq := + match goal with + | [ H : ?m1 = ?m2 |- _ ] => + let rec recur E := + match E with + | ?E' $+ (?k, _) => + (apply (f_equal (fun m => m $? k)) in H; simpl in *; autorewrite with core in *; simpl in *; congruence) + || recur E' + end in + recur m1 || recur m2 +end. + +Ltac fancy_neq := + repeat match goal with + | _ => maps_neq + | [ H : _ = _ |- _ ] => invert H + end. + +Ltac removeDups := + match goal with + | [ |- context[constant ?ls] ] => + someMatch ls; + erewrite (@removeDups_ok _ ls) + by repeat (apply RdNil + || (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ]) + || (apply RdDup; [ simpl; intuition congruence | ])) + end. + Ltac simplify := repeat (unifyTails; pose proof I); repeat match goal with | [ H : True |- _ ] => clear H