Skip to main content

🍃 Map.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Import Map.

#[local] Transparent Map.Make.

Module Valid.
  Definition t `{Make.FArgs} : Prop :=
    Compare.Valid.t (fun _True) (fun xx) (Make.Ord.(COMPARABLE.compare)).

  Lemma compare_keys_refl `{Make.FArgs} : t
     k, Make.compare_keys k k = Datatypes.Eq.
  Proof.
    intros Hv k.
    unfold Make.compare_keys.
    erewrite Compare.Valid.refl; auto.
    { exact Hv. }
    { exact I. }
  Qed.

  Lemma compare_keys_Lt_trans `{Make.FArgs} : t k1 k2 k3,
    Make.compare_keys k1 k2 = Datatypes.Lt
    Make.compare_keys k2 k3 = Datatypes.Lt
    Make.compare_keys k1 k3 = Datatypes.Lt.
  Proof.
    intros Hv k1 k2 k3 Hk1k2 Hk2k3.
    unfold Make.compare_keys in ×.
    destruct (Make.Ord.(COMPARABLE.compare) k1 k2 =? 0) eqn:Hz1;
      [discriminate|].
    destruct (Make.Ord.(COMPARABLE.compare) k1 k2 <=? 0) eqn:Hle1;
      [|discriminate].
    destruct (Make.Ord.(COMPARABLE.compare) k2 k3 =? 0) eqn:Hz2;
      [discriminate|].
    destruct (Make.Ord.(COMPARABLE.compare) k2 k3 <=? 0) eqn:Hle2;
      [|discriminate].
    assert (Make.Ord.(COMPARABLE.compare) k1 k3 = -1) as Hneg1.
    { rewrite Z.leb_le in ×.
      rewrite Z.eqb_neq in ×.
      assert ( x, x 0 x 0 x < 0) as Hfact by lia.
      apply (Compare.Valid.trans_lt Hv _ k2); auto;
      apply Compare.Valid.less_neg1; auto.
    }
    rewrite Hneg1; auto.
  Qed.

  Lemma compare_keys_Lt `{Make.FArgs} :
    t
     k k', Make.compare_keys k k' = Datatypes.Lt
    Make.Ord.(COMPARABLE.compare) k k' = -1.
  Proof.
    intros.
    pose proof (Compare.Valid.image H0 k k' I I).
    unfold Make.compare_keys in H1.
    destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
      simpl in *; try discriminate.
    destruct p; tauto.
  Qed.

  Lemma compare_keys_Gt `{Make.FArgs} :
    t
     k k', Make.compare_keys k k' = Datatypes.Gt
    Make.Ord.(COMPARABLE.compare) k k' = 1.
  Proof.
    intros.
    pose proof (Compare.Valid.image H0 k k' I I).
    unfold Make.compare_keys in H1.
    destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
      simpl in *; try discriminate.
    destruct p; tauto.
  Qed.

  Lemma compare_keys_Eq `{Make.FArgs} :
    t
     k k', Make.compare_keys k k' = Datatypes.Eq
    k = k'.
  Proof.
    intros.
    unfold Make.compare_keys in ×.
    destruct Z.eqb eqn:Heq;
      [| destruct Z.leb; discriminate].
    rewrite Z.eqb_eq in Heq.
    simpl in Heq.
    apply (Compare.Valid.zero H0); auto.
  Qed.
End Valid.

Module StrictlySorted.
The list is strictly increasing w.r.t. compare and furthermore bound below by lb. This is an auxiliary definition for strictly_sorted, using lb as an accumulator.
  Fixpoint strictly_sorted_lb {a : Set} (compare : a a int) (lb : a)
    (xs : list a) {struct xs} : Prop :=
    match xs with
    | []True
    | x :: ys
           compare lb x = -1
         strictly_sorted_lb compare x ys
    end.

The list is strictly increasing w.r.t. compare
  Definition strictly_sorted {a : Set} (compare : a a int)
    (xs : list a) : Prop :=
    match xs with
    | []True
    | x :: ysstrictly_sorted_lb compare x ys
    end.

  Lemma strictly_sorted_lb_weaken `{Make.FArgs} : xs x y,
    Valid.t strictly_sorted_lb Make.Ord.(COMPARABLE.compare) y xs
    Make.Ord.(COMPARABLE.compare) x y = -1
    strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs.
  Proof.
    induction xs; intros x y Hv Hss Hxy.
    { exact I. }
    { simpl; split.
      destruct Hss.
      apply (Compare.Valid.trans_lt Hv _ y); auto.
      destruct Hss; auto.
    }
  Qed.

  Lemma strictly_sorted_lb_correct `{Make.FArgs} : xs x,
    Valid.t strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs
     y, In y xs Make.Ord.(COMPARABLE.compare) x y = -1.
  Proof.
    induction xs; intros x Hv Hss y Hin.
    { destruct Hin. }
    { destruct Hin as [Heq|Hin].
      { rewrite Heq in Hss.
        simpl in Hss; tauto.
      }
      { apply IHxs; auto.
        simpl in Hss.
        apply (strictly_sorted_lb_weaken _ _ a); tauto.
      }
    }
  Qed.

  Lemma ss_tail {a : Set} (compare : a a int) (x : a) (xs : list a) :
    strictly_sorted compare (x :: xs) strictly_sorted compare xs.
  Proof.
    intros Hss; simpl in Hss.
    destruct xs.
    { exact I. }
    { simpl in *; tauto. }
  Qed.

  Lemma lb_find_None `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
    strictly_sorted_lb Make.Ord.(COMPARABLE.compare) k (List.map fst m)
    Make.find k m = None.
  Proof.
    destruct m; intros.
    { reflexivity. }
    { simpl.
      destruct p.
      simpl in H0.
      destruct H0.
      unfold Make.compare_keys.
      rewrite H0; reflexivity.
    }
  Qed.

  Definition t `{Make.FArgs} (keys : list Make.key) : Prop :=
    strictly_sorted (Make.Ord.(COMPARABLE.compare)) keys.

  Lemma map_extensional_head `{Make.FArgs} {A : Set} :
    Valid.t
     (m1 m2 : Make.t A) p1 p2,
    t (List.map fst (p1 :: m1))
    t (List.map fst (p2 :: m2))
    ( q, In q (p1 :: m1) In q (p2 :: m2))
    p1 = p2.
  Proof.
    intros.
    assert (In p1 (p2 :: m2)) by hauto.
    destruct H4; auto.
    assert (In p2 (p1 :: m1)) by hauto.
    destruct H5; auto.
    simpl in ×.
    pose (in_map fst _ _ H4).
    pose (in_map fst _ _ H5).
    pose proof (strictly_sorted_lb_correct
      _ _ H0 H1 _ i0).
    pose proof (strictly_sorted_lb_correct
      _ _ H0 H2 _ i).
    epose (Compare.Valid.sym H0).
    rewrite e in H7; auto.
    rewrite H6 in H7; lia.
  Qed.

  Lemma map_extensional_aux `{Make.FArgs} {A : Set} :
    Map.Valid.t
     (m1 m2 : Make.t A) k1 k2,
    strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k1 (List.map fst m1)
    strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k2 (List.map fst m2)
    ( p, In p m1 In p m2)
    m1 = m2.
  Proof.
    intro Hv.
    induction m1; intros m2 k1 k2 Hm1 Hm2 Hin.
    { destruct m2; [reflexivity|].
      pose (Hin p); hauto lq: on rew: off.
    }
    { destruct m2.
      { pose (Hin a); hauto lq: on rew: off. }
      { assert (a = p).
        eapply map_extensional_head; auto.
        { apply Hm1. }
        { apply Hm2. }
        { rewrite H0 in ×.
          simpl in Hm1, Hm2.
          f_equal.
          eapply IHm1.
          { apply Hm1. }
          { apply Hm2. }
          { intro; split; intro.
            { assert (In p0 (p :: m2))
                by (simpl in Hin; sauto lq: on).
              destruct H2; auto.
              rewrite <- H2 in H1.
              destruct Hm1 as [Hp Hm1].
              pose proof (in_map fst _ _ H1).
              epose proof (strictly_sorted_lb_correct
                _ _ Hv Hm1 _ H3).
              rewrite (Compare.Valid.refl Hv) in H4; auto.
              lia.
            }
            { assert (In p0 (p :: m1))
                by (simpl in Hin; sauto lq: on).
              destruct H2; auto.
              rewrite <- H2 in H1.
              destruct Hm2 as [Hp Hm2].
              pose proof (in_map fst _ _ H1).
              epose proof (strictly_sorted_lb_correct
                _ _ Hv Hm2 _ H3).
              rewrite (Compare.Valid.refl Hv) in H4; auto.
              lia.
            }
          }
        }
      }
    }
  Qed.

Two maps are equal when their keys are sorted and contain the same pairs.
  Lemma map_extensional `{Make.FArgs} {A : Set} :
    Valid.t
     m1 m2 : Make.t A,
    t (List.map fst m1)
    t (List.map fst m2)
    ( p, In p m1 In p m2)
    m1 = m2.
  Proof.
    destruct m1, m2; intros Hm1 Hm2 Heq.
    { reflexivity. }
    { pose (Heq p); simpl in *; tauto. }
    { pose (Heq p); simpl in *; tauto. }
    { epose map_extensional_aux.
      epose (e H0 _ _ _ _ Hm1 Hm2).
      assert (p = p0).
      eapply map_extensional_head; auto.
      apply Hm1.
      apply Hm2.
      rewrite H1; f_equal.
      apply e0.
      rewrite H1 in ×.
      intro; split; intro.
      { assert (In p1 (p0 :: m2)) by hauto.
        destruct H3; auto.
        assert (In p m1) by congruence.
        simpl in Hm1.
        assert (Make.Ord.(COMPARABLE.compare) (fst p) (fst p) = -1).
        eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
        { apply in_map; eauto. }
        { rewrite (Compare.Valid.refl H0) in H5; auto.
          lia.
        }
      }
      { assert (In p1 (p0 :: m1)) by hauto.
        destruct H3; auto.
        assert (In p m2) by congruence.
        simpl in Hm2.
        assert (Make.Ord.(COMPARABLE.compare) (fst p0) (fst p0) = -1).
        eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
        { apply in_map; congruence. }
        { rewrite (Compare.Valid.refl H0) in H5; auto.
          lia.
        }
      }
    }
  Qed.

[filter_map] preserves sortedness when keys are preserved
  Lemma filter_map_ss `{Make.FArgs} {A B : Set}
    (f : Make.key × A M× (Make.key × B))
    (f_pres_key : k a k' b,
      f (k, a) = Some (k', b) k = k')
    (Hv : Map.Valid.t) (m : Make.t A) :
    StrictlySorted.t (List.map fst m)
    StrictlySorted.t (List.map fst (filter_map f m)).
  Proof.
    induction m as [|x]; auto; intro Hl.
    assert (t (List.map fst (filter_map f m))). {
      apply IHm; destruct m; auto; induction Hl; auto.
    }
    clear IHm.
    induction m as [|y].
    { simpl; case (f x); auto. }
    { induction Hl.
      simpl in ×.
      remember (f x) as fx; destruct fx;
      remember (f y) as fy; destruct fy; auto;
      destruct p, x; symmetry in Heqfx; apply f_pres_key in Heqfx; subst;
      try (destruct p0, y; symmetry in Heqfy; apply f_pres_key in Heqfy; subst);
      simpl in *; auto.
      apply IHm; auto; clear IHm.
      clear Heqfy b.
      destruct m as [|z]; auto; simpl in ×.
      induction H2.
      split; auto.
      apply (Compare.Valid.trans_lt Hv) with (fst y); auto.
    }
  Qed.

  Lemma add_preserves_sorting `{Make.FArgs} {A : Set}
    (Hv : Map.Valid.t) (m : Make.t A) : k v,
    t (List.map fst m)
    t (List.map fst (Make.add k v m)).
  Proof.
    intros.
    destruct m; [exact I|].
    Tactics.destruct_pairs.
    simpl in ×.
    generalize H0.
    generalize k0.
    clear H0 k0.
    induction m; simpl in ×.
    { intros.
      destruct Make.compare_keys eqn:?.
      { exact I. }
      { simpl.
        split; auto.
        unfold Make.compare_keys in Heqc.
        simpl in ×.
        apply (Valid.compare_keys_Lt Hv); auto.
      }
      { simpl.
        split; auto.
        rewrite (Compare.Valid.sym Hv); auto.
        rewrite <- Pos2Z.opp_pos; f_equal.
        apply (Valid.compare_keys_Gt Hv); auto.
      }
    }
    { intros.
      destruct Make.compare_keys eqn:?.
      { simpl in *; split.
        { assert (k = k0) by
            (apply Valid.compare_keys_Eq; auto).
          rewrite <- H1 in H0; apply H0.
        }
        { apply H0. }
      }
      { simpl in ×.
        repeat split; try tauto.
        apply (Valid.compare_keys_Lt Hv); auto.
      }
      { destruct a0.
        destruct (Make.compare_keys k k1) eqn:?; simpl in ×.
        { simpl; split.
          { rewrite (Compare.Valid.sym Hv); auto.
            rewrite <- Pos2Z.opp_pos; f_equal.
            apply (Valid.compare_keys_Gt Hv); auto.
          }
          { assert (k = k1) by (apply (Valid.compare_keys_Eq Hv); auto).
            rewrite H1; tauto.
          }
        }
        { repeat split.
          { rewrite (Compare.Valid.sym Hv); auto.
            rewrite <- Pos2Z.opp_pos; f_equal.
            apply (Valid.compare_keys_Gt Hv); auto.
          }
          { apply (Valid.compare_keys_Lt Hv); auto. }
          { tauto. }
        }
        { split.
          { tauto. }
          { pose (IHm k1) as IH.
            rewrite Heqc0 in IH.
            apply IH; tauto.
          }
        }
      }
    }
  Qed.

  Inductive pick_opt_ind `{Make.FArgs} {A : Set} {Hv : Map.Valid.t} :
    Make.key Make.t A option A Make.t A Prop :=
    | pick_nil k : pick_opt_ind k [] None []
    | pick_eq k m v : pick_opt_ind k ((k,v) :: m) (Some v) m
    | pick_lt k k' v m :
      Make.compare_keys k k' = Datatypes.Lt pick_opt_ind k ((k',v) :: m) None ((k',v) :: m)
    | pick_gt k k' v v' m m' :
      Make.compare_keys k k' = Datatypes.Gt pick_opt_ind k m v' m'
      pick_opt_ind k ((k',v) :: m) v' ((k',v) :: m').

  Lemma pick_opt_to_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
    (k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
    Make.pick_opt k m = (v,m') pick_opt_ind (Hv := Hv) k m v m'.
  Proof.
    generalize dependent k.
    generalize dependent v.
    generalize dependent m'.
    induction m; simpl; intros.
    { inversion_clear H0; constructor. }
    { destruct a as [k'].
      destruct Make.compare_keys eqn:kk.
      { inversion_clear H0.
        apply (Valid.compare_keys_Eq Hv) in kk; subst.
        constructor.
      }
      { inversion_clear H0. constructor; auto. }
      { destruct Make.pick_opt eqn:?.
        inversion H0; subst; clear H0.
        econstructor 4; eauto.
      }
    }
  Qed.

  Lemma pick_opt_from_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
    (k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
    pick_opt_ind (Hv := Hv) k m v m' Make.pick_opt k m = (v,m').
  Proof.
    induction 1; simpl; try (rewrite H0); auto.
    { rewrite (Valid.compare_keys_refl Hv); auto. }
    { rewrite IHpick_opt_ind; auto. }
  Qed.

[merge] preserves sortedness
  Lemma merge_ss `{Make.FArgs} {A B C : Set}
    (f : Make.key M× A M× B M× C)
    (Hv : Map.Valid.t) (m1 : Make.t A) :
     (m2 : Make.t B),
    StrictlySorted.t (List.map fst m2)
    StrictlySorted.t (List.map fst
      (Make.merge f m1 m2)).
  Proof.
    induction m1.
    { simpl; intros.
      apply filter_map_ss; auto.
      intros k a k' b Hf.
      destruct f; inversion Hf; auto.
    }
    { simpl; intros.
      destruct a.
      destruct Make.pick_opt eqn:?.
      assert (t (List.map fst (Make.merge f m1 t1))). {
        apply IHm1; clear IHm1.
        apply (pick_opt_to_ind Hv) in Heqp.
        induction Heqp; auto.
        { simpl in H0. destruct (List.map fst m); auto. apply H0. }
        { simpl in ×.
          assert (t (List.map fst m)). {
            destruct (List.map fst m); auto. apply H0.
          }
          specialize (IHHeqp H2); clear H2.
          inversion Heqp; subst; auto.
          { induction H0. destruct (List.map fst m'); auto; induction H2.
            simpl in *; split; auto.
            apply (Compare.Valid.trans_lt Hv) with k; auto.
          }
          { simpl in ×. induction H0; split; auto. }
        }
      }
      { destruct f; auto.
        apply add_preserves_sorting; auto.
      }
    }
  Qed.

End StrictlySorted.

Lemma Make_fold_lemma `{Make.FArgs} {A B : Set}
  (P : B Prop)
  (f : Make.key A B B)
  (f_pres_P : k a b, P b P (f k a b)) :
   (m : Make.t A) b, P b
    P (Make.fold f m b).
Proof.
  induction m; intros.
  { exact H0. }
  { simpl.
    destruct a.
    apply IHm.
    apply f_pres_P; auto.
  }
Qed.

Lemma In_add_destruct `{Make.FArgs} {A : Set} {m : Make.t A} :
   {k k' : Make.key} {v v' : A},
  In (k, v) (Make.add k' v' m)
  (k', v') = (k, v) In (k, v) m.
Proof.
  induction m; intros.
  { left. simpl in *; tauto. }
  { simpl in ×.
    destruct a.
    destruct Make.compare_keys eqn:?.
    { destruct H0; tauto. }
    { destruct H0; tauto. }
    { destruct H0; try tauto.
      destruct (IHm _ _ _ _ H0); tauto.
    }
  }
Qed.

Lemma In_remove_In `{Make.FArgs} {A : Set} {m : Make.t A} :
   {k k' : Make.key} {v : A},
  In (k, v) (Make.remove k' m)
  In (k, v) m.
Proof.
  induction m; sauto.
Qed.

Lemma In_fold `{Make.FArgs} {A B : Set}
  (f : Make.key A B) :
   (m1 : Make.t A) (m2 : Make.t B) x y,
  In (x,y) (Make.fold (fun (k : Make.key) (v : A) ⇒
    Make.add k (f k v)) m1 m2)
  In (x,y) m2 ( z, In (x, z) m1 f x z = y).
Proof.
  induction m1; intros; simpl in ×.
  { tauto. }
  { destruct a.
    destruct (IHm1 _ _ _ H0) as
      [G| [z Hz]].
    { destruct (In_add_destruct G).
      { right; a; qauto. }
      { left; auto. }
    }
    { hauto. }
  }
Qed.

Lemma find_add : `{Make.FArgs} {a : Set} k v (m : Make.t a),
  Valid.t Make.find k (Make.add k v m) = Some v.
Proof.
  intros.
  induction m.
  { simpl.
    rewrite Valid.compare_keys_refl; auto.
  }
  { simpl.
    destruct a0.
    destruct (Make.compare_keys k k0) eqn:G.
    { simpl; rewrite Valid.compare_keys_refl; auto. }
    { simpl; rewrite Valid.compare_keys_refl; auto. }
    { simpl; rewrite G; exact IHm. }
  }
Qed.

Lemma find_respects_Eq `{Make.FArgs} {a : Set} : (k k' : Make.key)
  (m : Make.t a), Valid.t Make.compare_keys k k' = Datatypes.Eq
  Make.find k m = Make.find k' m.
Proof.
  intros k k' m Hv Heq.
  induction m.
  { reflexivity. }
  { simpl; destruct a0.
    unfold Make.compare_keys in ×.
    rewrite (Compare.Valid.congruence_left Hv k k'); auto.
    { destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0); auto.
      destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); auto.
    }
    { destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G.
      { rewrite Z.eqb_eq in G.
        apply (Compare.Valid.zero Hv); auto.
      }
      { destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0);
          try discriminate.
      }
    }
  }
Qed.

Lemma find_update : `{Make.FArgs} {a : Set} k f (m : Make.t a),
  Valid.t StrictlySorted.t (List.map fst m)
  Make.find k (Make.update k f m) = f (Make.find k m).
Proof.
  intros.
  induction m.
  { unfold Make.update.
    simpl.
    destruct (f None); auto.
    simpl; rewrite Valid.compare_keys_refl; auto.
  }
  { unfold Make.update in ×.
    simpl.
    destruct a0.
    destruct (Make.compare_keys k k0) eqn:G.
    { destruct (f (Some a0)).
      { simpl; rewrite Valid.compare_keys_refl; auto. }
      { rewrite (find_respects_Eq k k0 m H0); auto.
        unfold StrictlySorted.t in H1; simpl in H1.
        apply StrictlySorted.lb_find_None; auto.
      }
    }
    { destruct (f None).
      { simpl; rewrite Valid.compare_keys_refl; auto. }
      { simpl.
        rewrite G; reflexivity.
      }
    }
    { destruct (f (Make.find k m)).
      { simpl.
        rewrite G.
        apply IHm; eapply StrictlySorted.ss_tail; exact H1.
      }
      { simpl.
        rewrite G.
        apply IHm; eapply StrictlySorted.ss_tail; exact H1.
      }
    }
  }
Qed.

Lemma find_singleton : `{Make.FArgs} {a : Set} k (v : a),
  Valid.t Make.find k (Make.singleton k v) = Some v.
Proof.
  intros.
  simpl.
  rewrite Valid.compare_keys_refl; auto.
Qed.

Lemma mem_In `{Make.FArgs} : Valid.t
   k (s : Make.t unit), StrictlySorted.t (List.map fst s)
    Make.mem k s = true In (k,tt) s.
Proof.
  intros.
  induction s.
  { simpl; split; intro; (discriminate || tauto). }
  { simpl; split; intro; destruct a.
    { destruct (Make.compare_keys k k0) eqn:G.
      { left; simpl.
        unfold Make.compare_keys.
        destruct u; f_equal.
        unfold Make.compare_keys in ×.
        destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
        { rewrite Z.eqb_eq in G0.
          symmetry; apply (Compare.Valid.zero H0); auto.
        }
        { destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
             discriminate.
        }
      }
      { discriminate. }
      { right.
        apply IHs; try assumption.
        eapply StrictlySorted.ss_tail; exact H1.
      }
    }
    { destruct H2.
      { destruct u; inversion H2.
        rewrite Valid.compare_keys_refl; auto.
      }
      { destruct Make.compare_keys eqn:G; auto.
        { unfold Make.compare_keys in G.
          destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0);
            try discriminate.
          destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0) eqn:G0;
            try discriminate.
          rewrite Z.leb_le in G0.
          unfold StrictlySorted.t in H1.
          simpl in H1.
          assert (In k (List.map fst s)) as Hin.
          { assert (k = fst (k, tt)) as Hobv by auto.
            rewrite Hobv.
            apply in_map; auto.
          }
          pose proof (StrictlySorted.strictly_sorted_lb_correct
            (List.map fst s) k0 H0 H1 k Hin) as Hc.
          rewrite (Compare.Valid.sym H0) in Hc; auto. lia.
        }
        { rewrite IHs; auto.
          eapply StrictlySorted.ss_tail.
          exact H1.
        }
      }
    }
  }
Qed.

Lemma mem_not_In `{Make.FArgs} : Valid.t
   k (s : Make.t unit), StrictlySorted.t (List.map fst s)
    Make.mem k s = false ¬ In (k,tt) s.
Proof.
  intros.
  split; intros.
  { intro.
    rewrite <- mem_In in H3; auto.
    congruence.
  }
  { destruct Make.mem eqn:G.
    { rewrite mem_In in G; auto.
      contradiction.
    }
    { reflexivity. }
  }
Qed.

We can express the [mem] operation from the [find] one.
Lemma mem_from_find :
   {key value : Set} {Ord : COMPARABLE} (k : key)
    (m : Map.Make_t Ord value),
    (Map.Make Ord).(S.mem) k m =
    match (Map.Make Ord).(S.find) k m with
    | Some _true
    | Nonefalse
    end.
Proof.
  intros.
  induction m.
  { reflexivity. }
  { simpl.
    destruct a.
    destruct (Make.compare_keys k k0); auto.
  }
Qed.

Lemma mem_find_not_eq_none : {key value : Set} (k : key)
  (Ord : COMPARABLE) (m : Map.Make_t Ord value),
  (Map.Make Ord).(S.mem) k m = true
  (Map.Make Ord).(S.find (a := value)) k m None.
Proof.
  intros.
  induction m.
  { discriminate. }
  { simpl in ×.
    destruct a.
    destruct (Make.compare_keys k k0); try discriminate; auto.
  }
Qed.

Lemma find_mem_eq :
   {key value : Set} {Ord : COMPARABLE} (k : key) (v : value)
    (m : Map.Make_t Ord value),
    (Map.Make Ord).(S.find) k m = Some v
    (Map.Make Ord).(S.mem) k m = true.
Proof.
  intros.
  induction m.
  { discriminate. }
  { simpl in ×.
    destruct a.
    destruct (Make.compare_keys k k0); auto.
    discriminate.
  }
Qed.

Lemma add_found_eq : {key value : Set} (Ord : COMPARABLE)
                       (m : Map.Make_t Ord value)
                       (k : key) (v : value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    (Map.Make Ord).(S.find (a := value)) k m = Some v
    (Map.Make Ord).(S.add) k v m = m.
Proof.
  intros key value Ord m k v Hv Hfind.
  induction m.
  { discriminate. }
  { simpl in ×.
    destruct a.
    destruct (Make.compare_keys k k0) eqn:G.
    { inversion Hfind.
      repeat f_equal.
      apply (Compare.Valid.zero Hv); auto.
      unfold Make.compare_keys in G.
      destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
      { rewrite Z.eqb_eq in G0; auto. }
      { destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0); discriminate. }
    }
    { discriminate. }
    { f_equal; auto. }
  }
Qed.

Lemma find_eq_none_implies_mem_eq_false
  : {key value : Set} (k : key) (Ord : COMPARABLE)
      (m : Map.Make_t Ord value),
    (Map.Make Ord).(S.find (a := value)) k m = None
    (Map.Make Ord).(S.mem) k m = false.
Proof.
  intros.
  induction m.
  { reflexivity. }
  { simpl in ×.
    destruct a.
    destruct (Make.compare_keys k k0) eqn:G.
    { discriminate. }
    { reflexivity. }
    { tauto. }
  }
Qed.

Lemma find_add_eq_some
  : {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
      (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    (Map.Make Ord).(S.find (a := value))
       k ((Map.Make Ord).(S.add) k v m) = Some v.
Proof.
  intros key value k v Ord m Hv.
  induction m.
  { simpl.
    unfold Make.compare_keys.
    rewrite (Compare.Valid.refl Hv); auto.
  }
  { simpl.
    destruct a.
    destruct (Make.compare_keys k k0) eqn:G.
    { simpl.
      unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { simpl.
      unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { simpl.
      rewrite G.
      apply IHm.
    }
  }
Qed.

Lemma remove_add_id :
   {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
      (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    (Map.Make Ord).(S.mem) k m = false
    (Map.Make Ord).(S.remove (a := value))
       k((Map.Make Ord).(S.add) k v m) = m.
Proof.
  intros key value k v Ord m Hv Hmem.
  induction m.
  { simpl.
    unfold Make.compare_keys.
    rewrite (Compare.Valid.refl Hv); auto.
  }
  { destruct a.
    simpl in ×.
    destruct (Make.compare_keys k k0) eqn:G.
    { discriminate. }
    { simpl.
      unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { simpl.
      rewrite G.
      f_equal; auto.
    }
  }
Qed.

We do not change anything when removing an element which is not there.
Lemma remove_find_none :
   {key value : Set} (k : key) (Ord : COMPARABLE)
      (m : Map.Make_t Ord value),
    (Map.Make Ord).(S.find) k m = None
    (Map.Make Ord).(S.remove (a := value)) k m = m.
Proof.
  intros key value k Ord m Hfind.
  induction m.
  { reflexivity. }
  { destruct a; simpl in ×.
    destruct (Make.compare_keys k k0).
    { discriminate. }
    { reflexivity. }
    { f_equal; auto. }
  }
Qed.

Lemma add_add_eq :
   {key value : Set} (k : key) (v v' : value) (Ord : COMPARABLE)
      (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    (Map.Make Ord).(S.add (a := value)) k v
       ((Map.Make Ord).(S.add) k v' m) =
    (Map.Make Ord).(S.add (a := value)) k v m.
Proof.
  intros key value k v v' Ord m Hv.
  induction m.
  { simpl.
    unfold Make.compare_keys.
    rewrite (Compare.Valid.refl Hv); auto.
  }
  { destruct a.
    simpl in ×.
    destruct (Make.compare_keys k k0) eqn:G; simpl.
    { unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { rewrite G.
      f_equal; auto.
    }
  }
Qed.

Lemma mem_add_eq :
   {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
    (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    (Map.Make Ord).(S.mem)
       k ((Map.Make Ord).(S.add) k v m) = true.
Proof.
  intros key value k v Ord m Hv.
  induction m; simpl in ×.
  { unfold Make.compare_keys.
    rewrite (Compare.Valid.refl Hv); auto.
  }
  { destruct a; simpl.
    destruct (Make.compare_keys k k0) eqn:G; simpl.
    { unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { unfold Make.compare_keys.
      rewrite (Compare.Valid.refl Hv); auto.
    }
    { rewrite G; auto. }
  }
Qed.

Lemma find_add_neq: {key value : Set}
    (k k' : key) (v : value) (Ord : COMPARABLE)
    (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
    k k'
    ((Map.Make Ord).(S.find (a := value)) k
       ((Map.Make Ord).(S.add) k' v m)) =
      ((Map.Make Ord).(S.find (a := value)) k m).
Proof.
  intros key value k k' v Ord m Hv Hneq.
  induction m.
  { simpl.
    destruct (Make.compare_keys k k') eqn:G; auto.
    elim Hneq.
    apply (Compare.Valid.zero Hv); auto.
    unfold Make.compare_keys in G.
    destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G0.
    { apply Z.eqb_eq; auto. }
    { destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate.
    }
  }
  { destruct a; simpl in ×.
    destruct (Make.compare_keys k' k0) eqn:G; simpl in ×.
    { unfold Make.compare_keys in G.
      destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0) eqn:G0.
      { rewrite Z.eqb_eq in G0.
        rewrite (Compare.Valid.zero Hv _ _ I I G0).
        destruct (Make.compare_keys k k0) eqn:G1; auto.
        elim Hneq.
        apply (Compare.Valid.zero Hv); auto.
        rewrite (Compare.Valid.zero Hv _ _ I I G0).
        unfold Make.compare_keys in G1.
        destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G2.
        { rewrite <- Z.eqb_eq; auto. }
        { destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
            discriminate.
        }
      }
      { destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); discriminate. }
    }
    { destruct (Make.compare_keys k k') eqn:G0.
      { elim Hneq.
        unfold Make.compare_keys in G0.
        destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G1.
        { rewrite Z.eqb_eq in G1.
          apply (Compare.Valid.zero Hv); auto.
        }
        { destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate. }
      }
      { rewrite (@Valid.compare_keys_Lt_trans _
          (@Make.Build_FArgs key Ord) Hv _ _ _ G0 G); auto.
      }
      { destruct (Make.compare_keys k k0); auto. }
    }
    { destruct (Make.compare_keys k k0); auto. }
  }
Qed.

Lemma find_add_compare_int : {value : Set}
    (k k' : int) (v' : value) (Ord : COMPARABLE)
    (m : Map.Make_t Ord value),
    Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
  (Map.Make Ord).(S.find (a := value))
    k ((Map.Make Ord).(S.add) k' v' m) =
  if k =? k'
  then Some v'
  else (Map.Make Ord).(S.find (a := value)) k m.
Proof.
  intros.
  destruct (k =? k') eqn:Hkk'.
  { rewrite Z.eqb_eq in Hkk'.
    rewrite Hkk'.
    apply find_add_eq_some; auto.
  }
  { rewrite Z.eqb_neq in Hkk'.
    apply find_add_neq; auto.
  }
Qed.

Creates a map from a list of bindings.
Definition of_bindings {key value : Set} {Ord : COMPARABLE}
  (l : list (key × value)) : Map.Make_t Ord value :=
  List.fold_right
    (fun '(k, v) m ⇒ (Map.Make Ord).(S.add) k v m)
    l
    (Map.Make Ord).(S.empty).

Relate the [find] operation in a map and its bindings list.
Lemma find_of_bindings :
   {key value : Set} {Ord : COMPARABLE} (k : key)
  (l : list (key × value)),
  Compare.Valid.t (fun _True) (fun xx) Ord.(COMPARABLE.compare)
  (Map.Make Ord).(S.find) k (of_bindings l) =
  List.find_map
    (fun '(k', v)
      if Ord.(COMPARABLE.compare) k k' =? 0 then
        Some v
      else
        None
    )
    l.
Proof.
  intros key value Ord k l Hv.
  unfold of_bindings.
  induction l.
  { reflexivity. }
  { simpl.
    destruct a.
    destruct (Ord.(COMPARABLE.compare) k k0 =? 0) eqn:Hkk0.
    { rewrite Z.eqb_eq in Hkk0.
      rewrite (Compare.Valid.zero Hv _ _ I I Hkk0).
      apply find_add; auto.
    }
    { rewrite Z.eqb_neq in Hkk0.
      rewrite (find_add_neq k k0 v _ _ Hv); auto.
      intro Heq.
      apply Hkk0.
      rewrite Heq.
      apply (Compare.Valid.refl Hv); auto.
    }
  }
Qed.

[bindings] and [of_bindings] are inverse
Lemma bindings_of_bindings :
   {key value : Set} {Ord : COMPARABLE (t := key)}
  (l : list (key × value)),
  Sorted.Sorted (fun '(k1,_) '(k2,_)
    Ord.(COMPARABLE.compare) k1 k2 = -1) l
  (Map.Make Ord).(S.bindings) (of_bindings l) =
  l.
Proof.
  unfold Make; simpl.
  unfold Make.bindings.
  unfold of_bindings.
  intros.
  induction l.
  { reflexivity. }
  { destruct l.
    { destruct a; reflexivity. }
    { simpl in IHl.
      destruct p.
      simpl.
      rewrite IHl.
      { destruct a.
        simpl.
        unfold Make.compare_keys.
        inversion H.
        inversion H3.
        unfold Make.Ord.
        rewrite H5; auto.
      }
      { inversion H; auto. }
    }
  }
Qed.

Lemma cardinal_add_find_Some `{Make.FArgs} : {a : Set} (m : Make.t a)
  k v v', Map.Make.find k m = Some v'
  Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m.
Proof.
  intros ? m **.
  induction m.
  { discriminate. }
  { simpl in ×.
    destruct a0.
    destruct (Make.compare_keys k k0).
    { reflexivity. }
    { discriminate. }
    { unfold Make.cardinal; simpl.
      f_equal; tauto.
    }
  }
Qed.

Lemma cardinal_add_find_None `{Make.FArgs} : {a : Set} (m : Make.t a)
  k v, Map.Make.find k m = None
  Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m +i 1.
Proof.
  intros.
  induction m.
  { reflexivity. }
  { simpl in ×.
    destruct a0.
    destruct (Make.compare_keys k k0); try discriminate.
    { reflexivity. }
    { unfold Make.cardinal in *; simpl.
      rewrite (IHm H0); auto.
    }
  }
Qed.

The cardinal of a map after adding an element.
Lemma cardinal_add_find {key value : Set} (Ord : COMPARABLE (t := key))
  (k : key) (v : value) (m : (Map.Make Ord).(S.t) value) :
  (Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.add) k v m) =
  (Map.Make Ord).(S.cardinal) m +i
  match (Map.Make Ord).(S.find) k m with
  | None ⇒ 1
  | Some _ ⇒ 0
  end.
Proof.
  simpl.
  destruct Make.find as [v'|] eqn:?.
  { rewrite (cardinal_add_find_Some _ _ _ v') by assumption.
    unfold Make.cardinal.
    pose proof (List.length_is_valid m).
    lia.
  }
  { now rewrite cardinal_add_find_None. }
Qed.

Lemma length_remove_find_Some `{Make.FArgs} : {a : Set}
  (m : Make.t a) k v, Map.Make.find k m = Some v
   Datatypes.S (Datatypes.length (Map.Make.remove k m)) =
    Datatypes.length m.
Proof.
  intros.
  induction m.
  { discriminate. }
  { simpl in ×.
    Tactics.destruct_pairs.
    destruct Make.compare_keys.
    { reflexivity. }
    { discriminate. }
    { simpl; f_equal; auto. }
  }
Qed.

The cardinal of a map after removal, when the element is there.
Lemma cardinal_remove_find_Some `{Make.FArgs} : {a : Set}
  (m : Make.t a) k v, Map.Make.find k m = Some v
  Map.Make.cardinal (Map.Make.remove k m) =
  Map.Make.cardinal m -i 1.
Proof.
  intros.
  unfold Map.Make.cardinal.
  induction m; simpl in ×.
  { discriminate. }
  { Tactics.destruct_pairs.
    pose proof (List.length_is_valid m).
    destruct Make.compare_keys; simpl; try discriminate; lia.
  }
Qed.

The cardinal of a map after removal, when the element is not there.
Lemma cardinal_remove_find_None `{Make.FArgs} : {a : Set}
  (m : Make.t a) k, Map.Make.find k m = None
  Map.Make.cardinal (Map.Make.remove k m) =
  Map.Make.cardinal m.
Proof.
  intros.
  unfold Map.Make.cardinal.
  induction m; hauto q: on.
Qed.

The cardinal of a map after removing an element.
Lemma cardinal_remove_find {key value : Set} (Ord : COMPARABLE (t := key))
  (k : key) (m : (Map.Make Ord).(S.t) value) :
  (Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.remove) k m) =
  (Map.Make Ord).(S.cardinal) m -i
  match (Map.Make Ord).(S.find) k m with
  | None ⇒ 0
  | Some _ ⇒ 1
  end.
Proof.
  simpl.
  destruct Make.find eqn:?.
  { now apply (cardinal_remove_find_Some _ _ v). }
  { rewrite cardinal_remove_find_None by assumption.
    unfold Make.cardinal.
    pose proof (List.length_is_valid m).
    lia.
  }
Qed.

The cardinal of a map is a valid integer.
Lemma cardinal_is_valid {key value : Set} (Ord : COMPARABLE (t := key))
  (m : (Map.Make Ord).(S.t) value) :
  Pervasives.Int.Valid.t ((Map.Make Ord).(S.cardinal) m).
Proof.
  apply List.length_is_valid.
Qed.

Finding after a map operation is like finding before and then applying the mapping function over the result.
Lemma find_map {key value value' : Set} (Ord : COMPARABLE (t := key))
  (k : key) (f : value value') (map : Map.Make_t Ord value) :
  (let× x := (Map.Make Ord).(S.find) k map in
  Some (f x)) =
  (Map.Make Ord).(S.find) k ((Map.Make Ord).(S.map) f map).
Proof.
  simpl.
  induction map; hauto lq: on.
Qed.

A reformultion of [find_map] using typeclasses.
Lemma find_map_fargs `{Map.Make.FArgs} {a b : Set}
  (f : a b) (k : Map.Make.key) (map : Map.Make.t a) :
  (let× ' x := Map.Make.find k map in Some (f x)) =
  Map.Make.find k (Map.Make.map f map).
Proof.
  apply find_map.
Qed.

Adding and mapping a function over a map are commuting.
Lemma add_map {key value value' : Set} (Ord : COMPARABLE (t := key))
  (k : key) (v : value) (f : value value') (map : Map.Make_t Ord value) :
  (Map.Make Ord).(S.add) k (f v) ((Map.Make Ord).(S.map) f map) =
  (Map.Make Ord).(S.map) f ((Map.Make Ord).(S.add) k v map).
Proof.
  simpl.
  induction map; hauto lq: on.
Qed.

A reformulation of [add_map] using typeclasses.
Lemma add_map_fargs {value value' : Set} `{Map.Make.FArgs}
  (k : Map.Make.key) (v : value) (f : value value') (map : Map.Make.t value) :
  Map.Make.add k (f v) (Map.Make.map f map) =
  Map.Make.map f (Map.Make.add k v map).
Proof.
  apply add_map.
Qed.

The result of [Map.Make.mem] is not affected by [Map.Make.map].
Lemma mem_map_fargs {value value' : Set} `{Map.Make.FArgs}
  (k : Map.Make.key) (f : value value') (map : Map.Make.t value) :
  Map.Make.mem k (Map.Make.map f map) = Map.Make.mem k map.
Proof.
  induction map; [reflexivity|].
  destruct a; simpl.
  now destruct Map.Make.compare_keys.
Qed.

Removing and mapping a function over a map are commuting.
Lemma remove_map {key value value' : Set} (Ord : COMPARABLE (t := key))
  (k : key) (f : value value') (map : Map.Make_t Ord value) :
  (Map.Make Ord).(S.remove) k ((Map.Make Ord).(S.map) f map) =
  (Map.Make Ord).(S.map) f ((Map.Make Ord).(S.remove) k map).
Proof.
  simpl.
  induction map; hauto lq: on.
Qed.

Result of the application of a [fold] after a [map] operation.
Lemma fold_map {key value value' acc : Set} (Ord : COMPARABLE (t := key))
  (f : value value') (g : key value' acc acc)
  (map : Map.Make_t Ord value) :
   (init : acc),
  (Map.Make Ord).(S.fold) g ((Map.Make Ord).(S.map) f map) init =
  (Map.Make Ord).(S.fold) (fun k v ag k (f v) a) map init.
Proof.
  simpl.
  induction map as [|[k v] map]; simpl; sfirstorder.
Qed.

Result of the application of a [fold_es] after a [map] operation.
Lemma fold_es_map {key value value' acc : Set} (Ord : COMPARABLE (t := key))
  (f : value value') (g : key value' acc M? acc)
  (map : Map.Make_t Ord value) :
   (init : acc),
  (Map.Make Ord).(S.fold_es) g ((Map.Make Ord).(S.map) f map) init =
  (Map.Make Ord).(S.fold_es) (fun k v ag k (f v) a) map init.
Proof.
  intros.
  apply fold_map.
Qed.

Lemma In_add `{Make.FArgs} {A : Set}
  (k : Make.key) (a : A) (m : Make.t A) :
  In (k, a) (Make.add k a m).
Proof.
  induction m; [left; auto|].
  simpl. destruct a0.
  destruct Make.compare_keys eqn:?; simpl; [left|left|right]; auto.
Qed.

Lemma In_add_intro `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
  (k k': Make.key) (a a': A) (m : Make.t A) :
  (k,a) = (k', a') (k k' In (k, a) m)
  In (k, a) (Make.add k' a' m).
Proof.
  induction m; simpl; intro Hi.
  { destruct Hi; auto. induction H0; auto. }
  { destruct a0 as [k0 a0].
    destruct Hi.
    { inversion H0; subst k' a'; clear H0.
      destruct (Make.compare_keys k k0) eqn:?; simpl; [left|left|right]; auto.
    }
    { induction H0.
      induction H1.
      { inversion H1; subst k0 a0; clear H1.
        remember (Make.compare_keys k' k) as kk. symmetry in Heqkk.
        destruct kk.
        { apply (Valid.compare_keys_Eq Hv) in Heqkk; subst.
          contradiction H0; auto.
        }
        { right; left; auto. }
        { left; auto. }
      }
      { assert (In (k, a) (Make.add k' a' m)). {
        apply IHm; right; auto.
        }
        destruct (Make.compare_keys k' k0);
        [right|right; right| right]; auto.
      }
    }
  }
Qed.

Lemma pick_opt_not_In `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
  (k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
  StrictlySorted.t (List.map fst m)
  Make.pick_opt k m = (v,m')
  ¬ In k (List.map fst m').
Proof.
  intros Hss Hk F.
  apply (StrictlySorted.pick_opt_to_ind Hv) in Hk.
  induction Hk; simpl in *; auto.
  { induction (List.map fst m); auto; simpl in ×.
    induction Hss; induction F.
    { subst. rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
    { apply IHl; auto. destruct l; auto; simpl.
      induction H1; split; auto.
      apply (Compare.Valid.trans_lt Hv) with a; auto.
    }
  }
  { induction F.
    { subst. apply (Valid.compare_keys_Lt Hv) in H0.
      rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
    { induction (List.map fst m); auto.
      simpl in ×. induction Hss.
      induction H1.
      { subst. apply (Valid.compare_keys_Lt Hv) in H0.
        rewrite (Compare.Valid.sym Hv) in H0; auto.
        rewrite H2 in H0; inversion H0.
      }
      { apply IHl; auto.
        destruct l; auto.
        induction H3; simpl; split.
        { auto. apply (Compare.Valid.trans_lt Hv) with a; auto. }
        { induction H1; auto. }
      }
    }
  }
  { induction F.
    { subst. apply (Valid.compare_keys_Gt Hv) in H0.
      rewrite (Compare.Valid.refl Hv) in H0; inversion H0; auto.
    }
    { apply IHHk; auto.
      destruct (List.map fst m); auto; simpl.
      induction Hss; auto.
    }
  }
Qed.

Lemma Make_merge_In1 `{Make.FArgs} {A B C : Set}
  {f : Make.key M× A M× B M× C}
  {Hv : Map.Valid.t} {m1 : Make.t A} {Hss : StrictlySorted.t (List.map fst m1)}
  : {m2 k c a},
  In (k, a) m1
  ¬ In k (List.map fst m2)
  f k (Some a) None = Some c
  In (k, c) (Make.merge f m1 m2).
Proof.
  induction m1; intros.
  { destruct H0. }
  { destruct a as [k' a'].
    destruct H0.
    { simpl in ×.
      assert (Make.pick_opt k m2 = (None, m2)). {
        induction m2; simpl; auto.
        destruct a as [k'']; simpl in ×.
        destruct (Make.compare_keys k k'') eqn:?; auto.
        { apply (Valid.compare_keys_Eq Hv) in Heqc0.
          contradiction H1; left; auto.
        }
        { assert (Make.pick_opt k m2 = (None, m2)) by auto.
          rewrite H3; auto.
        }
      }
      inversion H0; subst k' a'; clear H0.
      rewrite H3, H2.
      apply In_add.
    }
    { simpl.
      destruct (Make.pick_opt k' m2) eqn:?.
      apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
      assert (In (k, c) (Make.merge f m1 t)). {
        apply IHm1 with a0; auto; clear IHm1.
            { simpl in Hss; destruct (List.map fst m1); auto.
              induction Hss; auto.
            }
            { induction Heqp; simpl; auto.
              { intro F; apply H1; right; auto. }
              { intro F; induction F; subst.
                { apply H1; left; auto. }
                { apply IHHeqp; auto.
                  intro F; apply H1; right; auto.
                }
              }
            }
      }
      destruct (f k' (Some a') o); auto.
      apply In_add_intro; auto; right; split; auto.
      simpl in Hss.
      intro F; subst k'.
      clear IHm1 H3.
      induction m1.
      { inversion H0. }
      { induction Hss.
        induction H0; subst.
        { simpl in H4. rewrite (Compare.Valid.refl Hv) in H3; auto.
          inversion H3; auto.
        }
        { apply IHm1; auto; clear IHm1.
          { induction (List.map fst m1); auto.
            induction H4; simpl; split; auto.
            apply (Compare.Valid.trans_lt Hv) with (fst a); auto.
          }
        }
      }
    }
  }
Qed.

Lemma Make_merge_In2 `{Make.FArgs} {A B C : Set}
  {f : Make.key M× A M× B M× C}
  {Hv : Map.Valid.t} {m1 : Make.t A} {Hss : StrictlySorted.t (List.map fst m1)}
  : {m2 k c b},
  In (k, b) m2
  ¬ In k (List.map fst m1)
  f k None (Some b) = Some c
  In (k, c) (Make.merge f m1 m2).
Proof.
  induction m1; intros.
  { simpl in ×.
    induction m2; simpl.
    { inversion H0. }
    { destruct H0.
      { subst a. rewrite H2. left. auto. }
      { destruct a. destruct (f k0 None (Some b0)); [right|]; auto. }
    }
  }
  { destruct a; simpl.
    destruct (Make.pick_opt k0 m2) eqn:?.
    apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
    assert (In (k, c) (Make.merge f m1 t)). {
      apply IHm1 with b; auto.
        { simpl in Hss.
          destruct (List.map fst m1); auto.
          destruct Hss; auto.
        }
        { induction Heqp; simpl in *; auto.
          { induction H0; auto.
            inversion H0; subst.
            contradiction H1; left; auto.
          }
          { destruct H0; [left|right]; auto. }
        }
        { intro F; apply H1; right; auto. }
    }
    destruct (f k0 (Some a) o); auto.
    apply (In_add_intro Hv); right; split; auto.
    intro F; subst k0.
    contradiction H1; left; auto.
  }
Qed.

Lemma Make_merge_In3 `{Make.FArgs} {A B C : Set}
  {f : Make.key M× A M× B M× C}
  {m1 : Make.t A} {Hss : StrictlySorted.t (List.map fst m1)}
  : {m2 k c a b},
  In (k, a) m1
  In (k, b) m2
  f k (Some a) (Some b) = Some c
  In (k, c) (Make.merge f m1 m2).
Proof.
  intros.
Admitted.

Lemma Make_merge_In_inversion `{Make.FArgs} {A B C : Set}
  {f : Make.key M× A M× B M× C}
  {m1 : Make.t A} : {m2 k c},
  In (k, c) (Make.merge f m1 m2)
     ( a, In (k, a) m1
         ¬ In k (List.map fst m2)
         f k (Some a) None = Some c)
   ( b, In (k, b) m2
         ¬ In k (List.map fst m1)
         f k None (Some b) = Some c)
   ( a b, In (k, a) m1 In (k, b) m2
         f k (Some a) (Some b) = Some c).
Proof.
  induction m1; simpl; intros.
  { destruct (List.filter_map_In_invert H0) as [x [Hx1 Hx2]].
    destruct x as [k' v].
    destruct f eqn:?; [|discriminate].
    inversion Hx2; sauto.
  }
  { destruct a.
    destruct Make.pick_opt eqn:?.
    destruct f eqn:?.
    { admit. }
    { admit. }
  }
Admitted.

Lemma Make_fold_shortcircuit `{Make.FArgs} {A B tr : Set}
  (f : Make.key A Pervasives.result B tr Pervasives.result B tr)
  (f_pres_err : t k x, f k x (Pervasives.Error t) = Pervasives.Error t)
  (t : tr) : m : Make.t A,
    Make.fold f m (Pervasives.Error t) = Pervasives.Error t.
Proof.
  unfold Make.fold.
  induction m as [|[k v] m]; simpl; [reflexivity|].
  congruence.
Qed.

Lemma find_In `{Make.FArgs} {A : Set}
  (Hv : Map.Valid.t)
  (m : Make.t A) k v :
  StrictlySorted.t (List.map fst m)
  Make.find k m = Some v In k (List.map fst m).
Proof.
  (*TODO*)
Admitted.

Lemma find_not_In `{Make.FArgs} {A : Set}
  (Hv : Map.Valid.t)
  (m : Make.t A) k : ¬ In k (List.map fst m)
  Make.find k m = None.
Proof.
  induction m; intro Hnin.
  { reflexivity. }
  { simpl.
    destruct a.
    destruct Make.compare_keys eqn:?; auto.
    { elim Hnin.
      left.
      symmetry; apply Map.Valid.compare_keys_Eq; auto.
    }
    { simpl in *; tauto. }
  }
Qed.

Lemma mapi_preserves_keys `{Make.FArgs} {A B : Set}
  (f : Make.key A B) :
  (m : Make.t A), List.map fst (Make.mapi f m)
  = List.map fst m.
Proof.
  induction m.
  { reflexivity. }
  { destruct a.
    simpl; congruence.
  }
Qed.

Lemma add_In `{Make.FArgs} {A : Set} (m : Make.t A)
  : k v, In (k, v) (Make.add k v m).
Proof.
  induction m; intros.
  { left; auto. }
  { simpl.
    Tactics.destruct_pairs.
    destruct Make.compare_keys; hauto.
  }
Qed.

Definition disj {A : Set} (xs ys : list A) : Prop :=
   x, In x xs ¬ In x ys.

Lemma disj_key_still_In `{Make.FArgs} {A : Set}
  (Hv : Map.Valid.t)
  (m : Make.t A) : p k v, ¬ In k (List.map fst m)
   In p m In p (Make.add k v m).
Proof.
  induction m; intros.
  { destruct H1. }
  { simpl.
    Tactics.destruct_pairs.
    destruct Make.compare_keys eqn:?.
    { assert (k = k1) by (apply Map.Valid.compare_keys_Eq; auto).
      elim H0; hauto.
    }
    { right; auto. }
    { destruct H1; hauto. }
  }
Qed.

Lemma In_to_In_fold `{Make.FArgs} {A B : Set}
  (f : Make.key A B)
  (m1 : Make.t A) : (m2 : Make.t B) k a,
  Map.Valid.t
  StrictlySorted.t (List.map fst m1)
  StrictlySorted.t (List.map fst m2)
  disj (List.map fst m1) (List.map fst m2)
  (In (k, a) m1 In (k, f k a) m2)
   In (k, f k a) (Make.fold
   (fun k0 vMake.add k0 (f k0 v)) m1 m2).
Proof.
  induction m1; intros m2 k a' Hv Hss1 Hss2 Hdis Hin.
  { simpl.
    destruct Hin as [[]|]; auto.
  }
  { simpl.
    destruct a.
    apply IHm1; auto.
    { eapply StrictlySorted.ss_tail; exact Hss1. }
    { apply StrictlySorted.add_preserves_sorting; auto. }
    { intros x Hx1 Hx2.
      destruct (List.In_map_invert Hx1) as [[] [Hp1 Hp2]].
      simpl in ×.
      rewrite <- Hp1 in *; clear Hp1.
      destruct (List.In_map_invert Hx2) as [[] [Hq1 Hq2]].
      simpl in ×.
      rewrite Hq1 in Hq2; clear Hq1.
      destruct (In_add_destruct Hq2).
      { inversion H0.
        rewrite <- H2 in Hp2.
        pose proof (in_map fst _ _ Hp2); simpl in ×.
        epose proof (StrictlySorted.strictly_sorted_lb_correct
          _ _ Hv Hss1 _ H1).
        rewrite (Compare.Valid.refl Hv) in H4; lia.
      }
      { eapply Hdis.
        { right. apply in_map; eauto. }
        { assert (fst (k1, a0) = fst (k1, b))
            by auto.
          rewrite H1.
          apply in_map; auto.
        }
      }
    }
    destruct Hin.
    { destruct H0; try tauto.
      right; inversion H0.
      simpl in Hss1.
      apply add_In.
    }
    { right.
      apply disj_key_still_In; auto.
      intro; eapply Hdis.
      { left; reflexivity. }
      { exact H1. }
    }
  }
Qed.

Lemma In_mapi `{Make.FArgs} {A B : Set}
  (f : Make.key A B) (m : Make.t A) :
   k v, In (k, v) m In (k, f k v) (Make.mapi f m).
Proof.
  induction m; intros k v Hin; destruct Hin.
  { simpl; Tactics.destruct_pairs.
    left; congruence.
  }
  { simpl; Tactics.destruct_pairs.
    right; auto.
  }
Qed.

Lemma In_mapi_invert `{Make.FArgs} {A B : Set}
  {f : Make.key A B} {m : Make.t A} :
   {k b}, In (k, b) (Make.mapi f m)
   a, In (k, a) m f k a = b.
Proof.
  induction m; intros k b Hin.
  { destruct Hin. }
  { simpl in Hin; Tactics.destruct_pairs.
    destruct Hin.
    { a; sfirstorder. }
    { destruct (IHm _ _ H0) as [a' [Ha'1 Ha'2]].
       a'; sfirstorder. }
  }
Qed.

[Make.map] is equivalent to [List.map] on the value
Lemma map_list_eq `{Make.FArgs} {A B : Set}
  (f : A B) (m : Make.t A) :
  Make.map f m = List.map (fun '(k, v)(k, f v)) m.
Proof.
  induction m; hauto lq:on.
Qed.

A reformulation of [map_list_eq].
Lemma map_list_eq_fargs `{Map.Make.FArgs} {a b : Set}
  {f : Map.Make.key × a Map.Make.key × b} (g : a b)
  (m : Map.Make.t a) : ( k v, f (k, v) = (k, g v))
  Map.Make.map g m = List.map f m.
Proof.
  intro; induction m; hauto.
Qed.

Adding a valid (w.r.t [P]) element to a map preserves [P]
Lemma make_add_preserves_P
  {A B : Set}
  `{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
  (P : (A × B) Prop) (x : B) k :
  P (k, x)
  Forall P m
  Forall P (Make.add k x m).
Proof.
  intros H_P H_Forall.
  induction m as [|? ? IHm]; [constructor; assumption|].
  inversion H_Forall.
  cbn. do 2 step; [now constructor..|].
  constructor; [assumption|]. now apply IHm.
Qed.

Removing an element from a map preserves [P]
Lemma make_remove_preserves_P
  {A B : Set}
  `{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
  (P : (A × B) Prop) k :
  Forall P m
  Forall P (Make.remove k m).
Proof.
  intros H_Forall.
  induction m as [|? ? IHm]; [constructor; assumption|].
  inversion H_Forall.
  cbn. do 2 step.
  { assumption. }
  { assumption. }
  { constructor; [assumption|].
    now apply IHm.
  }
Qed.

[of_seq_node] and [to_seq_node] are inverses
Lemma of_seq_node_to_seq_node_eq {k v : Set}
  `{FArgs : Make.FArgs (t := k)}
  (m : list (k × v)) :
  Make.of_seq_node (to_seq_node m) = m.
Proof.
  induction m; [reflexivity|]; cbn.
  step. now rewrite IHm.
Qed.

Calling [add_seq_node] on an empty map is the the same as creating a map with [of_seq_node]
Lemma of_seq_node_add_seq_node_eq {k v : Set}
  `{FArgs' : Map.Make.FArgs (t := k)}
  (l : list (k × v)) :
  Sorted.Sorted (fun '(k1, _) '(k2, _)
    Make.compare_keys k2 k1 = Datatypes.Gt) l
  Make.add_seq_node (to_seq_node l) [] =
  Make.of_seq_node (to_seq_node l).
Proof.
  intros H_Sorted.
  induction l; [reflexivity|]; cbn.
  step; cbn in ×.
  destruct l; [reflexivity|]; cbn in ×.
  step.
  inversion H_Sorted as [|? ? ? HRel].
  inversion HRel as [|? ? H_compare_keys].
  rewrite H_compare_keys.
  (* I have this goal I can't apply induction because
     [Map.add_seq_node] keeps accumulating the arguments
     in the list, when I need something like [
     (k, v) :: Map.add_seq_node ...] *)

  assert (GOAL :
    Make.add_seq_node (to_seq_node l) [(k0, v0); (k1, v1)] =
   (k0, v0) :: (k1, v1) :: Make.of_seq_node (to_seq_node l)) by admit.
  apply GOAL.
Admitted.

[add_seq_node] and [to_seq_node] are inverses
Fixpoint add_seq_node_to_seq_node_eq {k v : Set}
   `{FArgs' : Map.Make.FArgs (t := k)}
    (x : list (k × v)) {struct x} :
  Sorted.Sorted (fun '(k1, _) '(k2, _)
    Make.compare_keys k2 k1 = Datatypes.Gt) x
  Make.add_seq_node (to_seq_node x) [] = x.
Proof.
  intros H_Sorted.
  rewrite of_seq_node_add_seq_node_eq by assumption.
  induction x; [reflexivity|]; cbn. step.
  destruct x eqn:?; cbn; [reflexivity|].
  cbn in ×. inversion H_Sorted as [].
  inversion H0. step.
  now rewrite IHx.
Qed.

Maps order do not matter w.r.t bindings
Axiom make_bindings_rev_eq : {k v : Set}
   `{FArgs' : Map.Make.FArgs (t := k)}
    (map : list (k × v)),
    Make.bindings map = Make.bindings (rev map).

TODO: rewrite for [fold_e] The function [fold_es] is valid.
Lemma fold_es_is_valid {k v a : Set} `{Map.Make.FArgs (t := k)}
  (P : k v Prop)
  (Q : a Prop)
  (f : k v a M? a)
  (map : Map.Make.t v)
  (acc : a) :
  Valid.t
  StrictlySorted.t (List.map fst map)
  Q acc
  ( k v acc, P k v Q acc
    letP? acc' := f k v acc in Q acc')
  ( k v, Map.Make.find k map = Some v P k v)
  letP? acc' := Make.fold_es f map acc in Q acc'.
Proof.
  intros Hv Hsort.
  unfold Make.fold_es.
  unfold Make.fold_e.
  intros Qacc PQf Pmap.
  generalize Qacc;
  generalize acc.
  induction map as [|[key val] map']; [easy|].
  intros; simpl.
  assert (P key val) as Pkv.
  { apply Pmap.
    simpl.
    now rewrite Valid.compare_keys_refl.
  }
  pose proof (PQf key val acc0 Pkv Qacc0) as fkv.
  destruct (f key val acc0) eqn:?; [|now rewrite Make_fold_shortcircuit].
  simpl in fkv.
  assert ( k' v', Make.find k' map' = Some v' P k' v') as Pmap'.
  { intros.
    apply Pmap.
    simpl.
    simpl in Hsort.
    assert (Make.Ord.(V0.Compare.COMPARABLE.compare) key k' = -1) as Hc.
    { eapply StrictlySorted.strictly_sorted_lb_correct; auto.
      { exact Hsort. }
      { eapply find_In; eauto.
        admit. (*TODO*)
      }
    }
    unfold Make.compare_keys.
    rewrite (Compare.Valid.sym Hv); auto.
    now rewrite Hc.
  }
  pose proof (StrictlySorted.ss_tail _ _ _ Hsort) as Hsort'.
  exact (IHmap' Hsort' Pmap' a0 fkv).
Admitted.