text:
(******************************************)
(*   Finite multiset library              *)
(*   Developped for the PACTOLE project   *)
(*   L. Rieg                              *)
(*                                        *)
(*   This file is distributed under       *)
(*   the terms of the CeCILL-C licence    *)
(*                                        *)
(******************************************)

Require Import MMapInterface.
Require Import Arith_base.
Require Import Omega.
Require Import PArith.
Require Import RelationPairs.
Require Import Equalities.
Require Import MMultisets.Preliminary.
Require Import MMultisets.MMultisetInterface.

Module FMultisets (MMap : Sfun) (E : OrderedType) : Sord E.

Module M := MMap(E).

Definition eq_pair := RelProd E.eq (@Logic.eq nat).
Definition eq_elt := RelCompFun E.eq (@fst E.t nat).

Instance Meq_equiv A : Equivalence (@M.eq_key_elt A).
Proof. split.
  intro. reflexivity.
  intros ? ?. now symmetry.
  intros ? y ? ? ?. now transitivity y.
Qed.

Instance Meq_key_equiv A : Equivalence (@M.eq_key A).
Proof. split.
  intro. reflexivity.
  intros ? ?. now symmetry.
  intros ? y ? ? ?. now transitivity y.
Qed.

Instance eq_pair_equiv : Equivalence eq_pair.
Proof. split. easy. easy. intros ? y ? ? ?. now transitivity y. Qed.

Lemma Meq_dec : forall x y : E.t * positive, {M.eq_key_elt x y} + {~M.eq_key_elt x y}.
Proof.
intros [t1 n1] [t2 n2].
destruct (E.eq_dec t1 t2). destruct (Pos.eq_dec n1 n2).
  left. now split.
  right. intros []. contradiction.
  right. intros []. contradiction.
Defined.

Lemma eq_key_elt_eq_key_weak_In B : forall x y n m l,
  E.eq x y -> InA (@M.eq_key_elt B) (x, n) l -> InA (@M.eq_key B) (y, m) l.
Proof.
intros x y n m l Heq Hin. induction l.
+ now inversion Hin.
+ inversion_clear Hin.
  - left. destruct a. compute in *. destruct H. now transitivity x; auto.
  - right. now apply IHl.
Qed.

Lemma NoDup_pair_In : forall A x y n m l, NoDupA (@M.eq_key A) l ->
  InA (@M.eq_key_elt _) (x, n) l -> InA (@M.eq_key_elt _) (y, m) l -> E.eq x y -> n = m.
Proof.
intros A x y n m l Hl Hinx Hiny Heq. induction Hl as [| [z p] l]. inversion_clear Hiny.
inversion_clear Hinx; inversion_clear Hiny.
- compute in H0, H1. destruct H0 as [H0 ?], H1 as [H1 ?]. now subst p m.
- compute in H0. destruct H0 as [H0 ?]. subst p. elim H.
  apply eq_key_elt_eq_key_weak_In with y m. now transitivity x. assumption.
- compute in H1. destruct H1 as [H1 ?]. subst p. elim H.
  apply eq_key_elt_eq_key_weak_In with x n. now transitivity y; auto. assumption.
- now apply IHHl.
Qed.

Lemma Melements_InA : forall A x n s, InA (@M.eq_key_elt A) (x, n) (M.bindings s) <-> M.MapsTo x n s.
Proof. intros. now apply M.bindings_spec1. Qed.

Instance Mfind_compat {A} : Proper (E.eq ==> @M.Equal A ==> Logic.eq) (@M.find A).
Proof.
intros x1 x2 Hx s1 s2 Hs. rewrite Hs. clear s1 Hs. destruct (M.find x1 s2) eqn:Hin.
- rewrite M.find_spec, Hx, <- M.find_spec in Hin. auto.
- destruct (M.find x2 s2) eqn:Hin'; trivial. rewrite M.find_spec, <- Hx, <- M.find_spec, Hin in Hin'. discriminate.
Qed.

Definition elt := E.t.
Definition t := M.t positive.

Definition empty : t := @M.empty positive.
Definition is_empty (s : t) := M.is_empty s.
Definition multiplicity x (s : t) := match M.find x s with Some n => Pos.to_nat n | None => 0 end.
Definition add (x : elt) (n : nat) (s : t) : t :=
  if eq_nat_dec n 0 then s else M.add x (Pos.of_nat (multiplicity x s + n)) s.
Definition singleton x n := add x n empty.
Definition remove (x : elt) (n : nat) (s : t) : t :=
  if eq_nat_dec n 0 then s else
  if le_lt_dec (multiplicity x s) n then M.remove x s else M.add x (Pos.of_nat (multiplicity x s - n)) s.
Definition union (s s' : t) := M.fold (fun x n acc => add x (Pos.to_nat n) acc) s s'.
Definition inter (s s' : t) :=
  M.fold (fun x n acc => add x ((fun x n => min (multiplicity x s) (Pos.to_nat n)) x n) acc) s' empty.
Definition diff (s s' : t) := M.fold (fun x n acc => add x (Pos.to_nat n - multiplicity x s') acc) s empty.
Definition lub (s s' : t) := M.fold (fun x n acc => add x (Pos.to_nat n - multiplicity x s') acc) s s'.
Definition equal (s s' : t) := M.equal Pos.eqb s s'.
Definition subset s s' := is_empty (diff s s').
Definition fold {A} f (s : t) := @M.fold positive A (fun x y => f x (Pos.to_nat y)) s.
Definition for_all f (s : t) := M.fold (fun x n b => b && f x (Pos.to_nat n)) s true.
Definition exists_ f (s : t) := M.fold (fun x n b => b || f x (Pos.to_nat n)) s false.
Definition nfilter f (s : t) :=
  M.fold (fun x n acc => if f x (Pos.to_nat n) : bool then add x (Pos.to_nat n) acc else acc) s empty.
Definition filter f (s : t) := nfilter (fun x _ => f x) s.
Definition npartition f (s : t) :=
  M.fold (fun x n acc => if f x (Pos.to_nat n) : bool then (add x (Pos.to_nat n) (fst acc), snd acc)
                                                      else (fst acc, add x (Pos.to_nat n) (snd acc))) s (empty,empty).
Definition partition f (s : t) := npartition (fun x _ => f x) s.
Definition cardinal (s : t) := M.fold (fun _ n acc => Pos.to_nat n + acc) s 0.
Definition size (s : t) := M.fold (fun _ _ n => S n) s 0.
Definition elements (s : t) := List.map (fun xy => (fst xy, Pos.to_nat (snd xy))) (M.bindings s).
Definition support (s : t) := M.fold (fun x _ l => cons x l) s nil.
Definition choose (s : t) := M.fold (fun x _ _ => Some x) s None.

Definition In := fun x s => multiplicity x s > 0.
Definition eq s s' := forall x, multiplicity x s = multiplicity x s'.
Definition Subset s s' := forall x, multiplicity x s <= multiplicity x s'.
Definition For_all (P : elt -> nat -> Prop) s := forall x, In x s -> P x (multiplicity x s).
Definition Exists (P : elt -> nat -> Prop) s := exists x, In x s /\ P x (multiplicity x s).

Global Notation "s  [=]  t" := (eq s t) (at level 70, no associativity).
Global Notation "s  [c=]  t" := (Subset s t) (at level 70, no associativity).

