proposition: Lemma Scombine_spec_aux : forall A B C (f : A -> B -> C) g h x v m₁ m₂ l m, NoDupA X.eq l -> S.find (elt:=C) x (fold_left (fun (acc : S.t C) (x : Dom.elt) => match S.find x m₁, S.find x m₂ with | Some v₁, Some v₂ => S.add x (f v₁ v₂) acc | Some v, None => S.add x (g v) acc | None, Some v => S.add x (h v) acc | None, None => acc end) l m) = Some v <-> InA X.eq x l ∧ ((exists v₁ v₂, S.find x m₁ = Some v₁ ∧ S.find x m₂ = Some v₂ ∧ v = f v₁ v₂) ∨ (exists v₁, S.find x m₁ = Some v₁ ∧ S.find x m₂ = None ∧ v = g v₁) ∨ (exists v₂, S.find x m₁ = None ∧ S.find x m₂ = Some v₂ ∧ v = h v₂)) ∨ ((InA X.eq x l ∧ S.find x m₁ = None ∧ S.find x m₂ = None ∨ ¬InA X.eq x l) ∧ S.find x m = Some v).
proof: Proof. intros A B C f g h x v m₁ m₂ l. induction l as [| x' l]; intros m Hnodup; simpl. * rewrite InA_nil. tauto. * inversion_clear Hnodup. rewrite IHl; trivial. clear IHl. split; intros [Hin | Hin]. + left. destruct Hin as [Hl Hin]. split. - now right. - destruct Hin as [Hin | [Hin| Hin]]; tauto. + destruct Hin as [[[Hl [Hin₁ Hin₂]] | Hl] Hm]. - { right. split. + left. repeat split; trivial. now right. + destruct (X.eq_dec x x') as [Heq | Heq]. - rewrite (Sfind_compat Heq) in Hin₁; rewrite (Sfind_compat Heq) in Hin₂. rewrite Hin₁, Hin₂ in Hm. assumption. - destruct (S.find x' m₁), (S.find x' m₂); trivial; apply S.find_2, S.add_3, S.find_1 in Hm; trivial; symmetry; assumption. } - { destruct (X.eq_dec x x') as [Heq | Heq]. + destruct (S.find x' m₁) as [v₁ |] eqn:Hv₁, (S.find x' m₂) as [v₂ |] eqn:Hv₂. - left. split; try (left; assumption). left. exists v₁, v₂. repeat rewrite (Sfind_compat Heq). repeat split; trivial. cut (Some v = Some (f v₁ v₂)). intro Hfv; inversion Hfv; reflexivity. rewrite <- Hm. apply S.find_1, S.add_1. symmetry. assumption. - left. split; try (left; assumption). right; left. exists v₁. repeat rewrite (Sfind_compat Heq). repeat split; trivial. cut (Some v = Some (g v₁)). intro Hfv; inversion Hfv; reflexivity. rewrite <- Hm. apply S.find_1, S.add_1. symmetry. assumption. - left. split; try (left; assumption). do 2 right. exists v₂. repeat rewrite (Sfind_compat Heq). repeat split; trivial. cut (Some v = Some (h v₂)). intro Hfv; inversion Hfv; reflexivity. rewrite <- Hm. apply S.find_1, S.add_1. symmetry. assumption. - right. split; trivial. left. repeat rewrite (Sfind_compat Heq). repeat split; trivial. now left. + right. split. - right. intro Habs. inversion_clear Habs; contradiction. - destruct (S.find x' m₁), (S.find x' m₂); trivial; apply S.find_2, S.add_3, S.find_1 in Hm; trivial; symmetry; assumption. } + destruct Hin as [Hl Hin]. inversion_clear Hl. - right. rewrite H1 at 4. split; try now right. destruct Hin as [[v₁ [v₂ [Hin₁ [Hin₂ Hv]]]] | [[v₁ [Hin₁ [Hin₂ Hv]]] | [v₂ [Hin₁ [Hin₂ Hv]]]]]; rewrite (Sfind_compat H1) in Hin₁; rewrite (Sfind_compat H1) in Hin₂; rewrite Hin₁, Hin₂; subst v; apply S.find_1, S.add_1; symmetry; assumption. - left. split; assumption. + destruct Hin as [[[Hin [Hin₁ Hin₂]] | Hin] Hm]. - { right. inversion_clear Hin. + rewrite (Sfind_compat H1) in Hin₁; rewrite (Sfind_compat H1) in Hin₂; rewrite Hin₁, Hin₂. split; trivial. right. rewrite H1. assumption. + assert (¬X.eq x x'). { intro Habs. apply H. rewrite <- Habs. assumption. } split; try tauto. destruct (S.find x' m₁), (S.find x' m₂); trivial; apply S.find_1, S.add_2, S.find_2; trivial; symmetry; assumption. } - { right. split. + right. intro Habs. apply Hin. now right. + assert (¬X.eq x x'). { intro Habs. apply Hin. now left. } destruct (S.find x' m₁), (S.find x' m₂); trivial; apply S.find_1, S.add_2, S.find_2; trivial; symmetry; assumption. } Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface