proposition: Lemma refine_M_hrel_elements : refines (M_hrel ==> list_R (prod_R eq rAC)) (@M.elements A) (@M.elements C).
proof: Proof. apply refines_abstr => m m'; rewrite !refinesE => ref_m. set em := M.elements m; set em' := M.elements m'. have: ((forall k, {e | InA (M.eq_key_elt (elt:=A)) (k, e) em} <=> {e' | InA (M.eq_key_elt (elt:=C)) (k, e') em'}) * (forall k e e', InA (M.eq_key_elt (elt:=A)) (k, e) em -> InA (M.eq_key_elt (elt:=C)) (k, e') em' -> rAC e e'))%type. { split. { move=> k; split. { move=> [e He]. have Hkm : M.In k m; [by exists e; apply M.elements_2|]. have /MIn_sig [e' He'] := proj1 (fst ref_m k) Hkm. exists e'; by apply M.elements_1. } move=> [e' He']. have Hkm' : M.In k m'; [by exists e'; apply M.elements_2|]. have /MIn_sig [e He] := proj2 (fst ref_m _) Hkm'. exists e; by apply M.elements_1. } move=> k e e' He He'. move: (M.elements_2 He) (M.elements_2 He'); apply (snd ref_m). } move: (M.elements_3 m) (M.elements_3 m'); rewrite -/em -/em'. clearbody em em'; move: {m m' ref_m} em em'. elim=> [|h t IH]; case=> [|h' t'] //=. { move/SortedT_dec=> _ _ [Heq _]. move: (ifft2 (Heq h'.1)); elim. { by move=> h'2 /InA_nil. } by exists h'.2; apply InA_cons_hd; split; [apply E.eq_refl|]. } { move=> _ _ [Heq _]; move: (ifft1 (Heq h.1)); elim. { by move=> h2 /InA_nil. } by exists h.2; apply InA_cons_hd; split; [apply E.eq_refl|]. } move=> Sht Sht' [Hht1 Hht2]. have St := proj1 (Sorted_inv Sht); have St' := proj1 (Sorted_inv Sht'). have Hhh' : E.eq h.1 h'.1. { apply MultinomOrd.intro_eq; apply/negbTE/negP. { move=> Hhh'1. have Hh1 : {e | InA (M.eq_key_elt (elt:=A)) (h.1, e) (h :: t)}. { by exists h.2; apply InA_cons_hd; split; [apply E.eq_refl|]. } have [e' He'] := (ifft1 (Hht1 _) Hh1). have Hhh'1' : M.lt_key (h.1, e') h'; [by simpl|]. by apply (Sorted_InA_not_lt_hd Sht' He'). } move=> Hh'h1. have Hh1 : {e | InA (M.eq_key_elt (elt:=C)) (h'.1, e) (h' :: t')}. { by exists h'.2; apply InA_cons_hd; split; [apply E.eq_refl|]. } move: (ifft2 (Hht1 _) Hh1) => [e He]. have Hh'h1' : M.lt_key (h'.1, e) h; [by simpl|]. by apply (Sorted_InA_not_lt_hd Sht He). } constructor 2. apply: prod_RI. split; [by move: Hhh' => /mnmc_eq_seqP /eqP|]. { apply (Hht2 h.1); apply InA_cons_hd. { by split; [apply E.eq_refl|]. } by move: Hhh' => /mnmc_eq_seqP/eqP->; split; [apply E.eq_refl|]. } apply (IH _ St St'). constructor=> k; specialize (Hht1 k); specialize (Hht2 k). { split. { move=> [e He]. have Ht1 : {e | InA (M.eq_key_elt (elt:=A)) (k, e) (h :: t)}. { by exists e; apply InA_cons_tl. } case (ifft1 Hht1 Ht1) => e' He'. exists e'. have /InA_cons[Heq0|//] := He'. move: (Sorted_InA_tl_lt Sht He); move /E.lt_not_eq. move: Hhh'; move/mnmc_eq_seqP/eqP-> => Heq; exfalso; apply Heq. move: (proj1 Heq0); move/mnmc_eq_seqP/eqP => /= ->. by apply E.eq_refl. } move=> [e' He']. have Ht1 : { e' | InA (M.eq_key_elt (elt:=C)) (k, e') (h' :: t')}. { by exists e'; apply InA_cons_tl. } elim (ifft2 Hht1 Ht1) => e He. exists e. have /InA_cons[Heq0|//] := He. move: (Sorted_InA_tl_lt Sht' He'); move /E.lt_not_eq. move: Hhh'; move/mnmc_eq_seqP/eqP<- => Heq; exfalso; apply Heq. move: (proj1 Heq0); move/mnmc_eq_seqP/eqP => /= ->. by apply E.eq_refl. } by move=> e e' He He'; apply Hht2; apply InA_cons_tl. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)