Add FMap{Flip,N,Z}

Also make sure to remove stupid hints from core db, to work around
COQBUG(https://github.com/coq/coq/issues/16133)

_CoqProject

@@ -315,6 +315,7 @@ src/Util/ErrorT/Show.v
 src/Util/FSets/FMapBool.v
 src/Util/FSets/FMapEmpty.v
 src/Util/FSets/FMapFacts.v
+src/Util/FSets/FMapFlip.v
 src/Util/FSets/FMapInterface.v
 src/Util/FSets/FMapIso.v
 src/Util/FSets/FMapN.v
@@ -324,6 +325,7 @@ src/Util/FSets/FMapSect.v
 src/Util/FSets/FMapSum.v
 src/Util/FSets/FMapTrie.v
 src/Util/FSets/FMapUnit.v
+src/Util/FSets/FMapZ.v
 src/Util/FSets/FMapTrie/Shape.v
 src/Util/ListUtil/CombineExtend.v
 src/Util/ListUtil/Concat.v

src/Bedrock/Everything.v

@@ -263,6 +263,7 @@ Crypto.Util.ErrorT.Show
 Crypto.Util.FSets.FMapBool
 Crypto.Util.FSets.FMapEmpty
 Crypto.Util.FSets.FMapFacts
+Crypto.Util.FSets.FMapFlip
 Crypto.Util.FSets.FMapInterface
 Crypto.Util.FSets.FMapIso
 Crypto.Util.FSets.FMapN
@@ -273,6 +274,7 @@ Crypto.Util.FSets.FMapSum
 Crypto.Util.FSets.FMapTrie
 Crypto.Util.FSets.FMapTrie.Shape
 Crypto.Util.FSets.FMapUnit
+Crypto.Util.FSets.FMapZ
 Crypto.Util.Factorize
 Crypto.Util.FixCoqMistakes
 Crypto.Util.FsatzAutoLemmas

src/Everything.v

@@ -186,6 +186,7 @@ Crypto.Util.ErrorT.Show
 Crypto.Util.FSets.FMapBool
 Crypto.Util.FSets.FMapEmpty
 Crypto.Util.FSets.FMapFacts
+Crypto.Util.FSets.FMapFlip
 Crypto.Util.FSets.FMapInterface
 Crypto.Util.FSets.FMapIso
 Crypto.Util.FSets.FMapN
@@ -196,6 +197,7 @@ Crypto.Util.FSets.FMapSum
 Crypto.Util.FSets.FMapTrie
 Crypto.Util.FSets.FMapTrie.Shape
 Crypto.Util.FSets.FMapUnit
+Crypto.Util.FSets.FMapZ
 Crypto.Util.Factorize
 Crypto.Util.FixCoqMistakes
 Crypto.Util.FsatzAutoLemmas

src/Util/FSets/FMapFlip.v

@@ -0,0 +1,214 @@
+Require Import Coq.Bool.Bool.
+Require Import Coq.Lists.List.
+Require Import Coq.Structures.Equalities.
+Require Import Coq.Structures.OrderedType.
+Require Import Coq.Structures.Orders.
+Require Import Coq.Structures.OrdersEx.
+Require Import Coq.FSets.FMapInterface.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.SetoidList.
+Require Import Crypto.Util.ListUtil.SetoidListRev.
+Require Import Crypto.Util.Compose.
+Require Import Crypto.Util.Logic.Forall.
+Require Import Crypto.Util.Logic.Exists.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Structures.Equalities.
+Require Import Crypto.Util.Structures.Orders.
+Require Import Crypto.Util.Structures.Orders.Flip.
+Require Import Crypto.Util.FSets.FMapInterface.
+Require Import Crypto.Util.Sorting.Sorted.Proper.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SpecializeUnderBindersBy.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SetoidSubst.
+
+Local Set Implicit Arguments.
+(* TODO: move to global settings *)
+Local Set Keyed Unification.
+
+Module FlipWSfun (E : DecidableTypeOrig) (W' : WSfun E) <: WSfun E.
+  Module E' := E <+ UpdateEq.
+  Global Remove Hints E'.eq_refl E'.eq_sym E'.eq_trans : core.
+  Local Hint Resolve E'.eq_refl E'.eq_sym E'.eq_trans : core.
+
+  Local Instance W'_eq_key_equiv elt : Equivalence (@W'.eq_key elt) | 10. split; cbv; eauto. Qed.
+  Local Instance W'_eq_key_elt_equiv elt : Equivalence (@W'.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
+
+  Definition key := W'.key.
+  Definition t := W'.t.
+  Definition empty := W'.empty.
+  Definition is_empty := W'.is_empty.
+  Definition add := W'.add.
+  Definition find := W'.find.
+  Definition remove := W'.remove.
+  Definition mem := W'.mem.
+  Definition map := W'.map.
+  Definition mapi := W'.mapi.
+  Definition map2 := W'.map2.
+  Definition cardinal := W'.cardinal.
+  Definition equal := W'.equal.
+  Definition MapsTo := W'.MapsTo.
+  Definition In := W'.In.
+  Definition eq_key := W'.eq_key.
+  Definition eq_key_elt := W'.eq_key_elt.
+  Definition MapsTo_1 := W'.MapsTo_1.
+  Definition mem_1 := W'.mem_1.
+  Definition mem_2 := W'.mem_2.
+  Definition empty_1 := W'.empty_1.
+  Definition is_empty_1 := W'.is_empty_1.
+  Definition is_empty_2 := W'.is_empty_2.
+  Definition add_1 := W'.add_1.
+  Definition add_2 := W'.add_2.
+  Definition add_3 := W'.add_3.
+  Definition remove_1 := W'.remove_1.
+  Definition remove_2 := W'.remove_2.
+  Definition remove_3 := W'.remove_3.
+  Definition find_1 := W'.find_1.
+  Definition find_2 := W'.find_2.
+  Definition Empty := W'.Empty.
+  Definition Equal := W'.Equal.
+  Definition Equiv := W'.Equiv.
+  Definition Equivb := W'.Equivb.
+  Definition equal_1 := W'.equal_1.
+  Definition equal_2 := W'.equal_2.
+  Definition map_1 := W'.map_1.
+  Definition map_2 := W'.map_2.
+  Definition mapi_1 := W'.mapi_1.
+  Definition mapi_2 := W'.mapi_2.
+  Definition map2_1 := W'.map2_1.
+  Definition map2_2 := W'.map2_2.
+
+  Definition elements elt (v : t elt) : list (key * elt)
+    := List.rev_append (W'.elements v) nil.
+  Definition fold elt A (f : key -> elt -> A -> A) (m : t elt) (a : A) : A
+    := W'.fold (fun k v acc a => acc (f k v a)) m id a.
+
+  Section Spec.
+    Variable elt : Type.
+    Variable m m' m'' : t elt.
+    Variable x y z : key.
+    Variable e e' : elt.
+
+    Lemma elements_1 :
+      MapsTo x e m -> InA (@eq_key_elt _) (x,e) (elements m).
+    Proof using Type.
+      clear; cbv [elements]; rewrite <- rev_alt, InA_rev.
+      apply W'.elements_1.
+    Qed.
+    Lemma elements_2 :
+      InA (@eq_key_elt _) (x,e) (elements m) -> MapsTo x e m.
+    Proof using Type.
+      clear; cbv [elements]; rewrite <- rev_alt, InA_rev.
+      apply W'.elements_2.
+    Qed.
+    Lemma elements_3w : NoDupA (@eq_key _) (elements m).
+    Proof using Type.
+      clear; cbv [elements]; rewrite <- rev_alt.
+      apply NoDupA_rev; try exact _.
+      apply W'.elements_3w.
+    Qed.
+    Lemma cardinal_1 : cardinal m = length (elements m).
+    Proof using Type.
+      clear; cbv [elements]; rewrite <- rev_alt, rev_length.
+      apply W'.cardinal_1.
+    Qed.
+    Lemma fold_1 :
+      forall (A : Type) (i : A) (f : key -> elt -> A -> A),
+        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
+    Proof using Type.
+      clear; cbv [fold elements]; intros; rewrite <- rev_alt, W'.fold_1, fold_left_rev_higher_order.
+      reflexivity.
+    Qed.
+  End Spec.
+End FlipWSfun.
+
+Module FlipWeakMap (W' : WS) <: WS.
+  Module E := W'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
+  Include FlipWSfun W'.E W'.
+End FlipWeakMap.
+
+Module FlipUsualWeakMap (W' : UsualWS) <: UsualWS := FlipWeakMap W'.
+
+Module FlipSfun (E' : OrderedTypeOrig) (W' : Sfun E').
+  Include FlipWSfun E' W'.
+  Section elt.
+    Variable elt:Type.
+    Definition lt_key (p p':key*elt) := flip E'.lt (fst p) (fst p').
+
+    Lemma elements_3 m : sort lt_key (elements m).
+    Proof using Type.
+      cbv [elements lt_key].
+      rewrite <- rev_alt, SortA_rev_iff.
+      apply W'.elements_3.
+    Qed.
+  End elt.
+End FlipSfun.
+
+Module FlipUsualMap (S' : UsualS) <: UsualS.
+  Module E <: UsualOrderedTypeOrig := FlipUsualOrderedTypeOrig S'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
+  Include FlipSfun S'.E S'.
+End FlipUsualMap.
+
+Module FlipMap (S' : S) <: S.
+  Module E <: OrderedTypeOrig := FlipOrderedTypeOrig S'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
+  Include FlipSfun S'.E S'.
+End FlipMap.
+
+Module FlipSord (S' : Sord) <: Sord.
+  Module Data <: OrderedTypeOrig := FlipOrderedTypeOrig S'.Data.
+  Module MapS <: S := FlipMap S'.MapS.
+  Import MapS.
+
+  Definition t := S'.t.
+  Definition eq := S'.eq.
+  Definition lt := flip S'.lt.
+  Definition eq_refl := S'.eq_refl.
+  Definition eq_sym := S'.eq_sym.
+  Definition eq_trans := S'.eq_trans.
+  Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
+  Proof. cbv [lt flip]; intros; eapply S'.lt_trans; eassumption. Qed.
+  Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
+  Proof. cbv [lt flip]; intros * H H'; apply S'.lt_not_eq in H; apply H, S'.eq_sym, H'. Qed.
+
+  Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.
+
+  Lemma cmp_iff : forall e e', cmp e e' = flip S'.cmp e e'.
+  Proof.
+    cbv [cmp flip S'.cmp].
+    intros e e'.
+    destruct Data.compare, S'.Data.compare; try reflexivity.
+    all: cbv [flip] in *.
+    all: match goal with
+         | [ H : _ |- _ ] => apply S'.Data.lt_not_eq in H; []
+         end.
+    all: try now exfalso; eauto using S'.Data.eq_sym.
+  Qed.
+
+  Lemma compare : forall m1 m2, Compare lt eq m1 m2.
+  Proof.
+    intros m1 m2.
+    destruct (S'.compare m2 m1).
+    all: constructor; (idtac + apply S'.eq_sym); assumption.
+  Defined.
+
+  Lemma eq_iff : forall m m', Equivb cmp m m' <-> eq m m'.
+  Proof.
+    intros m m'; cbv [eq].
+    rewrite (conj (@eq_sym m m') (@eq_sym m' m) : iff _ _).
+    rewrite <- (conj (@S'.eq_1 m' m) (@S'.eq_2 m' m) : iff _ _).
+    cbv [Equivb S'.MapS.Equivb S'.MapS.Equiv Cmp eq flip] in *.
+    firstorder; first [ rewrite cmp_iff | setoid_rewrite <- cmp_iff ]; cbv [flip].
+    all: eauto.
+  Qed.
+
+  Lemma eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
+  Proof. intros *; apply eq_iff. Qed.
+  Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
+  Proof. intros *; apply eq_iff. Qed.
+End FlipSord.

src/Util/FSets/FMapN.v

@@ -5,58 +5,15 @@ Require Import Coq.Structures.OrderedType.
 Require Import Coq.FSets.FMapInterface.
 Require Import Coq.FSets.FMapPositive.
 Require Import Coq.NArith.NArith.
+Require Import Crypto.Util.FSets.FMapInterface.
 Require Import Crypto.Util.FSets.FMapIso.
+Require Import Crypto.Util.FSets.FMapOption.
 Require Import Crypto.Util.Structures.Equalities.Iso.
 Require Import Crypto.Util.Structures.Orders.Iso.
+Require Import Crypto.Util.Structures.OrdersEx.
 
 Local Set Implicit Arguments.
 
-(* TODO: Swap out for the version in Util/Structures/OrdersEx.v, and profile to see if there are any perf implications *)
-Module NIsoPositive <: IsoOrderedTypeOrig PositiveMap.E.
-  Definition t := N.
-  Definition eq : t -> t -> Prop := eq.
-  Definition eq_equiv : Equivalence eq := _.
-  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y} := N.eq_dec.
-  Definition to_ : t -> PositiveMap.E.t := N.succ_pos.
-  Definition of_ : PositiveMap.E.t -> t := Pos.pred_N.
-  Lemma Proper_to_ : Proper (eq ==> PositiveMap.E.eq) to_.
-  Proof. cbv [eq]; repeat intro; subst; reflexivity. Qed.
-  Lemma Proper_of_ : Proper (PositiveMap.E.eq ==> eq) of_.
-  Proof. cbv [PositiveMap.E.eq]; repeat intro; subst; reflexivity. Qed.
-  Lemma of_to : forall x : t, eq (of_ (to_ x)) x.
-  Proof. cbv [eq of_ to_]; intros; now rewrite N.pos_pred_succ. Qed.
-  Lemma to_of : forall x : PositiveMap.E.t, PositiveMap.E.eq (to_ (of_ x)) x.
-  Proof.
-    intro x.
-    cut (N.pos (to_ (of_ x)) = N.pos x); [ congruence | ].
-    cbv [PositiveMap.E.eq of_ to_].
-    rewrite N.pos_pred_spec, N.succ_pos_spec.
-    lia.
-  Qed.
-  Definition eq_refl : Reflexive eq := _.
-  Definition eq_sym : Symmetric eq := _.
-  Definition eq_trans : Transitive eq := _.
-  Definition lt (x y : t) : Prop := PositiveMap.E.lt (to_ x) (to_ y).
-  Global Instance lt_trans : Transitive lt | 100.
-  Proof. repeat intro; eapply PositiveMap.E.lt_trans; eassumption. Qed.
-  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof.
-    cbv [lt eq]; intros * H ?; apply PositiveMap.E.lt_not_eq in H; subst.
-    cbv [PositiveMap.E.eq] in *; congruence.
-  Qed.
-  Definition compare (x y : t) : Compare lt eq x y.
-  Proof.
-    refine match PositiveMap.E.compare (to_ x) (to_ y) with
-           | LT pf => LT _
-           | EQ pf => EQ (eq_trans (eq_sym (of_to _)) (eq_trans (f_equal _ pf) (of_to _)))
-           | GT pf => GT _
-           end;
-      cbv [lt eq PositiveMap.E.eq] in *; try assumption.
-  Defined.
-  Global Instance Proper_to_lt : Proper (lt ==> PositiveMap.E.lt) to_ | 10.
-  Proof. cbv [lt Proper]; repeat intro; assumption. Qed.
-  Global Instance Proper_of_lt : Proper (PositiveMap.E.lt ==> lt) of_ | 10.
-  Proof. cbv [lt Proper]; repeat intro; rewrite !to_of; assumption. Qed.
-End NIsoPositive.
+Module OptionPositiveMap <: UsualS := OptionUsualMap PositiveMap.
 
-Module NMap <: S := IsoS PositiveMap NIsoPositive.
+Module NMap <: UsualS := IsoS OptionPositiveMap NIsoOptionPositiveOrig.

src/Util/FSets/FMapZ.v

@@ -0,0 +1,22 @@
+Require Import Coq.micromega.Lia.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Lists.List.
+Require Import Coq.Structures.OrderedType.
+Require Import Coq.FSets.FMapInterface.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.FSets.FMapInterface.
+Require Import Crypto.Util.FSets.FMapIso.
+Require Import Crypto.Util.FSets.FMapFlip.
+Require Import Crypto.Util.FSets.FMapSum.
+Require Import Crypto.Util.FSets.FMapN.
+Require Import Crypto.Util.Structures.Equalities.Iso.
+Require Import Crypto.Util.Structures.Orders.Iso.
+Require Import Crypto.Util.Structures.OrdersEx.
+
+Local Set Implicit Arguments.
+
+Module NegativeMap <: UsualS := FlipUsualMap PositiveMap.
+Module SumNegNMap <: UsualS := SumUsualMap NegativeMap NMap.
+
+Module ZMap <: UsualS := IsoS SumNegNMap ZIsoSumNegNOrig.