proposition: Lemma merge_inv : equivalence _ eqA -> (reflexive _ eqB) -> forall (l1 l2 : list (A*B)), (forall a1 a1' b1 c1, In (a1,b1) l1 -> In (a1',c1) l1 -> eq_bool a1 a1' = true -> eqB_bool b1 c1 =true) -> (forall a2 a2' b2 c2, In (a2,b2) l2 -> In (a2',c2) l2 -> eq_bool a2 a2' = true -> eqB_bool b2 c2 = true) -> match merge l1 l2 with | Some l => (forall a a' b c, In (a,b) l -> In (a',c) l -> eq_bool a a' = true -> eqB_bool b c = true) | None => True end.
proof: Proof. intros eq_proof RB; fix merge_inv 2. intros l1 l2; case l2; clear l2. intros Inv1 _; exact Inv1. intros p l2; case p; clear p; simpl. intros a2 b2 Inv1 Inv2. case_eq (find a2 l1). intros b H; case_eq (eqB_bool b2 b); [intro b2_eq_b | intro b2_diff_b]. apply merge_inv. exact Inv1. intros a a' b' c ab_in_l2 ac_in_l2; apply (Inv2 a a' b' c). right; assumption. right; assumption. exact I. intro H; apply merge_inv; simpl. intros a a' b' c [H1 | ab_in_l1] [H2 | ac_in_l1]. injection H1; injection H2; intros; subst a a' b' c. generalize (eqB_bool_ok b2 b2); case (eqB_bool b2 b2). intros _; reflexivity. intro b2_diff_b2; apply False_rect; apply b2_diff_b2; apply RB. injection H1; intros; subst a b'. apply False_rect; apply (find_not_found c l1 H H3 ac_in_l1). injection H2; intros; subst a' c. apply False_rect; refine (find_not_found (a' := a) b' l1 H _ ab_in_l1). generalize (eq_bool_ok a2 a) (eq_bool_ok a a2); rewrite H3; case (eq_bool a2 a). intros _ _; reflexivity. intros a2_diff_a a_eq_a2; apply False_rect; apply a2_diff_a; destruct eq_proof as [_ _ Se]; apply Se; assumption. apply Inv1; assumption. intros a a' b' c ab_in_l2 ac_in_l2; apply (Inv2 a a' b' c). right; assumption. right; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)