Lemma eq_Meq : forall s s', s [=] s' <-> M.Equal s s'.
Proof.
intros s s'. unfold eq, multiplicity, M.Equal. split; intros Heq x.
+ specialize (Heq x). destruct (M.find x s), (M.find x s').
  - apply Pos2Nat.inj in Heq. now subst.
  - assert (Hpos := Pos2Nat.is_pos p). omega.
  - assert (Hpos := Pos2Nat.is_pos p). omega.
  - reflexivity.
+ now rewrite Heq.
Qed.

Instance multiplicity_compat : Proper (E.eq ==> eq ==> Logic.eq) multiplicity.
Proof.
intros x y Hxy s s' Hs. rewrite eq_Meq in Hs. unfold multiplicity. now rewrite (Mfind_compat _ _ Hxy _ _ Hs).
Qed.

Global Instance eq_equiv : Equivalence eq.
Proof. split; try easy. intros x y z Hxy Hyz a. now rewrite Hxy, Hyz. Qed.
(** [eq] is obviously an equivalence, for subtyping only. *)

Instance In_compat : Proper (E.eq ==> eq ==> iff) In.
Proof. intros x y Hxy s s' ?. unfold In. now rewrite H, Hxy. Qed.

Theorem In_dec : forall x s, {In x s} + {~In x s}.
Proof. unfold In. intros. apply gt_dec. Qed.

Lemma In_MIn : forall x s, In x s <-> M.In x s.
Proof.
intros x s. split; intro H.
- exists (Pos.of_nat (multiplicity x s)). rewrite <- M.find_spec. unfold In, multiplicity in *.
  destruct (M.find x s). now rewrite Pos2Nat.id. now inversion H.
- destruct H as [n Hn]. rewrite <- M.find_spec in Hn. unfold In, multiplicity. rewrite Hn. now apply Pos2Nat.is_pos.
Qed.

Lemma Mequal_Mequivb_equiv : forall s s' : M.t positive, M.Equal s s' <-> M.Equivb Pos.eqb s s'.
Proof.
intros s s'. split.
+ intro Heq. split.
  - intro x. split; intros [e Hin]; exists e.
      now rewrite <- M.find_spec, <- Heq, M.find_spec.
      now rewrite <- M.find_spec, Heq, M.find_spec.
  - intros x e e' He He'. rewrite <- M.find_spec in *.
    rewrite Heq in He. rewrite He in He'. inversion_clear He'. unfold Cmp. now apply Pos.eqb_refl.
+ intros [Heq1 Heq2] x.
  destruct (M.find x s) as [e |] eqn:Hfind, (M.find x s') as [e' |] eqn:Hfind'.
  - f_equal. apply Pos.eqb_eq. apply (Heq2 x); now rewrite <- M.find_spec.
  - assert (Habs : M.In x s'). { rewrite <- Heq1. exists e. now rewrite <- M.find_spec. }
    destruct Habs as [e' Habs]. rewrite <- M.find_spec, Hfind' in Habs. discriminate Habs.
  - assert (Habs : M.In x s). { rewrite Heq1. exists e'. now rewrite <- M.find_spec. }
    destruct Habs as [e Habs]. rewrite <- M.find_spec, Hfind in Habs. discriminate Habs.
  - reflexivity.
Qed.

Lemma multiplicity_find_in : forall x s, In x s -> M.find x s = Some (Pos.of_nat (multiplicity x s)).
Proof.
intros x s Hin. unfold In, multiplicity in *. destruct (M.find x s) eqn:Hfind.
- now rewrite Pos2Nat.id.
- now inversion Hin.
Qed.

Lemma multiplicity_out : forall x s, multiplicity x s = 0 <-> M.find x s = None.
Proof.
unfold multiplicity. intros x s. split; intro Hs.
+ destruct (M.find x s).
  - elim (lt_irrefl 0). rewrite <- Hs at 2. now apply Pos2Nat.is_pos.
  - reflexivity.
+ now rewrite Hs.
Qed.

Lemma equal_spec : forall s s', equal s s' = true <-> s[=]s'.
Proof.
intros s s'. unfold equal. simpl. destruct (M.equal Pos.eqb s s') eqn:Heq.
+ split; intro H; trivial || clear H. rewrite M.equal_spec, <- Mequal_Mequivb_equiv in Heq.
  unfold eq, multiplicity. intro. now rewrite Heq.
+ split; intro Habs; try discriminate Habs. exfalso.
  assert (Hneq : ~M.Equivb Pos.eqb s s').
  { intro Habs'. rewrite <- M.equal_spec, Heq in Habs'. discriminate Habs'. }
  rewrite <- Mequal_Mequivb_equiv in Hneq. apply Hneq. intro x.
  unfold eq, multiplicity in Habs. specialize (Habs x). simpl in Habs.
  destruct (M.find x s) eqn:Hin1, (M.find x s') eqn:Hin2.
  - f_equal. now apply Pos2Nat.inj.
  - elim (lt_irrefl 0). rewrite <- Habs at 2. now apply Pos2Nat.is_pos.
  - elim (lt_irrefl 0). rewrite Habs at 2. now apply Pos2Nat.is_pos.
  - reflexivity.
Qed.

Corollary eq_dec : forall s s' : t, {s [=] s'} + {~s [=] s'}.
Proof.
intros s s'. destruct (equal s s') eqn:Heq.
- left. now rewrite <- equal_spec.
- right. rewrite <- equal_spec. rewrite Heq. discriminate.
Qed.

Lemma empty_spec : forall x, multiplicity x empty = 0.
Proof.
intro x. unfold multiplicity, empty.
destruct (M.find x M.empty) eqn:Hin.
- rewrite (M.empty_spec positive x) in Hin. discriminate Hin.
- reflexivity.
Qed.

Lemma is_empty_spec : forall s, is_empty s = true <-> s [=] empty.
Proof.
intros s. unfold is_empty. split; intro H.
+ rewrite M.is_empty_spec in H. intros x. rewrite empty_spec.
  unfold multiplicity. now rewrite H.
+ rewrite M.is_empty_spec. intro x. rewrite eq_Meq in H. rewrite H. apply M.empty_spec.
Qed.

Corollary is_empty_multiplicity : forall x s, is_empty s = true -> multiplicity x s = 0.
Proof.
intros x s Hs. unfold multiplicity. destruct (M.find x s) eqn:Hin; trivial.
rewrite is_empty_spec in Hs. rewrite eq_Meq in Hs. rewrite Hs, M.empty_spec in Hin. discriminate.
Qed.

Lemma add_same : forall x n s, multiplicity x (add x n s) = multiplicity x s + n.
Proof.
intros x n s. unfold add. destruct (eq_nat_dec n 0). omega.
unfold multiplicity at 1. simpl.
rewrite (M.add_spec1 s x (Pos.of_nat (multiplicity x s + n))).
rewrite Nat2Pos.id. reflexivity. omega.
Qed.

Lemma add_other : forall x y n s, ~E.eq y x -> multiplicity y (add x n s) = multiplicity y s.
Proof.
intros x y n s Hyx. unfold add. destruct (eq_nat_dec n 0); trivial. unfold multiplicity at 1 3.
rewrite (M.add_spec2 s (Pos.of_nat (multiplicity x s + n))). reflexivity. now intro; apply Hyx.
Qed.

Lemma remove_same : forall x n s, multiplicity x (remove x n s) = multiplicity x s - n.
Proof.
intros x n s. unfold remove. destruct (eq_nat_dec n 0). omega.
destruct (le_lt_dec (multiplicity x s) n) as [Hle | Hlt]; unfold multiplicity at 1; simpl.
- rewrite M.remove_spec1. omega.
- rewrite M.add_spec1. rewrite Nat2Pos.id. reflexivity. omega.
Qed.

Lemma remove_other : forall x y n s, ~E.eq y x -> multiplicity y (remove x n s) = multiplicity y s.
Proof.
intros x y n s Hyx. unfold remove. destruct (eq_nat_dec n 0); trivial.
assert (Hxy : ~E.eq x y) by (intro; now apply Hyx).
destruct (le_lt_dec (multiplicity x s) n) as [Hle | Hlt]; unfold multiplicity at 1; simpl.
- now rewrite M.remove_spec2.
- now rewrite M.add_spec2.
Qed.

Lemma singleton_same : forall x n, multiplicity x (singleton x n) = n.
Proof.
intros x n. unfold singleton, add. destruct (eq_nat_dec n 0).
+ subst n. apply empty_spec.
+ rewrite empty_spec. simpl. unfold multiplicity. rewrite M.add_spec1. now apply Nat2Pos.id.
Qed.

Lemma singleton_other : forall x y n, ~E.eq y x -> multiplicity y (singleton x n) = 0.
Proof.
intros x y n Heq. unfold singleton, add. destruct (eq_nat_dec n 0).
+ subst n. apply empty_spec.
+ rewrite empty_spec. simpl. unfold multiplicity. rewrite M.add_spec2, M.empty_spec; trivial. intro; now apply Heq.
Qed.

Lemma fold_add_out_list : forall f x n l s, ~InA (@M.eq_key positive) (x, n) l -> NoDupA (@M.eq_key _) l ->
  multiplicity x (fold_left (fun acc xn => add (fst xn) (f (fst xn) (snd xn)) acc) l s) = multiplicity x s.
Proof.
intros f x n l s Hin Hdup. revert s. induction l as [| [y m] l]; intro s; simpl.
- reflexivity.
- rewrite IHl. apply add_other. intro Habs. apply Hin. left. compute. auto. auto. now inversion_clear Hdup.
Qed.

Lemma fold_add_out : forall f x (s s' : t), ~M.In x s ->
  multiplicity x (M.fold (fun x n acc => add x (f x n) acc) s s') = multiplicity x s'.
Proof.
intros f x s s' Hin. rewrite M.fold_spec.
assert (Hs : forall n, ~(InA (@M.eq_key_elt _) (x, n) (M.bindings s))).
{ intros n Habs. apply Hin. exists n. now rewrite <- M.bindings_spec1. }
revert s'. induction (M.bindings s) as [| [y m] l]; intro s'; simpl.
+ reflexivity.
+ assert ( Hxy : ~E.eq x y). { intro Habs. apply (Hs m). left. now split. }
  rewrite IHl.
  - apply add_other. now auto.
  - intros n Habs. apply (Hs n). now right.
Qed.

Notation compatb := (Proper (E.eq ==> Logic.eq ==> Logic.eq)) (only parsing).

Lemma fold_add : forall f x (s s' : t), compatb f -> M.In x s ->
  multiplicity x (M.fold (fun x n acc => add x (f x (Pos.to_nat n)) acc) s s')
  = f x (multiplicity x s) + multiplicity x s'.
Proof.
intros f x s s' Hf [n Hin]. rewrite M.fold_spec.
assert (Hs : InA (@M.eq_key_elt positive) (x, n) (M.bindings s)) by now rewrite M.bindings_spec1.
assert (Hdup := M.bindings_spec2w s).
revert s'. induction (M.bindings s) as [| [y m] l]; intro s'; simpl; [now inversion Hs |].
destruct (Meq_dec (x, n) (y, m)) as [[H1 H2] | Hneq]; simpl in *; try subst m.
* transitivity (multiplicity x (add y (f y (Pos.to_nat n)) s')).
  + rewrite (fold_add_out_list (fun x y => f x (Pos.to_nat y)) x n).
    - reflexivity.
    - inversion_clear Hdup. clear -H H1. intro Habs. apply H. revert Habs. apply InA_eqA; trivial. refine _.
    - now inversion_clear Hdup.
  + rewrite H1, add_same, plus_comm. f_equal. unfold multiplicity.
    rewrite H1, <- M.find_spec in Hin. now rewrite Hin.
* rewrite IHl.
  + f_equal. apply add_other. intro Habs. apply Hneq. compute. split. now auto.
    apply (NoDup_pair_In _ x y n m ((y, m) :: l)); trivial. left. compute. now auto.
  + inversion_clear Hs. contradiction. assumption.
  + now inversion_clear Hdup.
Qed.

Lemma union_spec : forall x s s', multiplicity x (union s s') = multiplicity x s + multiplicity x s'.
Proof.
intros x s s'. unfold union. destruct (M.find x s) eqn:Hin.
- apply (fold_add (fun x n => n)). now intros until 2. exists p. now rewrite <- M.find_spec.
- unfold multiplicity at 2. rewrite Hin. simpl. apply fold_add_out.
  intros [n Habs]. now rewrite <- M.find_spec, Hin in Habs.
Qed.

Lemma inter_spec : forall x s s', multiplicity x (inter s s') = min (multiplicity x s) (multiplicity x s').
Proof.
intros x s s'. unfold inter. destruct (M.find x s') eqn:Hin.
+ rewrite (fold_add (fun x n => min (multiplicity x s) n) x s' empty).
  - rewrite (empty_spec x). now rewrite plus_0_r.
  - intros ? ? Heq ? ? ?. simpl. subst. now rewrite Heq.
  - exists p. now rewrite <- M.find_spec.
+ rewrite fold_add_out.
  - unfold multiplicity at 3. rewrite Hin. rewrite Min.min_0_r. now apply empty_spec.
  - intros [n Habs]. now rewrite <- M.find_spec, Hin in Habs.
Qed.

Lemma diff_spec : forall x s s', multiplicity x (diff s s') = multiplicity x s - multiplicity x s'.
Proof.
intros x s s'. unfold diff. destruct (M.find x s) eqn:Hin.
+ rewrite (fold_add (fun x n => n - multiplicity x s') x s empty).
  - rewrite empty_spec. now rewrite plus_0_r.
  - intros ? ? Heq ? ? ?. subst. now rewrite Heq.
  - exists p. now rewrite <- M.find_spec.
+ rewrite fold_add_out.
  - unfold multiplicity at 2. rewrite Hin. simpl. now apply empty_spec.
  - intros [n Habs]. now rewrite <- M.find_spec, Hin in Habs.
Qed.

Lemma lub_spec : forall x s s', multiplicity x (lub s s') = max (multiplicity x s) (multiplicity x s').
Proof.
Proof.
intros x s s'. unfold lub.
replace (max (multiplicity x s) (multiplicity x s'))
  with (multiplicity x s - multiplicity x s'  + multiplicity x s') by (apply Max.max_case_strong; omega).
destruct (M.find x s) eqn:Hin.
+ apply (fold_add (fun x n => n - multiplicity x s')).
  - intros ? ? Heq ? ? ?. subst. now rewrite Heq.
  - exists p. now rewrite <- M.find_spec.
+ rewrite fold_add_out.
  - unfold multiplicity at 2. rewrite Hin. simpl. reflexivity.
  - intros [n Habs]. now rewrite <- M.find_spec, Hin in Habs.
Qed.

Lemma subset_spec : forall s s', subset s s' = true <-> s [c=] s'.
Proof.
intros s s'. split; intro Hle.
- intro x. apply (is_empty_multiplicity x) in Hle. rewrite diff_spec in Hle. omega.
- unfold subset. rewrite is_empty_spec. intro x. unfold In. rewrite diff_spec.
  specialize (Hle x). rewrite empty_spec. omega.
Qed.

Lemma fold_spec : forall (A : Type) s (i : A) (f : elt -> nat -> A -> A),
    fold f s i = fold_left (fun acc xn => f (fst xn) (snd xn) acc) (elements s) i.
Proof. intros A i f s. unfold fold, elements. now rewrite M.fold_spec, fold_left_map. Qed.

Lemma cardinal_spec : forall s, cardinal s = fold (fun x n acc => n + acc) s 0.
Proof. intro. unfold cardinal. rewrite fold_spec. unfold elements. now rewrite fold_left_map, M.fold_spec. Qed.

Lemma size_spec : forall s, size s = length (support s).
Proof.
intro. unfold size, support. now rewrite M.fold_spec, fold_left_length, M.fold_spec, fold_left_cons_length.
Qed.

Lemma Melements_multiplicity : forall s x n,
  InA (@M.eq_key_elt _) (x, n) (M.bindings s)
  <-> multiplicity x s = Pos.to_nat n /\ Pos.to_nat n > 0.
Proof.
intros s x n. split; intro H.
+ apply M.bindings_spec1, M.find_spec in H. unfold multiplicity.
  rewrite H. split. reflexivity. apply Pos2Nat.is_pos.
+ destruct H as [H1 H2]. unfold multiplicity in H1. destruct (M.find x s) eqn:Hin.
  - rewrite M.bindings_spec1, <- M.find_spec. rewrite Hin. f_equal. now apply Pos2Nat.inj.
  - rewrite  <- H1 in H2. inversion H2.
Qed.

Corollary elements_spec : forall x n s,
  InA eq_pair (x, n) (elements s) <-> multiplicity x s = n /\ n > 0.
Proof.
intros x n s. unfold elements. rewrite InA_map_iff.
split; intro H.
+ destruct H as [[y m] [[Heq1 Heq2] Hin]]. rewrite Melements_multiplicity in Hin.
  hnf in Heq1, Heq2. simpl in *. subst n. now rewrite <- Heq1.
+ exists (x, Pos.of_nat n). destruct H as [H1 H2]. simpl in *. split.
  - split; hnf; simpl. reflexivity. apply Nat2Pos.id. omega.
  - rewrite Melements_multiplicity. simpl. rewrite H1. rewrite Nat2Pos.id. now split. omega.
+ apply Meq_equiv.
+ apply Meq_equiv.
+ clear. intros [] [] []. intros. split; simpl in *. assumption. now subst.
Qed.

Lemma elements_NoDupA : forall s, NoDupA (@M.eq_key _) (elements s).
Proof.
intro s. unfold elements. rewrite NoDupA_inj_map;
apply M.bindings_spec2w || apply Meq_key_equiv || (intros [] [] ?; assumption).
Qed.

Lemma support_elements_aux : forall x l1 l2, NoDupA (@M.eq_key _) (l1 ++ l2) ->
  ((InA E.eq x (fold_left (fun acc xn => fst xn :: acc) l1 (map (@fst _ _) l2)) <->
  exists n, InA eq_pair (x, n) (map (fun xn => (fst xn, Pos.to_nat (snd xn))) (l1 ++ l2)))).
Proof.
intros x l1. induction l1; simpl; intros l2 Hdup.
* split; intro H.
  + induction l2.
    - now inversion H.
    - destruct a as [y m]. inversion_clear H.
        exists (Pos.to_nat m). left. now split.
        apply IHl2 in H0. destruct H0 as [n Hn]. exists n. simpl. now right. now inversion_clear Hdup.
  + destruct H as [n Hn]. induction l2; simpl.
    - now inversion Hn.
    - destruct a as [y m]. inversion_clear Hdup. inversion_clear Hn.
        left. now destruct H1.
        right. now apply IHl2.
* destruct a as [y m]. simpl. split; intro H.
  + destruct (E.eq_dec x y). exists (Pos.to_nat m). left. now split.
    change (y :: map (fst (B:=positive)) l2) with (map (fst (B:=positive)) ((y,m) :: l2)) in H.
    rewrite IHl1 in H.
    - destruct H as [p Hp]. exists p. rewrite map_app in *. rewrite InA_app_iff in Hp.
        simpl in Hp. destruct Hp.
          right. rewrite InA_app_iff. now left.
          inversion_clear H.
             now left.
             right. rewrite InA_app_iff. now right.
    - rewrite NoDupA_swap_iff. assumption. refine _.
  + change (y :: map (fst (B:=positive)) l2) with (map (fst (B:=positive)) ((y,m) :: l2)).
    rewrite IHl1. destruct H as [n Hn]. exists n. rewrite map_app, InA_app_iff. inversion_clear Hn.
    - right. now left.
    - rewrite map_app, InA_app_iff in H. destruct H. now left. now do 2 right.
    - rewrite NoDupA_swap_iff. assumption. now apply Meq_key_equiv.
Qed.

Lemma support_elements : forall x s, InA E.eq x (support s) <-> InA eq_pair (x, multiplicity x s) (elements s).
Proof.
intros x s. unfold support, elements. rewrite M.fold_spec.
change nil with (map (@fst E.t nat) nil).
rewrite (support_elements_aux x (M.bindings s) nil); rewrite app_nil_r; [split; intro H |].
+ destruct H as [n Hn].
  assert (n = multiplicity x s).
  { rewrite (InA_map_iff (Meq_equiv _) eq_pair_equiv) in Hn.
    - destruct Hn as [[y m] [[Heqx Heqn] Hin]]. rewrite Melements_multiplicity in Hin.
      hnf in *. simpl in *. subst. symmetry. destruct Hin. rewrite <- Heqx. assumption.
    - intros [? ?] [? ?] Heq; simpl in *. hnf in Heq. destruct Heq; split; hnf; simpl in *; subst; auto. }
  now subst n.
+ now exists (multiplicity x s).
+ apply M.bindings_spec2w.
Qed.

Corollary support_spec : forall x s, InA E.eq x (support s) <-> In x s.
Proof. intros x s. rewrite support_elements. rewrite elements_spec. intuition. Qed.

Lemma support_NoDupA_aux : forall A B (l1 : list (A*B)) l2,
  fold_left (fun acc p => fst p :: acc) l1 l2 = rev (map (@fst _ _) l1) ++ l2.
Proof.
intros A B l1. induction l1; intro l2; simpl.
  reflexivity.
  rewrite IHl1. now rewrite <- app_assoc.
Qed.

Lemma support_NoDupA : forall s, NoDupA E.eq (support s).
Proof.
intro s. unfold support. rewrite M.fold_spec, support_NoDupA_aux, app_nil_r.
apply NoDupA_rev. now auto with typeclass_instances.
rewrite NoDupA_inj_map; (now apply M.bindings_spec2w) || (now auto with typeclass_instances) || (now intros ? ? ?).
Qed.

Lemma fold_nfilter_out_list : forall f x n l s, ~InA (@M.eq_key positive) (x, n) l -> NoDupA (@M.eq_key _) l ->
  multiplicity x (fold_left (fun acc xn => if f (fst xn) (snd xn) : bool
                                           then add (fst xn) (Pos.to_nat (snd xn)) acc else acc) l s)
  = multiplicity x s.
Proof.
intros f x n l s Hin Hdup. revert s. induction l as [| [y m] l]; intro s; simpl.
  reflexivity.
  rewrite IHl.
    destruct (f y m). apply add_other. intro Habs. apply Hin. left. compute. auto. auto.
    intro Habs. apply Hin. now right.
    now inversion_clear Hdup.
Qed.

Lemma nfilter_spec_In : forall f s s' x, compatb f -> In x s ->
  multiplicity x
    (M.fold
       (fun (x0 : M.key) (n : positive) (acc : t) =>
        if f x0 (Pos.to_nat n) : bool then add x0 (Pos.to_nat n) acc else acc) s s')
  = if f x (multiplicity x s) then multiplicity x s + multiplicity x s' else multiplicity x s'.
Proof.
intros f s s' x Hf Hin. rewrite M.fold_spec. revert s'. unfold In in Hin.
assert (Hs : InA (@M.eq_key_elt _) (x, multiplicity x s) (elements s)). { rewrite elements_spec. simpl. now split. }
assert (Hdup : NoDupA (@M.eq_key _) (elements s)) by apply elements_NoDupA.
unfold elements in Hs, Hdup.
induction (M.bindings s); simpl; intro s'; simpl in Hs.
* exfalso. rewrite <- InA_nil. apply Hs.
* destruct a as [y m].
  destruct (Meq_dec (x, Pos.of_nat (multiplicity x s)) (y, m)) as [Heq | Hneq].
  + destruct Heq as [H1 H2]. simpl in H1, H2 |- *. rewrite H1 in *. subst m.
    rewrite (fold_nfilter_out_list (fun x y => f x (Pos.to_nat y)) _ (Pos.of_nat (multiplicity y s))).
    - rewrite Nat2Pos.id; try omega.
      destruct (f y (multiplicity y s)) eqn:Htest.
        rewrite add_same, H1. now apply plus_comm.
        now rewrite H1.
    - inversion_clear Hdup. intro Habs. apply H. rewrite InA_map_iff.
        exists (y, Pos.of_nat (multiplicity y s)). split. reflexivity. eassumption.
        apply Meq_key_equiv.
        apply Meq_key_equiv.
        clear. intros [] [] Hxy. now compute in *.
    - inversion_clear Hdup. rewrite NoDupA_inj_map in H0.
        eassumption.
        now apply Meq_key_equiv.
        now apply Meq_key_equiv.
        now intros [] [].
        now intros [] [].
  + inversion_clear Hs.
    - elim Hneq. destruct H. split. assumption. simpl in *. now rewrite H0, Pos2Nat.id.
    - inversion_clear Hdup. assert (Hxy : ~E.eq x y).
      { intro Habs. apply H0. now apply (eq_key_elt_eq_key_weak_In _ x y (multiplicity x s)). }
      rewrite IHl; try assumption. simpl.
      destruct (f x (multiplicity x s)), (f y (Pos.to_nat m));
      reflexivity || rewrite add_other; reflexivity || now auto.
Qed.

Lemma nfilter_spec_out : forall f s s' x, ~In x s ->
  multiplicity x
    (M.fold
       (fun (x0 : M.key) (n : positive) (acc : t) =>
        if f x0 (Pos.to_nat n) : bool then add x0 (Pos.to_nat n) acc else acc) s s')
  = multiplicity x s'.
Proof.
intros f s s' x Hin. rewrite M.fold_spec.
assert (Hs : forall n, ~(InA (@M.eq_key_elt _) (x, n) (M.bindings s))).
{ intros n Habs. apply Hin. rewrite M.bindings_spec1, <- M.find_spec in Habs.
  unfold In, multiplicity. rewrite Habs. apply Pos2Nat.is_pos. }
revert s'. induction (M.bindings s) as [| [y m] l]; intro s'; simpl.
  reflexivity.
  assert ( Hxy : ~E.eq x y). { intro Habs. apply (Hs m). left. now split. }
  rewrite IHl. destruct (f y (Pos.to_nat m)). apply add_other. now auto. reflexivity.
  intros n Habs. apply (Hs n). now right.
Qed.

Corollary nfilter_spec : forall f x s, compatb f ->
    multiplicity x (nfilter f s) = if f x (multiplicity x s) then multiplicity x s else 0.
Proof.
intros f x s Hf. unfold nfilter.
destruct (multiplicity x s) eqn:Hin.
  rewrite nfilter_spec_out.
    now destruct (f x 0); apply empty_spec.
    unfold In. omega.
  rewrite nfilter_spec_In.
    now rewrite empty_spec, Hin, plus_0_r.
    assumption.
    unfold In. rewrite Hin. omega.
Qed.

Theorem filter_nfilter : forall f s, filter f s [=] nfilter (fun x _ => f x) s.
Proof. now unfold filter. Qed.

Corollary filter_spec : forall f x s, Proper (E.eq ==> Logic.eq) f ->
    multiplicity x (filter f s) = if f x then multiplicity x s else 0.
Proof.
intros f x s Hf. rewrite filter_nfilter, nfilter_spec.
- reflexivity.
- repeat intro. now apply Hf.
Qed.

Lemma choose_spec_aux : forall x s o, ~M.In x s ->
  fold_left (fun (_ : option M.key) (p : M.key * positive) => Some (fst p)) (M.bindings s) o = Some x ->
  o = Some x.
Proof.
intros x s o Hs.
assert (Hs' : forall n, ~InA (@M.eq_key_elt _) (x, n) (M.bindings s)).
{ intros n Habs. apply Hs. exists n. now apply M.bindings_spec1. } clear Hs.
revert o. induction (M.bindings s); simpl; intros o Hin.
+ assumption.
+ apply IHl in Hin.
  - elim (Hs' (snd a)). left. split; simpl. now inversion Hin. reflexivity.
  - intros n Habs. apply (Hs' n). now right.
Qed.

Lemma choose_Some : forall x s, choose s = Some x -> In x s.
Proof.
intros x s Hin. destruct (In_dec x s). assumption. unfold choose in Hin.
rewrite M.fold_spec in Hin. apply choose_spec_aux in Hin. now inversion Hin. now rewrite <- In_MIn.
Qed.

Lemma choose_None : forall s, choose s = None <-> s [=] empty.
Proof.
intros s. split; intro Hs.
+ intro x. unfold choose in Hs. rewrite M.fold_spec in Hs. rewrite empty_spec, multiplicity_out.
  destruct (M.find x s) eqn:Habs.
  - rewrite M.find_spec, <- M.bindings_spec1 in Habs. destruct (M.bindings s).
      now inversion Habs.
      clear -Hs. simpl in Hs. revert p0 Hs. induction l. discriminate. intros. simpl in Hs. now apply (IHl _ Hs).
  - reflexivity.
+ destruct (choose s) eqn:H.
  - apply choose_Some in H. rewrite Hs in H. unfold In in H. rewrite empty_spec in H. omega.
  - reflexivity.
Qed.

Lemma fold_and_true_base_step : forall A f (l : list A) b,
  fold_left (fun a x => a && f x) l b = true -> b = true.
Proof.
intros A f l. induction l; simpl; intros b Hl.
- assumption.
- apply IHl in Hl. destruct b. reflexivity. simpl in Hl. discriminate Hl.
Qed.

Lemma fold_and_true_inductive_step : forall A f (l : list A) a b,
  fold_left (fun a x => a && f x) (a :: l) b = true -> f a = true.
Proof.
simpl. intros A f l a b Hl. apply fold_and_true_base_step in Hl.
destruct (f a). reflexivity. destruct b; simpl in Hl; discriminate Hl.
Qed.

Lemma for_all_spec_aux : forall (f : M.key -> nat -> bool) s b, compatb f ->
  (M.fold (fun x n b => b && (f x (Pos.to_nat n))) s b = true
   <-> b = true /\ For_all (fun x n => f x n = true) s).
Proof.
intros f s b Hf. rewrite M.fold_spec. unfold For_all. split; intro H.
+ split. now apply fold_and_true_base_step in H.
  intros x Hin. rewrite In_MIn in Hin. destruct Hin as [n Hin]. apply M.bindings_spec1 in Hin.
  assert (Hn : multiplicity x s = Pos.to_nat n) by now rewrite Melements_multiplicity in Hin.
  revert b H x n Hn Hin. induction (M.bindings s); intros b H x n Hn Hin; inversion_clear Hin.
  - simpl in H. apply fold_and_true_base_step in H. rewrite andb_true_iff in H.
    destruct H as [_ H ], a, H0 as [H1 H2]. simpl in *. rewrite Hn, H1. now subst p.
  - simpl in H. apply (IHl _ H _ _ Hn H0).
+ destruct H as [Hb H]. subst b.
  assert (forall xn, InA (@M.eq_key_elt _) xn (M.bindings s) -> f (fst xn) (Pos.to_nat (snd xn)) = true).
  { intros [x n] Hx. simpl. rewrite Melements_multiplicity in Hx. destruct Hx as [Hm Hp].
    setoid_rewrite <- Pos2Nat.id. rewrite <- Hm. rewrite Nat2Pos.id. apply H. unfold In. now rewrite Hm. omega. }
  clear H. revert H0. induction (M.bindings s); simpl; intro Hin; trivial.
  rewrite Hin. apply IHl. intros x Hx. apply Hin. now right. now left.
Qed.

Corollary for_all_spec : forall f s, compatb f ->
  (for_all f s = true <-> For_all (fun x n => f x n = true) s).
Proof. intros. unfold for_all. rewrite for_all_spec_aux; intuition. Qed.

Lemma exists_spec_aux : forall (f : M.key -> nat -> bool) s b, compatb f ->
  (M.fold (fun x n b => b || (f x (Pos.to_nat n))) s b = true
   <-> b = true \/ Exists (fun x n => f x n = true) s).
Proof.
intros f s b Hf.
assert (Hequiv : Exists (fun x n => f x n = true) s <->
        exists x, exists n, InA (@M.eq_key_elt _) (x, n) (M.bindings s) /\ f x (Pos.to_nat n) = true).
{ split; intros [x Hx].
  destruct Hx as [Hin Hfx]. exists x. exists (Pos.of_nat (multiplicity x s)). split.
    rewrite Melements_multiplicity. unfold In in Hin. simpl. rewrite Nat2Pos.id. now split. omega.
    rewrite Nat2Pos.id. assumption. unfold In in Hin. omega.
  destruct Hx as [n [Hin Hfx]]. exists x. rewrite Melements_multiplicity in Hin. destruct Hin as [Hn Hp]. split.
    simpl in *. unfold In. now rewrite Hn.
    simpl in *. now rewrite Hn. }
rewrite Hequiv. clear Hequiv. rewrite M.fold_spec. unfold For_all. split; intro H.
+ revert b H. induction (M.bindings s); intros b H.
  - simpl in H. now left.
  - simpl in H. apply IHl in H. rewrite orb_true_iff in H. destruct H as [[H | H] | H]; (now left) || right.
      destruct a as [x n]. exists x. exists n. split. now left. assumption.
      destruct H as [x [n [Hin Hfx]]]. exists x. exists n. split. now right. assumption.
+ revert b H. induction (M.bindings s); simpl; intros b H.
  - destruct H. assumption.
    destruct H as [? [? [Habs _]]]. now inversion Habs.
  - apply IHl. rewrite orb_true_iff. destruct H as [H | H].
      now do 2 left.
      destruct H as [x [n [Hin Hfx]]]. inversion_clear Hin.
        left. right. destruct H as [H1 H2]. simpl in H1, H2. now rewrite <- H1, <- H2.
        right. exists x. exists n. now split.
Qed.

Corollary exists_spec : forall f s, compatb f ->
  (exists_ f s = true <-> Exists (fun x n => f x n = true) s).
Proof. intros. unfold exists_. rewrite exists_spec_aux; intuition discriminate. Qed.

Definition npartition_fun f := fun x n acc =>
         if f x (Pos.to_nat n) : bool
         then (add x (Pos.to_nat n) (fst acc), snd acc)
         else (fst acc, add x (Pos.to_nat n) (snd acc)).

Lemma fold_npartition_fst_out_list : forall f x n l s12,
  ~InA (@M.eq_key positive) (x, n) l -> NoDupA (@M.eq_key _) l ->
  multiplicity x
  (fst
     (fold_left (fun acc xn => if f (fst xn) (Pos.to_nat (snd xn)) : bool
         then (add (fst xn) (Pos.to_nat (snd xn)) (fst acc), snd acc)
         else (fst acc, add (fst xn) (Pos.to_nat (snd xn)) (snd acc))) l s12))
  = multiplicity x (fst s12).
Proof.
intros f x n l s12 Hin Hdup. revert s12. induction l as [| [y m] l]; intros s12; simpl.
  reflexivity.
  rewrite IHl.
    destruct (f y (Pos.to_nat m)); simpl.
      apply add_other. intro Habs. apply Hin. left. compute. auto. auto.
    intro Habs. apply Hin. now right.
    now inversion_clear Hdup.
Qed.

Lemma npartition_spec_fst_In : forall f (s : t) (s12 : t * t) x, compatb f -> In x s ->
  multiplicity x (fst (M.fold (fun x n acc =>
         if f x (Pos.to_nat n) : bool
         then (add x (Pos.to_nat n) (fst acc), snd acc)
         else (fst acc, add x (Pos.to_nat n) (snd acc))) s s12)) =
  (if f x (multiplicity x s) then multiplicity x s + multiplicity x (fst s12) else multiplicity x (fst s12)).
Proof.
intros f s s' x Hf Hin. rewrite M.fold_spec. revert s'. unfold In in Hin.
assert (Hs : InA (@M.eq_key_elt _) (x, multiplicity x s) (elements s)). { rewrite elements_spec. simpl. now split. }
assert (Hdup : NoDupA (@M.eq_key _) (elements s)) by apply elements_NoDupA.
unfold elements in Hs, Hdup.
induction (M.bindings s); simpl; intros [s1 s2]; simpl in Hs.
* exfalso. rewrite <- InA_nil. apply Hs.
* destruct a as [y m].
  destruct (Meq_dec (x, Pos.of_nat (multiplicity x s)) (y, m)) as [Heq | Hneq].
  + destruct Heq as [H1 H2]. simpl in H1, H2 |- *. rewrite H1 in *. subst m.
    rewrite (fold_npartition_fst_out_list f _ (Pos.of_nat (multiplicity y s))).
    - unfold npartition_fun. rewrite Nat2Pos.id; try omega.
      destruct (f y (multiplicity y s)) eqn:Htest; simpl.
        rewrite add_same, H1. now apply plus_comm.
        now rewrite H1.
    - inversion_clear Hdup. intro Habs. apply H. rewrite InA_map_iff.
        exists (y, Pos.of_nat (multiplicity y s)). split. reflexivity. eassumption.
        apply Meq_key_equiv.
        apply Meq_key_equiv.
        clear. intros [] [] Hxy. now compute in *.
    - inversion_clear Hdup. rewrite NoDupA_inj_map in H0.
        eassumption.
        now apply Meq_key_equiv.
        now apply Meq_key_equiv.
        now intros [] [].
        now intros [] [].
  + inversion_clear Hs.
    - elim Hneq. destruct H. split. assumption. simpl in *. now rewrite H0, Pos2Nat.id.
    - inversion_clear Hdup. assert (Hxy : ~E.eq x y).
      { intro Habs. apply H0. now apply (eq_key_elt_eq_key_weak_In _ x y (multiplicity x s)). }
      rewrite IHl; try assumption. simpl. unfold npartition_fun.
      destruct (f x (multiplicity x s)), (f y (Pos.to_nat m));
      reflexivity || simpl; rewrite add_other; reflexivity || now auto.
Qed.

Lemma npartition_spec_fst_out : forall f s s12 x, ~In x s ->
  multiplicity x (fst (M.fold (fun x n acc =>
         if f x (Pos.to_nat n) : bool
         then (add x (Pos.to_nat n) (fst acc), snd acc)
         else (fst acc, add x (Pos.to_nat n) (snd acc))) s s12)) = multiplicity x (fst s12).
Proof.
intros f s s' x Hin. rewrite M.fold_spec.
assert (Hs : forall n, ~(InA (@M.eq_key_elt _) (x, n) (M.bindings s))).
{ intros n Habs. apply Hin. rewrite M.bindings_spec1, <- M.find_spec in Habs.
  unfold In, multiplicity. rewrite Habs. apply Pos2Nat.is_pos. }
revert s'. induction (M.bindings s) as [| [y m] l]; intro s'; simpl.
  reflexivity.
  assert ( Hxy : ~E.eq x y). { intro Habs. apply (Hs m). left. now split. }
  rewrite IHl. unfold npartition_fun. destruct (f y (Pos.to_nat m)). apply add_other. now auto. reflexivity.
  intros n Habs. apply (Hs n). now right.
Qed.

Corollary npartition_spec_fst : forall f s, compatb f -> fst (npartition f s) [=] nfilter f s.
Proof.
intros f s Hf x. unfold npartition. rewrite nfilter_spec; trivial.
destruct (multiplicity x s) eqn:Hin.
  rewrite npartition_spec_fst_out.
    now destruct (f x 0); apply empty_spec.
    unfold In. omega.
  rewrite npartition_spec_fst_In.
    now rewrite empty_spec, Hin, plus_0_r.
    assumption.
    unfold In. rewrite Hin. omega.
Qed.

Lemma fold_npartition_snd_out_list : forall f x n l s12,
  ~InA (@M.eq_key positive) (x, n) l -> NoDupA (@M.eq_key _) l ->
  multiplicity x
  (snd
     (fold_left
        (fun acc xn =>
         if f (fst xn) (Pos.to_nat (snd xn)) : bool
         then (add (fst xn) (Pos.to_nat (snd xn)) (fst acc), snd acc)
         else (fst acc, add (fst xn) (Pos.to_nat (snd xn)) (snd acc))) l s12))
  = multiplicity x (snd s12).
Proof.
intros f x n l s12 Hin Hdup. revert s12. induction l as [| [y m] l]; intros s12; simpl.
  reflexivity.
  rewrite IHl.
    destruct (f y (Pos.to_nat m)). reflexivity. simpl. apply add_other. intro Habs. apply Hin. left. compute. auto.
    intro Habs. apply Hin. now right.
    now inversion_clear Hdup.
Qed.

Lemma npartition_spec_snd_In : forall f (s : t) (s12 : t * t) x, compatb f -> In x s ->
  multiplicity x
  (snd
     (M.fold
        (fun y n acc =>
         if f y (Pos.to_nat n) : bool
         then (add y (Pos.to_nat n) (fst acc), snd acc)
         else (fst acc, add y (Pos.to_nat n) (snd acc))) s s12)) =
  (if f x (multiplicity x s) then multiplicity x (snd s12) else multiplicity x s + multiplicity x (snd s12)).
Proof.
intros f s s' x Hf Hin. rewrite M.fold_spec. revert s'. unfold In in Hin.
assert (Hs : InA (@M.eq_key_elt _) (x, multiplicity x s) (elements s)). { rewrite elements_spec. simpl. now split. }
assert (Hdup : NoDupA (@M.eq_key _) (elements s)) by apply elements_NoDupA.
unfold elements in Hs, Hdup.
induction (M.bindings s); simpl; intros [s1 s2]; simpl in Hs.
* exfalso. rewrite <- InA_nil. apply Hs.
* destruct a as [y m].
  destruct (Meq_dec (x, Pos.of_nat (multiplicity x s)) (y, m)) as [Heq | Hneq].
  + destruct Heq as [H1 H2]. simpl in H1, H2 |- *. rewrite H1 in *. subst m.
    rewrite (fold_npartition_snd_out_list f _ (Pos.of_nat (multiplicity y s))).
    - rewrite Nat2Pos.id; try omega.
      destruct (f y (multiplicity y s)) eqn:Htest; simpl.
        now rewrite H1.
        rewrite add_same, H1. now apply plus_comm.
    - inversion_clear Hdup. intro Habs. apply H. rewrite InA_map_iff.
        exists (y, Pos.of_nat (multiplicity y s)). split. reflexivity. eassumption.
        apply Meq_key_equiv.
        apply Meq_key_equiv.
        clear. intros [] [] Hxy. now compute in *.
    - inversion_clear Hdup. rewrite NoDupA_inj_map in H0.
        eassumption.
        now apply Meq_key_equiv.
        now apply Meq_key_equiv.
        now intros [] [].
        now intros [] [].
  + inversion_clear Hs.
    - elim Hneq. destruct H. split. assumption. simpl in *. now rewrite H0, Pos2Nat.id.
    - inversion_clear Hdup. assert (Hxy : ~E.eq x y).
      { intro Habs. apply H0. now apply (eq_key_elt_eq_key_weak_In _ x y (multiplicity x s)). }
      rewrite IHl; try assumption. simpl.
      destruct (f x (multiplicity x s)), (f y (Pos.to_nat m));
      reflexivity || simpl; rewrite add_other; reflexivity || now auto.
Qed.

Lemma npartition_spec_snd_out : forall f s s12 x, ~In x s ->
  multiplicity x
  (snd
     (M.fold
        (fun y n acc =>
         if f y (Pos.to_nat n) : bool
         then (add y (Pos.to_nat n) (fst acc), snd acc)
         else (fst acc, add y (Pos.to_nat n) (snd acc))) s s12)) =
  multiplicity x (snd s12).
Proof.
intros f s s' x Hin. rewrite M.fold_spec.
assert (Hs : forall n, ~(InA (@M.eq_key_elt _) (x, n) (M.bindings s))).
{ intros n Habs. apply Hin. rewrite M.bindings_spec1, <- M.find_spec in Habs.
  unfold In, multiplicity. rewrite Habs. apply Pos2Nat.is_pos. }
revert s'. induction (M.bindings s) as [| [y m] l]; intro s'; simpl.
  reflexivity.
  assert ( Hxy : ~E.eq x y). { intro Habs. apply (Hs m). left. now split. }
  rewrite IHl. destruct (f y (Pos.to_nat m)); simpl. reflexivity. apply add_other. now auto.
  intros n Habs. apply (Hs n). now right.
Qed.

Corollary npartition_spec_snd : forall f s, compatb f -> snd (npartition f s) [=] nfilter (fun x n => negb (f x n)) s.
Proof.
intros f s Hf x. unfold npartition. rewrite nfilter_spec.
destruct (multiplicity x s) eqn:Hin.
  rewrite npartition_spec_snd_out.
    now destruct (f x 0); apply empty_spec.
    unfold In. omega.
  rewrite npartition_spec_snd_In.
    rewrite empty_spec, Hin, plus_0_r. now destruct (f x (S n)).
    assumption.
    unfold In. rewrite Hin. omega.
    intros ? ? Heq ? ? ?. subst. now rewrite Heq.
Qed.

Theorem partition_npartition_fst : forall f s, fst (partition f s) [=] fst (npartition (fun x _ => f x) s).
Proof. now unfold partition. Qed.

Theorem partition_npartition_snd : forall f s, snd (partition f s) [=] snd (npartition (fun x _ => f x) s).
Proof. now unfold partition. Qed.

Corollary partition_spec_fst : forall f s, Proper (E.eq ==> Logic.eq) f -> fst (partition f s) [=] filter f s.
Proof.
intros f s Hf. rewrite partition_npartition_fst, npartition_spec_fst.
- reflexivity.
- repeat intro. now apply Hf.
Qed.

Corollary partition_spec_snd : forall f s, Proper (E.eq ==> Logic.eq) f ->
  snd (partition f s) [=] filter (fun x => negb (f x)) s.
Proof.
intros f s Hf. rewrite partition_npartition_snd, npartition_spec_snd.
- reflexivity.
- repeat intro. now apply Hf.
Qed.

Instance fold_compat A (eqA : A -> A -> Prop) `{Equivalence A eqA} : forall f,
  Proper (E.eq ==> Logic.eq ==> eqA ==> eqA) f -> transpose2 eqA f ->
  Proper (eq ==> eqA ==> eqA) (fold f).
Proof.
intros f Hf Hfcomm s1 s2 Hs x y Hxy. unfold fold. do 2 rewrite M.fold_spec.
rewrite fold_left_symmetry_PermutationA.
+ reflexivity.
+ now apply Meq_equiv.
+ assumption.
+ repeat intro. now apply Hf; rewrite H1 || rewrite H0.
+ intros. apply Hfcomm.
+ apply NoDupA_equivlistA_PermutationA.
  - now apply Meq_equiv.
  - eapply NoDupA_strengthen; try apply M.bindings_spec2w. now intros [? ?] [? ?] [? ?].
  - eapply NoDupA_strengthen; try apply M.bindings_spec2w. now intros [? ?] [? ?] [? ?].
  - clear -Hs. intros [x n]. do 2 rewrite Melements_multiplicity. now rewrite Hs.
+ assumption.
Qed.

(** Specifics about ordering of elements *)
Definition lt_elt (xn yp : elt * nat) := E.lt (fst xn) (fst yp).

Theorem elements_Sorted : forall s, Sorted lt_elt (elements s).
Proof.
intros s. unfold elements. assert (Hsorted := M.bindings_spec2 s).
induction (M.bindings s).
+ constructor.
+ simpl. inversion_clear Hsorted. constructor.
  - now apply IHl.
  - induction H0; constructor; assumption.
Qed.

End FMultisets.

author: coq-contribs

repo: mmultisets


Require Import Crypto.Specific.Framework.RawCurveParameters.
Require Import Crypto.Util.LetIn.

(***
Modulus : 2^401 - 31
Base: 64
***)

Definition curve : CurveParameters :=
  {|
    sz := 7%nat;
    base := 64;
    bitwidth := 64;
    s := 2^401;
    c := [(1, 31)];
    carry_chains := None;

    a24 := None;
    coef_div_modulus := None;

    goldilocks := None;
    karatsuba := None;
    montgomery := true;
    freeze := Some false;
    ladderstep := false;

    mul_code := None;

    square_code := None;

    upper_bound_of_exponent_loose := None;
    upper_bound_of_exponent_tight := None;
    allowable_bit_widths := None;
    freeze_extra_allowable_bit_widths := None;
    modinv_fuel := None
  |}.

Ltac extra_prove_mul_eq _ := idtac.
Ltac extra_prove_square_eq _ := idtac.


text:
From mathcomp Require Import all_ssreflect.

(* 6. Sub-Types Terms with properties *)
(* 6.5 Finite functions *)

Section FinFunDef.
  Variables (aT : finType) (rT : Type).

  Inductive finfun_type : Type := Finfun of #|aT|.-tuple rT.
  (* テキストは finfun だが、finfun_type に変更する。 *)

  Definition fgraph f := let: Finfun t := f in t.
  (* Finfun 構造体から tupple を取り出す。 *)

  Canonical finfun_subType := Eval hnf in [newType for fgraph].
  Eval hnf in [newType for fgraph].         (* [subType for fgraph] *)
End FinFunDef.

(* Notation "{ 'ffun' aT -> rT }" := (finfun_type aT rT). *)
(* Notation "{ 'ffun' fT }" := (finfun_type (Phant fT)). *)

(* 有限ドメイン関数から通常の関数に変換する。 *)
Check fgraph : forall (aT : finType) (rT : Type), (finfun_type aT rT) -> #|aT|.-tuple rT.
Check @enum_rank : forall T : finType, T -> 'I_ _.
Check tnth : forall (n : nat) (T : Type), n.-tuple T -> 'I_n -> T.

Definition fun_of_fin (aT : finType) (rT : Type) (f : finfun_type aT rT) : (aT -> rT) :=
  fun (x : aT) => tnth (@fgraph aT rT f) (enum_rank x).
Coercion fun_of_fin : finfun_type >-> Funclass.

(* 通常の関数から有限ドメイン関数に変換する。 *)
Check codom_tuple : forall (aT : finType) (rT : Type), (aT -> rT) -> #|aT|.-tuple rT.

Definition finfun (aT : finType) (rT : Type) (f : aT -> rT) : (finfun_type aT rT) :=
  @Finfun aT rT (codom_tuple f).

Notation "[ 'ffun' x : aT => F ]" := (finfun _ _ (fun x : aT => F)).

Check [ffun i : 'I_4 => i + 2] : finfun_type (ordinal_finType 4) nat.
Check {ffun ordinal_finType 4 -> nat}.

(* eqType の継承 *)
Definition finfun_eqMixin (aT : finType) (rT : eqType) :=
  Eval hnf in [eqMixin of finfun_type aT rT by <:].
Canonical finfun_eqType (aT : finType) (rT : eqType) :=
  Eval hnf in EqType (finfun_type aT rT) (finfun_eqMixin aT rT).

(* codomain も有限な場合 *)

(* Exercise 7 の答え *)
Definition all_words n T (alphabet : seq T) :=
  let prepend x wl := [seq x :: w | w <- wl] in
  let extend wl := flatten [seq prepend x wl | x <- alphabet] in
  iter n extend [:: [::] ].

(*
Definition tuple_enum (T : finType) n : seq (n.-tuple T) :=
  pmap insub (all_words n (enum T)).

Lemma enumP T n : Finite.axiom (tuple_enum T n).
*)

(* 有限型としての としての 有限tuple (有限型を要素とするtuple) *)
Definition tuple_finMixin (n : nat_eqType) (T : finType) :=
  Eval hnf in FinMixin (@FinTuple.enumP n T).
Canonical tuple_finType (n : nat_eqType) (T : finType) :=
  Eval hnf in FinType (n.-tuple T) (tuple_finMixin n T).

(* 有限型としてのfinfun *)
Unset Printing Implicit.    (* Unset : implicitな引数を表示しない。 D:しない。 A:する。*)
Unset Printing Coercions.   (* Unset : コアーションを表示しない     D:しない。 A:する。*)
Unset Printing Notations. (*   Set : Notation を使って表示する。  D:する。  A:しない。*)
Unset Printing Universe.  (* Unset : 高階のTypeを表示しない。     D:しない。 A:- *)

(* 上で定義した funfun_type ではうまくいかない。 *)
Definition finfun_finMixin (aT rT : finType)  :=
  [finMixin of (finfun.finfun_type aT rT) by <:].
Canonical finfun_finType (aT rT : finType)  :=
  Eval hnf in FinType (finfun.finfun_type aT rT) (finfun_finMixin aT rT).

(* [finMixin of T] の T は、a subCountType structure over a type
   that has a finType structure. *)
(* [finMixin of T by <:] == a finType structure for T, when T has a subType   *)
(*                   structure over an existing finType.                      *)

Lemma card_ffun (aT rT : finType) : #|{ffun aT -> rT}| = #|rT| ^ #|aT|.
Proof.
Admitted.

Definition eqfun (A B : Type) (f g : B -> A) : Prop :=
  forall x, f x = g x.
Notation "f1 =1 f2" := (eqfun f1 f2).

(*
Lemma ffunP (aT rT : Type) (f1 f2 : {ffun aT -> rT}) : f1 =1 f2 <-> f1 = f2.
Proof.
  Admitted.
 *)

(*
Lemma bigA_distr_bigA (I J : finType) F :
  \big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j
    = \big[+%M/0]_(f : {ffun I -> J}) \big[*%M/1]_i F i (f i).
 *)

(* END *)

author: suharahiromichi

repo: coq

save_path: github-repos/coq/suharahiromichi-coq


text:
Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.arrival.basic.arrival_sequence rt.model.priority.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.schedulability rt.model.schedule.uni.basic.platform.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module TotalService.

  Import UniprocessorSchedule Schedulability Platform Job.

  (* In this section, we prove some useful lemmas about total_service. *)
  Section Lemmas.

    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job -> time.
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
    Variable job_task: Job -> Task.

    (* Consider any job arrival sequence with no duplicate jobs... *)
    Context {arr_seq: arrival_sequence Job}.
    Hypothesis H_arrival_sequence_is_a_set:
      arrival_sequence_is_a_set arr_seq.

    (* ... and any schedule of this arrival sequence. *)
    Variable sched: schedule Job.

    (* Assume that jobs only execute after they arrived. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    (* added hypothesis. need to fix.*)
    Lemma busy_last_instant:
      forall t d,  ( \sum_(j <- jobs_arrived_before arr_seq (t + d).+1)
      service_during sched j t (t + d).+1)
            =   ((\sum_(j <- jobs_arrived_before arr_seq (t + d))
                   service_during sched j t (t + d)) + (~~ is_idle sched (t + d))).
    Proof.
      unfold service_during.
      unfold service_at.
      unfold scheduled_at.
      unfold jobs_arrived_before.
      unfold arrived_between.
      intros t d.
      replace (jobs_arrived_between arr_seq 0 (t + d).+1) with (jobs_arrived_between arr_seq 0 (t + d) ++ jobs_arriving_at arr_seq (t + d)).
      Focus 2.
      unfold jobs_arrived_between.
      rewrite -> big_nat_recr.
      auto. rewrite -> leq0n; auto.
      replace (jobs_arrived_between arr_seq 0 (t + d).+1) with (jobs_arrived_between arr_seq 0 (t + d) ++ jobs_arriving_at arr_seq (t + d)).
      rewrite -> big_cat.
      rewrite -> exchange_big.
      rewrite -> big_cat_nat with (n := t + d).
      unfold is_idle.
      replace (\big[addn_comoid/0]_(t <= i < t + d) \big[addn_comoid/0]_(i0 <- jobs_arrived_between arr_seq 0 (t + d))(sched i == Some i0)) with (\sum_(j <- jobs_arrived_between arr_seq 0 (t + d)) \sum_(t <= t0 < t + d) (sched t0 == Some j)).
      Focus 2.
      rewrite -> exchange_big.
      auto.
      Focus 4.
      unfold jobs_arrived_between.
      symmetry.
      rewrite -> big_nat_recr.
      auto.
      auto.
      Focus 2.
      apply leq_addr.
      Focus 2.
      apply leqnSn with (n := (t + d)).
      replace (\big[addn_comoid/0]_(t + d <= i < (t + d).+1) \big[addn_comoid/0]_(i0 <- jobs_arrived_between arr_seq 0 (t + d)) (sched i == Some i0)) with (\big[addn_comoid/0]_(i0 <- jobs_arrived_between arr_seq 0 (t + d))(sched (t + d) == Some i0)).
      Focus 2.
      symmetry.
      rewrite -> big_nat1.
      auto.
      replace (\big[addn_monoid/0]_(i <- jobs_arriving_at arr_seq (t + d))(\sum_(t <= t0 < (t + d).+1) (sched t0 == Some i))) with (\big[addn_monoid/0]_(i <- jobs_arriving_at arr_seq (t + d))(sched (t + d) == Some i)).
      Focus 2.
      symmetry.
      rewrite -> exchange_big.
      rewrite -> big_cat_nat with (n := t + d).
      replace (\big[addn_comoid/0]_(t + d <= i < (t + d).+1) \big[addn_comoid/0]_(i0 <- jobs_arriving_at arr_seq (t + d)) (sched i == Some i0)) with (\big[addn_monoid/0]_(i <- jobs_arriving_at arr_seq (t + d)) (sched (t + d) == Some i)).
      Focus 2.
      symmetry.
      rewrite -> big_nat1.
      auto.
      Focus 2.
      apply leq_addr.
      Focus 2.
      apply leqnSn with (n := (t + d)).
      replace (\big[addn_comoid/0]_(t <= i < t + d) \big[addn_comoid/0]_(i0 <- jobs_arriving_at arr_seq (t + d)) (sched i == Some i0)) with 0.
      auto.
      induction d.
      symmetry.
      rewrite -> big_geq.
      auto.
      rewrite -> addn0.
      auto.
      symmetry.
      unfold jobs_must_arrive_to_execute in H_jobs_must_arrive_to_execute.
      unfold scheduled_at in H_jobs_must_arrive_to_execute.
      unfold has_arrived in H_jobs_must_arrive_to_execute.
      unfold jobs_arriving_at.

    Qed.
    Admitted.

    (* added hypothesis. need to fix.*)
    Lemma idle_last_instant:
      forall t d,  (is_idle sched (t + d))
      ->   ( \sum_(j <- jobs_arrived_before arr_seq (t + d).+1)
      service_during sched j t (t + d).+1)
            =   ((\sum_(j <- jobs_arrived_before arr_seq (t + d))
                   service_during sched j t (t + d)) + 0).
    Proof.
      Admitted.

    (* The total service provided is bounded by the length of the interval. *)
    Lemma total_service_bounded_by_interval_length:
      forall (t:time) (d:time), total_service_during sched t (t + d) <= d.
    Proof.
      intros t d. elim d.
      unfold total_service_during. replace (t+0) with t; auto.
      rewrite [\sum_(t <= t0 < t)_]big_geq. auto. auto.
      move => n. intros IH.
      unfold total_service_during. nat_norm.
      rewrite [\sum_(t <= t0 < (t+n).+1)_]big_nat_recr. Focus 2. apply leq_addr.
      replace (\big[addn_monoid/0]_(t <= i < t + n)_) with (total_service_during sched t (t+n)); auto.
      case_eq(~~ is_idle sched (t+n)); intros CaseH.
      rewrite -> addn1. apply IH.
      rewrite -> addn0. rewrite -> leqW. auto. apply IH.
      Qed.

    (* The total service during an interval is the sum of service
       of all jobs that arrive before the end of the interval. *)
    Lemma sum_of_service_of_jobs_is_total_service:
      forall (t:time) (d:time), total_service_during sched t (t+d) =
                                \sum_(j <- (jobs_arrived_before arr_seq (t+d))) service_during sched j t (t + d).
    Proof.
      intros t.
      unfold total_service_during in *.
      induction d.
      replace (t+0) with t by trivial.
      rewrite [\sum_(t <= t0 < t)_]big_geq; trivial.
      unfold service_during in *.
      rewrite [\sum_(j <- jobs_arrived_before arr_seq t)
                \sum_(t <= t0 < t)_]exchange_big.
      rewrite [\big[addn_comoid/0]_(t <= j < t)_]big_geq; auto; auto.
      rewrite -> big_cat_nat with (n := t+d);
        [> | apply leq_addr | nat_norm; apply leqnSn].
      unfold jobs_must_arrive_to_execute in *.
      rewrite -> big_cat_nat with (n := t+d) in IHd;
        [> | apply leq_addr | auto].
      rewrite [\big[addn_monoid/0]_(t + d <= i < t + d)_]big_geq in IHd; auto.
      rewrite -> addn0 in IHd.
      rewrite -> IHd. nat_norm.
      rewrite[\big[addn_monoid/0]_(t + d <= i < (t + d).+1)_]big_nat1.

      case_eq (~~ is_idle sched (t + d)). intro H.
      replace (addn_monoid (\sum_(j <- jobs_arrived_before arr_seq (t + d))
                             service_during sched j t (t + d)) (nat_of_bool true))
        with
          (addn_monoid (\sum_(j <- jobs_arrived_before arr_seq (t + d))
                         service_during sched j t (t + d)) 1); auto. symmetry.
      apply busy_last_instant; apply H.
      intro H.
      replace (addn_monoid (\sum_(j <- jobs_arrived_before arr_seq (t + d))
                             service_during sched j t (t + d)) (nat_of_bool false))
        with
          (addn_monoid (\sum_(j <- jobs_arrived_before arr_seq (t + d))
                         service_during sched j t (t + d)) 0); auto. symmetry.
      apply idle_last_instant. rewrite -> negbFE; [auto | apply H].
      Qed.

  End Lemmas.

End TotalService.

author: cd-public

repo: edf

save_path: github-repos/coq/cd-public-edf


text:
Require Import VST.floyd.proofauto.
Require Import sha.sha.
Require Import sha.SHA256.
Require Import sha.spec_sha.
Require Import sha.sha_lemmas.
Local Open Scope nat.
Local Open Scope logic.
Import LiftNotation.

Lemma Zlength_repeat:
  forall {A} n (x:A), Zlength (repeat x (Z.to_nat n)) = Z.max 0 n.
Proof.
intros.
rewrite Zlength_correct, repeat_length.
destruct (zlt n 0).
rewrite Z.max_l by lia.
rewrite Z2Nat_neg by auto. reflexivity.
rewrite Z2Nat.id by lia.
rewrite Z.max_r by lia.
auto.
Qed.

Import field_at_wand.SegmentHole.

Lemma splice_into_list_simplify0:
  forall {A} n (src dst: list A),
    Zlength src = n ->
    Zlength dst = n ->
    splice_into_list 0 n src dst = src.
Proof.
 intros.
 unfold splice_into_list.
rewrite !sublist_nil.
rewrite app_nil_l.
pose proof (Zlength_nonneg src).
rewrite sublist_nil' by lia.
rewrite app_nil_r.
auto.
Qed.

Lemma splice_into_list_self:
  forall {A} lo hi (l: list A),
    (0 <= lo <= hi)%Z ->
    (hi <= Zlength l)%Z ->
    splice_into_list lo hi (sublist lo hi l) l = l.
Proof.
 intros.
 unfold splice_into_list.
 autorewrite with sublist.
 auto.
Qed.
(*
Lemma splice_into_list_simplify1:
  forall lo hi src tgt,
    lo = Zlength tgt ->
    (hi-lo = Zlength src)%Z ->
    splice_into_list lo hi src tgt = tgt++src.
Proof.
intros; subst; unfold splice_into_list.
pose proof (Zlength_nonneg tgt).
pose proof (Zlength_nonneg src).
rewrite H0.
rewrite Z.sub_diag.
change (Z.to_nat 0) with 0%nat; simpl.
rewrite <- app_nil_end.
rewrite sublist_same by lia.
f_equal.
rewrite (sublist_nil hi), <- app_nil_end.
rewrite sublist_app by (rewrite ?Zlength_repeat, ?Z.max_r; lia).
rewrite ?Z.min_l by lia.
rewrite ?Z.max_r by lia.
rewrite sublist_nil, <- app_nil_end.
apply sublist_same; lia.
Qed.

Lemma splice_into_list_simplify2:
  forall lo hi src tgt,
    lo = Zlength tgt ->
    (lo <= hi)%Z ->
    (hi-lo <= Zlength src)%Z ->
    splice_into_list lo hi hi src tgt = tgt++ sublist 0 (hi-lo) src.
Proof.
intros; subst; unfold splice_into_list.
pose proof (Zlength_nonneg tgt).
pose proof (Zlength_nonneg src).
repeat rewrite Z.sub_diag.
change (Z.to_nat 0) with 0.
unfold repeat at 1.
rewrite <- app_nil_end.
rewrite sublist_same by lia.
f_equal.
rewrite sublist_nil, <- app_nil_end by lia.
rewrite sublist_app by (rewrite ?Zlength_repeat, ?Z.max_r; lia).
rewrite ?Z.min_l by lia.
rewrite ?Z.max_r by lia.
rewrite sublist_nil, <- app_nil_end by lia.
auto.
Qed.
*)
Lemma JMeq_skipn:
  forall ta tb n (la: list ta) (lb: list tb),
     ta=tb ->
     JMeq la lb ->
     JMeq (skipn n la) (skipn n lb).
Proof.
intros. subst tb. apply JMeq_eq in H0. subst lb. auto.
Qed.

Lemma JMeq_firstn:
  forall ta tb n (la: list ta) (lb: list tb),
    ta=tb -> JMeq la lb -> JMeq (firstn n la) (firstn n lb).
Proof.
intros. subst tb. apply JMeq_eq in H0. subst lb. auto.
Qed.

Lemma JMeq_length:
  forall ta tb (la: list ta) (lb: list tb),
     ta=tb -> JMeq la lb -> length la = length lb.
Proof.
intros. subst tb.  apply JMeq_eq in H0. subst lb. auto.
Qed.

Lemma JMeq_sublist:
  forall ta tb lo hi (la: list ta) (lb: list tb),
    ta=tb -> JMeq la lb -> JMeq (sublist lo hi la) (sublist lo hi lb).
Proof.
intros. subst tb. apply JMeq_eq in H0. subst lb. auto.
Qed.

 Definition fsig_of_funspec (fs: funspec)  :=
  match fs with mk_funspec fsig _ _ _ _ _ _=> fsig end.

Lemma part1_splice_into_list:
  forall {A} lo hi (al bl: list A),
    (0 <= lo <= Zlength bl)%Z ->
    sublist 0 lo (splice_into_list lo hi al bl) = sublist 0 lo bl.
Proof.
 intros.
 unfold splice_into_list.
 rewrite (sublist_app); rewrite ?Zlength_repeat, ?Z.max_l by lia; try lia;
 rewrite ?Zlength_sublist by lia;
 try (rewrite ?Zlength_correct; lia).
rewrite ?Z.min_l by lia.
rewrite ?Z.max_r by lia.
rewrite sublist_nil, <- app_nil_end by lia.
rewrite sublist_same; auto.
rewrite Zlength_sublist; lia.
Qed.

Lemma part3_splice_into_list:
  forall {A} lo hi n (al bl: list A),
    (0 <= lo <= hi)%Z -> (hi <= n)%Z ->
   (Zlength bl = n)%Z ->
   (Zlength al = hi-lo)%Z ->
    sublist hi n (splice_into_list lo hi al bl) = sublist hi n bl.
Proof.
 intros.
 unfold splice_into_list.
rewrite <- app_ass.
 rewrite (sublist_app); rewrite ?Zlength_repeat, ?Z.max_r, ?Z.max_l by lia; try lia;
 rewrite ?Zlength_sublist by lia;
 try (rewrite ?Zlength_correct; lia).
rewrite !Zlength_app.
rewrite Zlength_sublist; try lia.
rewrite ?Z.min_r by lia.
rewrite ?Z.max_r by lia.
rewrite sublist_nil by lia.
simpl.
rewrite Z.max_l by lia.
rewrite sublist_sublist by lia.
f_equal. lia.
rewrite !Zlength_app.
rewrite !Zlength_sublist; lia.
Qed.

Lemma Zlength_splice_into_list:
  forall {A} lo hi (al bl: list A),
    (0 <= lo <= hi)%Z -> (hi <= Zlength bl)%Z ->
    (hi - lo = Zlength al)%Z ->
    Zlength (splice_into_list lo hi al bl) = Zlength bl.
Proof.
intros.
unfold splice_into_list.
rewrite !Zlength_app.
rewrite !Zlength_sublist; rewrite ?Zlength_app; rewrite ?Zlength_repeat; try lia.
Qed.

Local Arguments nested_field_type cs t gfs : simpl never.

Lemma semax_call_id0_alt:
 forall Espec {cs: compspecs} Delta P Q R id bl argsig tfun retty cc A x Pre Post
   (GLBL: (var_types Delta) ! id = None),
       (glob_specs Delta) ! id = Some (NDmk_funspec (argsig, retty) cc A Pre Post) ->
       (glob_types Delta) ! id = Some (type_of_funspec (NDmk_funspec (argsig, retty) cc A Pre Post)) ->
   (*tfun = type_of_params argsig ->*)tfun =typelist_of_type_list argsig ->
  @semax cs Espec Delta (tc_exprlist Delta argsig bl
                  && |>((fun rho : environ =>
               Pre x (ge_of rho, eval_exprlist argsig bl rho)) *
              PROPx P (LOCALx Q (SEPx R))))
    (Scall None (Evar id (Tfunction tfun retty cc)) bl)
    (normal_ret_assert
       ((ifvoid retty (`(Post x) (make_args nil nil))
           (EX v:val, `(Post x) (make_args (ret_temp::nil) (v::nil))))
         * PROPx P (LOCALx Q (SEPx R)))).
Proof.
intros.
subst tfun.
eapply (@semax_call_id0 Espec cs Delta P Q R id bl (NDmk_funspec (argsig, retty) cc A Pre Post)
           argsig retty cc (rmaps.ConstType A) nil x
                  (fun _ => Pre) (fun _ => Post)); eauto.
apply funspec_sub_refl.
Qed.

Lemma call_memcpy_tuchar:  (* Uses CompSpecs from sha. *)
  forall (shp : share) (tp: type) (pathp: list gfield) (lop: Z) (vp': list val) (p: val)
           (shq: share) (tq: type) (pathq: list gfield) (loq: Z) (contents: list int) (q: val)
           (len : Z)
           (R': list mpred)
           (np nq : Z)
           (vp vp'': reptype (nested_field_type tp pathp))
           (vq : reptype (nested_field_type tq pathq))
           (e_p e_q e_n : expr)
           Espec Delta P Q R,
      typeof e_p = tptr tuchar ->
      typeof e_q = tptr tuchar ->
      typeof e_n = tuint ->
      (var_types Delta) ! _memcpy = None ->
     (glob_specs Delta) ! _memcpy = Some (snd memcpy_spec) ->
     (glob_types Delta) ! _memcpy = Some (type_of_funspec (snd memcpy_spec)) ->
     writable_share shp ->  readable_share shq ->
     nested_field_type tp pathp = tarray tuchar np ->
     nested_field_type tq pathq = tarray tuchar nq ->
     (0 <= lop)%Z ->
     (0 <= len <= Int.max_unsigned)%Z ->
     (lop + len <= np)%Z ->
     (0 <= loq)%Z ->  (loq + len <=  (*Zlength contents <=*) nq)%Z ->
     JMeq vq (map Vint contents) ->
     JMeq vp vp' ->
     JMeq vp'' (splice_into_list lop (lop+len) (sublist loq (loq + len) (map Vint contents)) vp') ->
     ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |--
         tc_exprlist Delta [tptr tvoid; tptr tvoid; tuint] [e_p; e_q; e_n]  &&
         local (`(eq (field_address0 tp (ArraySubsc lop :: pathp) p)) (eval_expr e_p)) &&
         local (`(eq (field_address0 tq (ArraySubsc loq :: pathq) q)) (eval_expr e_q)) &&
         local (`(eq (Vint (Int.repr len))) (eval_expr e_n)) &&
         PROP () (LOCALx Q (SEPx (field_at shp tp pathp vp p ::
                                                 field_at shq tq pathq vq q :: R'))) ->
   @semax _ Espec Delta
    (PROPx P (LOCALx Q (SEPx R)))
    (Scall None
             (Evar _memcpy
               (Tfunction
                (Tcons (tptr tvoid) (Tcons (tptr tvoid) (Tcons tuint Tnil)))
                  (tptr tvoid) cc_default))
              [e_p; e_q; e_n])
    (normal_ret_assert (PROPx P (LOCALx Q
     (SEPx (field_at shp tp pathp vp'' p ::
               field_at shq tq pathq vq q :: R'))))).
Proof.
intros until R.
intros TCp TCq TCn Hvar Hspec Hglob ? SHq ? ? Hlop Hlen Hnp Hloq Hnq; intros.
assert_PROP (fold_right and True P); [ go_lowerx; entailer! | ].
apply semax_post' with
   (PROPx nil   (LOCALx Q
           (SEPx
              (field_at shp tp pathp vp'' p
               :: field_at shq tq pathq vq q :: R'))));
 [ go_lowerx; entailer! | ].
clear H6. rename H5 into Hpre.
assert_PROP (Zlength vp' = np /\ Zlength contents = nq). {
eapply derives_trans; [apply Hpre |].
apply andp_left2.
go_lowerx; entailer!.
clear - H8 H10 H0 H1 H2 H3 H Hlop Hloq Hnp Hnq Hlen.
forget (nested_field_type tp pathp) as t0.
forget (nested_field_type tq pathq) as t1.
subst t0 t1.
simplify_value_fits in H8. destruct H8 as [H8 _].
simplify_value_fits in H10. destruct H10 as [H10 _].
apply JMeq_eq in H3. subst vp; auto.
apply JMeq_eq in H2. subst vq; auto.
rewrite Zlength_map in H10.
split; auto.
} destruct H5 as [Hvp' Hvq'].

assert (reptype (tarray tuchar np) = list val) by reflexivity.
rewrite <- H0 in H5.
assert (H99: reptype (nested_field_type tp (ArraySubsc 0 :: pathp)) = val)
  by (rewrite nested_field_type_ind, H0; reflexivity).
assert (exists vpx : list (reptype (nested_field_type tp (ArraySubsc 0 :: pathp))),
                    JMeq vp vpx)
  by (rewrite H99, <- H5; exists vp; auto).
destruct H6 as [vpx Hvpx].
assert_PROP (legal_nested_field tp pathp /\ legal_nested_field tq pathq). {
  eapply derives_trans; [apply Hpre | apply andp_left2].
go_lowerx; entailer!.
} destruct H6 as [LNFp LNFq].

pose (witness := ((shq,shp),
                              field_address0 tp (ArraySubsc lop :: pathp) p,
                              field_address0 tq (ArraySubsc loq :: pathq) q,
                              len,  sublist loq (loq+len) contents)).
pose (Frame :=
        array_with_hole shq tuchar loq (loq + len) nq (map Vint contents) (field_address tq pathq q)
          :: array_with_hole shp tuchar lop (lop + len) np vp' (field_address tp pathp p) :: R').
eapply semax_pre_post';
  [ | | eapply semax_call_id0_alt with (x:=witness)(P:=nil)(Q:=Q);
       try eassumption;
       try (rewrite ?Hspec, ?Hglob; reflexivity)].

* unfold convertPre. simpl fst; simpl snd.
 rewrite <- (andp_dup (local (tc_environ _))), andp_assoc.
 eapply derives_trans; [ apply andp_derives; [apply derives_refl | apply Hpre] | ].
 rewrite !andp_assoc.
 apply andp_right; [apply andp_left2, andp_left1, derives_refl |].
 eapply derives_trans; [ | apply now_later].
 assert_PROP (field_address0 tp (pathp SUB lop) p <> Vundef) as DEFp.
 {
   unfold tc_exprlist.
   simpl typecheck_exprlist.
   rewrite !denote_tc_assert_andp.
   apply derives_trans with (local (tc_environ Delta) && denote_tc_assert (typecheck_expr Delta e_p) && local ((` (eq (field_address0 tp (pathp SUB lop) p))) (eval_expr e_p))); [solve_andp |].
   go_lowerx.
   eapply derives_trans; [apply typecheck_expr_sound; auto |].
   apply prop_derives; intros.
   rewrite <- H7 in H8.
   intro.
   rewrite H9 in H8.
   revert H8; apply tc_val_Vundef.
 }
 assert_PROP (field_address0 tq (pathq SUB loq) q <> Vundef) as DEFq.
 {
   unfold tc_exprlist.
   simpl typecheck_exprlist.
   rewrite !denote_tc_assert_andp.
   apply derives_trans with (local (tc_environ Delta) && denote_tc_assert (typecheck_expr Delta e_q) && local ((` (eq (field_address0 tq (pathq SUB loq) q))) (eval_expr e_q))); [solve_andp |].
   go_lowerx.
   eapply derives_trans; [apply typecheck_expr_sound; auto |].
   apply prop_derives; intros.
   rewrite <- H7 in H8.
   intro.
   rewrite H9 in H8.
   revert H8; apply tc_val_Vundef.
 }
 apply andp_left2, andp_left2.
 subst witness. cbv beta iota. simpl @fst; simpl @snd.
 clear Hpre.
 autorewrite with norm1 norm2.
 instantiate (1:=Frame). simpl. unfold env_set, local, lift1, liftx, lift. simpl. intros tau. entailer!.

(* rewrite PROP_combine.*)
(* unfold app at 1.*)
(* instantiate (1:=Frame).
 unfold app at 2.
 go_lowerx.
 apply andp_right.
 apply prop_right.
 unfold make_args'. simpl.
 unfold eval_id, env_set.*)
 rewrite TCp, TCq, TCn.  simpl.
 unfold_lift; simpl.
 (*rewrite <- H6, <- H7, <- H8.*)
 normalize. unfold PROPx, LOCALx, SEPx, local, liftx, lift1, lift. simpl. unfold liftx, lift. simpl. normalize.

(* split3; try (repeat split; auto; congruence).*)
 apply andp_right.
 { apply prop_right; split3; auto. repeat split; trivial.  congruence.  }
 subst Frame.
 cancel.
 rewrite !field_at_data_at.
 rewrite (data_at_type_changable _ _ _ _ _ H0 H3).
 rewrite (data_at_type_changable _ _ _ _ _ H1 H2).
 sep_apply (array_with_hole_intro shp tuchar lop (lop + len) (*np*)(Zlength vp') vp' (field_address tp pathp p)); [lia | ].
 sep_apply (array_with_hole_intro shq tuchar loq (loq + len) (*nq*)(Zlength contents)  (map Vint contents) (field_address tq pathq q)); [lia | ].
 cancel.
 apply sepcon_derives.
 - apply derives_refl'.
   rewrite <- H1.
   rewrite <- field_address0_app by congruence.
   simpl app.
   apply equal_f.
   apply data_at_type_changable.
   + f_equal; clear; lia.
   + rewrite <- sublist_map.
     apply JMeq_sublist; auto.
 - replace (memory_block shp len) with
     (memory_block shp (sizeof (nested_field_array_type tp pathp lop (lop + len)))).
   2: {
     f_equal. unfold nested_field_array_type.
     rewrite nested_field_type_ind. rewrite H0. simpl.
     rewrite Z.max_r by lia. rewrite Z.mul_1_l. clear; lia.
   }
   eapply derives_trans; [ | apply data_at__memory_block_cancel]; cancel.
   rewrite <- H0.
   rewrite <- field_address0_app by congruence.
   simpl app.
   unfold nested_field_array_type, tarray.
   rewrite nested_field_type_ind, H0.
   apply data_at_data_at_.
 *
 intros. apply andp_left2.
 go_lowerx. unfold_lift.
 simpl.
 Intros x. rewrite prop_true_andp by auto.
 rewrite map_sublist.
 clear witness Frame.
 normalize in H7.
 subst x.
 simpl.
 clear Hpre H6 P Q rho .
assert (exists (vpy : list (reptype (nested_field_type tp (ArraySubsc 0 :: pathp)))),
                  JMeq vp'' vpy)
  by (rewrite H99; eauto).
destruct H6 as [vpy H7].
assert (Zlength vpy = np). {
 assert (JMeq vpy  (splice_into_list lop (lop + len)
          (sublist loq (loq + len) (map Vint contents)) vp')) by (eapply JMeq_trans; [apply @JMeq_sym |]; eassumption).
 transitivity (Zlength  (splice_into_list lop (lop + len)
          (sublist loq (loq + len) (map Vint contents)) vp')).
 clear - H6 H99 H5.
 forget (splice_into_list lop (lop + len)
          (sublist loq (loq + len) (map Vint contents)) vp') as vv.
 forget val as t. subst t. apply JMeq_eq in H6. subst; auto.
 rewrite Zlength_splice_into_list; try lia.
 autorewrite with sublist; auto.
}
cancel.
change (ArraySubsc loq :: pathq) with ([ArraySubsc loq] ++ pathq).
change (ArraySubsc lop :: pathp) with ([ArraySubsc lop] ++ pathp).
rewrite !field_address0_app by congruence.
rewrite H0, H1.
erewrite (data_at_type_changable shq _ (tarray tuchar (loq + len - loq)));
[| f_equal; lia | apply JMeq_refl].
erewrite (data_at_type_changable shp _ (tarray tuchar (lop + len - lop)));
[| f_equal; lia | apply JMeq_refl].
sep_apply (array_with_hole_elim shp tuchar lop (lop + len) np (sublist loq (loq + len) (map Vint contents)) vp' (field_address tp pathp p)).
sep_apply (array_with_hole_elim shq tuchar loq (loq + len) nq (sublist loq (loq + len) (map Vint contents)) (map Vint contents) (field_address tq pathq q)).
rewrite !field_at_data_at.
rewrite sepcon_comm.
apply sepcon_derives.
- apply derives_refl'.
  apply equal_f.
  apply data_at_type_changable; auto.
- apply derives_refl'.
  apply equal_f.
  apply data_at_type_changable; auto.
  eapply JMeq_trans; [| apply JMeq_sym, H2].
  apply eq_JMeq.
  apply splice_into_list_self.
  { lia. }
  { autorewrite with sublist. lia. }
Qed.

Lemma call_memset_tuchar:
  forall (shp : share) (tp: type) (pathp: list gfield) (lop: Z) (vp': list val) (p: val)
           (c: int) (len : Z)
           (R': list mpred)
           (np : Z)
           (vp vp'': reptype (nested_field_type tp pathp))
           (e_p e_c e_n : expr)
           Espec Delta P Q R (s: signedness)
   (TCp : typeof e_p = tptr tuchar)
   (TCc : typeof e_c = tint)
   (TCn : typeof e_n = Tint I32 s noattr)
   (Hvar : (var_types Delta) ! _memset = None)
   (Hspec : (glob_specs Delta) ! _memset = Some (snd memset_spec))
   (Hglob : (glob_types Delta) ! _memset =
        Some (type_of_funspec (snd memset_spec)))
   (H:  writable_share shp)
   (Hlop : (0 <= lop)%Z)
   (Hlen: (0 <= len <= Int.max_unsigned)%Z)
   (H0:  nested_field_type tp pathp = tarray tuchar np)
   (Hnp : (lop + len <= np)%Z)
   (H3:  JMeq vp vp')
   (H4:  JMeq vp'' (splice_into_list lop (lop+len) (repeat (Vint c) (Z.to_nat len)) vp'))
   (H5: ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |--
         tc_exprlist Delta [tptr tvoid; tint; tuint] [e_p; e_c; e_n] &&
         local (`(eq (field_address0 tp (ArraySubsc lop :: pathp) p)) (eval_expr e_p)) &&
         local (`(eq (Vint c)) (eval_expr e_c)) &&
         local (`(eq (Vint (Int.repr len))) (eval_expr e_n)) &&
         PROP () (LOCALx Q (SEPx (field_at shp tp pathp vp p :: R')))),
   @semax _ Espec Delta
    (PROPx P (LOCALx Q (SEPx R)))
    (Scall None
             (Evar _memset
               (Tfunction
                (Tcons (tptr tvoid) (Tcons tint (Tcons tuint Tnil)))
                  (tptr tvoid) cc_default))
              [e_p; e_c; e_n])
    (normal_ret_assert (PROPx P (LOCALx Q
     (SEPx (field_at shp tp pathp vp'' p :: R'))))).
Proof.
intros.
assert_PROP (fold_right and True P)
  by (go_lowerx; entailer!).
apply semax_post' with
   (PROPx nil   (LOCALx Q
           (SEPx (field_at shp tp pathp vp'' p :: R'))));
 [ go_lowerx; entailer! | ].
rename H5 into Hpre.
clear H1.
assert_PROP (Zlength vp' = np). {
eapply derives_trans; [apply Hpre | apply andp_left2].
go_lowerx; entailer!.
clear - H6 H4 H3 Hnp H0 Hlen Hlop.
forget (nested_field_type tp pathp) as t0.
subst t0.
simplify_value_fits in H6. destruct H6 as [H6 _].
apply JMeq_eq in H3. subst vp; auto.
} rename H1 into Hvp'.
assert (H5: reptype (tarray tuchar np) = list val) by reflexivity.
rewrite <- H0 in H5.
assert (H99: reptype (nested_field_type tp (ArraySubsc 0 :: pathp)) = val).
 clear - H0. unfold nested_field_type in *; simpl in *.
  destruct (nested_field_rec tp pathp); inv H0. destruct p. subst.
 reflexivity.
assert (H6: exists vpx : list (reptype (nested_field_type tp (ArraySubsc 0 :: pathp))),
                    JMeq vp' vpx).
rewrite H99. eauto.
destruct H6 as [vpx Hvpx].
assert_PROP (legal_nested_field tp pathp). {
  eapply derives_trans; [apply Hpre | apply andp_left2].
go_lowerx; entailer!.
} rename H1 into LNFp.
apply (fun H => JMeq_trans H Hvpx) in H3.
assert (LENvpx: Zlength vpx = np). {
clear - H99 Hvp' Hvpx.
forget val as t. subst t.
apply JMeq_eq in Hvpx. subst; auto.
}
erewrite field_at_Tarray in Hpre; try eassumption; auto; try lia.
rewrite (split3seg_array_at shp tp pathp 0 lop (lop+len)) in Hpre by lia.
rewrite !Z.sub_0_r in Hpre.

assert_PROP (field_compatible0 tp (pathp SUB lop) p /\
            field_compatible0 tp (pathp SUB (lop + len)) p)
  as FC. {
 eapply derives_trans; [apply Hpre | clear Hpre].
 go_lowerx. apply andp_left2. normalize.
 saturate_local.
 apply prop_right.
 split; auto.
}
pose (witness := (shp,
                              field_address0 tp (ArraySubsc lop :: pathp) p,
                              len,  c)).
pose (Frame :=
         array_at shp tp pathp (lop + len) np
              (sublist (lop+len) np vpx) p
          :: array_at shp tp pathp 0 lop (sublist 0 lop vpx) p
              :: R').
eapply semax_pre_post';
  [ | | eapply semax_call_id0_alt with (x:=witness)(P:=nil)(Q:=Q);
       try eassumption;
       try (rewrite ?Hspec, ?Hglob; reflexivity)].
* unfold convertPre. simpl fst; simpl snd.
 rewrite <- (andp_dup (local (tc_environ _))), andp_assoc.
 eapply derives_trans; [ apply andp_derives; [apply derives_refl | apply Hpre] | ].
 rewrite !andp_assoc.
 apply andp_right; [apply andp_left2, andp_left1, derives_refl |].
 eapply derives_trans; [ | apply now_later].
 assert_PROP (field_address0 tp (pathp SUB lop) p <> Vundef) as DEFp.
 {
   unfold tc_exprlist.
   simpl typecheck_exprlist.
   rewrite !denote_tc_assert_andp.
   apply derives_trans with (local (tc_environ Delta) && denote_tc_assert (typecheck_expr Delta e_p) && local ((` (eq (field_address0 tp (pathp SUB lop) p))) (eval_expr e_p))); [solve_andp |].
   go_lowerx.
   eapply derives_trans; [apply typecheck_expr_sound; auto |].
   apply prop_derives; intros.
   rewrite <- H2 in H6.
   intro.
   rewrite H7 in H6.
   revert H6; apply tc_val_Vundef.
 }
 apply andp_left2, andp_left2.
 subst witness. cbv beta iota. simpl @fst; simpl @snd.
 clear Hpre.
 autorewrite with norm1 norm2.

 instantiate (1:=Frame). simpl. unfold env_set, local, lift1, liftx, lift. simpl. intros tau. entailer!.

(* rewrite PROP_combine.*)
(* unfold app at 1.*)
(* instantiate (1:=Frame).
 unfold app at 2.
 go_lowerx.
 apply andp_right.
 apply prop_right.
 unfold make_args'. simpl.
 unfold eval_id, env_set.*)
 rewrite TCp, TCc, TCn.  simpl.
 (*rewrite <- H6, <- H7, <- H8.*)
 unfold PROPx, LOCALx, SEPx, local, liftx, lift1, lift. simpl. unfold liftx, lift. simpl. normalize.

(* split3; try (repeat split; auto; congruence).*)
 apply andp_right.
 { apply prop_right; split3; auto. repeat split; trivial; congruence. }
 subst Frame.
 cancel. (*
 rewrite !field_at_data_at.
 rewrite (data_at_type_changable _ _ _ _ _ H0 H3).
 rewrite (data_at_type_changable _ _ _ _ _ H1 H2).
 sep_apply (array_with_hole_intro shp tuchar lop (lop + len) (*np*)(Zlength vp') vp' (field_address tp pathp p)); [lia | ].
 sep_apply (array_with_hole_intro shq tuchar loq (loq + len) (*nq*)(Zlength contents)  (map Vint contents) (field_address tq pathq q)); [lia | ].
 cancel.

 rewrite PROP_combine.
 unfold app at 1.
 instantiate (1:=Frame).
 unfold app at 2.
 simpl argtypes. unfold eval_exprlist.
 unfold make_args'. simpl map at 2.
 rewrite TCp, TCc, TCn.
 go_lowerx. unfold env_set, eval_id. unfold_lift. simpl.
 autorewrite with gather_prop.
 apply andp_right.
 apply prop_right. split3; try (repeat split; auto; congruence).
 normalize.
 subst Frame.
 cancel.*)
 rewrite array_at_data_at' by  (try solve [clear - FC; intuition]; lia).
 eapply derives_trans; [apply data_at_data_at_ | ].
 eapply derives_trans; [apply data_at__memory_block_cancel | ].
 apply derives_refl'; f_equal.
  unfold nested_field_array_type.
   rewrite nested_field_type_ind, H0. simpl.
  rewrite Z.max_r by lia. lia.
*
 intros. apply andp_left2.
 unfold ifvoid. unfold tptr at 1.
 Intros v. subst witness. cbv beta zeta iota.
 clear Hpre.
 autorewrite with norm1 norm2.
 rewrite PROP_combine.
 unfold app at 1.
 subst Frame.
 simpl map.
 go_lowerx. normalize.
 cancel.
 clear H1 H2.
 assert (H2: exists (vpy : list (reptype (nested_field_type tp (ArraySubsc 0 :: pathp)))),
                  JMeq vp'' vpy).
 rewrite H99. eauto.
destruct H2 as [vpy H8].
erewrite field_at_Tarray; try eassumption; auto; try lia.
apply (JMeq_trans (JMeq_sym H4)) in H8.
clear dependent vp''. clear dependent e_c. clear dependent e_p. clear dependent e_n.
clear dependent Delta.
assert (Zlength vpy = np). {
clear - H0 H8 Hvp' Hnp Hlop Hlen.
generalize dependent vpy.
rewrite nested_field_type_ind, H0. simpl. rewrite reptype_eq; simpl.
intros.
apply JMeq_eq in H8.
subst.
clear H0.
rewrite Zlength_splice_into_list; try lia.
autorewrite with sublist.
auto.
}
rewrite (split3seg_array_at shp tp pathp 0 lop (lop+len) np) by lia.
rewrite !Z.sub_0_r.
replace (sublist 0 lop vpx) with (sublist 0 lop vpy).
2:{
generalize dependent vpy.
generalize dependent vpx.
rewrite H99.
intros.
apply JMeq_eq in H8. apply JMeq_eq in Hvpx.
subst.
apply part1_splice_into_list; lia.
}
replace (sublist (lop+len) np vpx) with (sublist (lop+len) np vpy).
2:{
generalize dependent vpy.
generalize dependent vpx.
rewrite H99.
intros.
apply JMeq_eq in H8. apply JMeq_eq in Hvpx.
subst.
apply part3_splice_into_list; try lia.
rewrite Zlength_repeat. rewrite Z.max_r by lia. lia.
}
cancel.
 rewrite array_at_data_at' by  (try solve [clear - FC; intuition]; lia).
   apply derives_refl'.
   apply equal_f. apply data_at_type_changable.
   unfold nested_field_array_type.
   rewrite nested_field_type_ind, H0.
   unfold tarray; f_equal. clear; lia.
   apply (JMeq_sublist _ _ lop (lop + len) _ _ (eq_sym H99)) in H8.
   eapply JMeq_trans, H8.
   apply eq_JMeq.
   unfold splice_into_list.
   autorewrite with sublist. auto.
Qed.

author: anshumanmohan

repo: CertiGraph-VST