proposition: Lemma refine_M_hrel_map2 : refines ((option_R rAC ==> option_R rAC ==> option_R rAC) ==> M_hrel ==> M_hrel ==> M_hrel) (@M.map2 A A A) (@M.map2 C C C).
proof: Proof. apply refines_abstr => f f' ref_f. apply refines_abstr => m1 m1' ref_m1. apply refines_abstr => m2 m2' ref_m2. have Hf : forall k, option_R rAC (f (M.find k m1) (M.find k m2)) (f' (M.find k m1') (M.find k m2')). { move=> k; apply refinesP; eapply refines_apply; [eapply refines_apply|]. { apply ref_f. } { eapply refines_apply; [|by apply ref_m1]. eapply refines_apply; [apply refine_M_hrel_find|by apply trivial_refines]. } eapply refines_apply; [|by apply ref_m2]. eapply refines_apply; [apply refine_M_hrel_find|by apply trivial_refines]. } rewrite refinesE; rewrite refinesE in ref_m1, ref_m2; split. { move=> k; split. { move=> Hk; have Hor := M.map2_2 Hk; move: Hk => [e He]. apply M.find_1 in He; rewrite (M.map2_1 _ Hor) in He. move: (Hf k); rewrite He; case_eq (f' (M.find k m1') (M.find k m2')) => //. move=> e' He' _; exists e'; apply M.find_2; rewrite -He'; apply M.map2_1. by destruct Hor as [Hk|Hk]; [left; apply ref_m1|right; apply ref_m2]. by move=> _ K; inversion_clear K. } move=> Hk; have Hor := M.map2_2 Hk; move: Hk => [e He]. apply M.find_1 in He; rewrite (M.map2_1 _ Hor) in He. move: (Hf k); rewrite He; case_eq (f (M.find k m1) (M.find k m2)) => //. move=> e' He' _; exists e'; apply M.find_2; rewrite -He'; apply M.map2_1. by destruct Hor as [Hk|Hk]; [left; apply ref_m1|right; apply ref_m2]. by move=> _ K; inversion_clear K. } move=> k e e' He He'; move: (M.find_1 He) (M.find_1 He') (Hf k). case_eq (M.find k m1) => [e1|] He1. { rewrite M.map2_1; [|by left; exists e1; apply M.find_2]. rewrite M.map2_1; [|by left; apply ref_m1; exists e1; apply M.find_2]. by rewrite He1 => -> -> H; inversion_clear H. } case_eq (M.find k m2) => [e2|] He2. { rewrite M.map2_1; [|by right; exists e2; apply M.find_2]. rewrite M.map2_1; [|by right; apply ref_m2; exists e2; apply M.find_2]. by rewrite He1 He2 => -> -> H; inversion_clear H. } elim (@map2_2_dec _ _ _ m1 m2 k f); [| |by exists e]. { by move/MIn_sig=> [e'1 He'1]; apply M.find_1 in He'1; rewrite He'1 in He1. } by move/MIn_sig=> [e'2 He'2]; apply M.find_1 in He'2; rewrite He'2 in He2. 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)