proposition: Lemma merge_correct : equivalence _ eqA -> (reflexive _ eqB) -> forall (l1 l2 : list (A * B)), match merge l1 l2 with | Some l => (forall a b, find a l1 = Some b -> find a l = Some b) /\ (forall a b, find a l2 = Some b -> (exists b', find a l = Some b' /\ eqB_bool b b' = true)) /\ (forall a b, find a l = Some b -> (find a l1 = Some b \/ (find a l1 = None /\ find a l2 = Some b))) | None => exists a, exists a', exists b1, exists b2, (find a l1 = Some b1 \/ In (a,b1) l2) /\ In (a',b2) l2 /\ eq_bool a a' = true /\ eqB_bool b2 b1 = false end.
proof: Proof. intros eq_proof RB; fix merge_correct 2. intros l1 l2; case l2; clear l2; simpl. repeat split. intros a b H; exact H. intros a b H; discriminate. intros a b H; left; exact H. intros p l2; case p; clear p; intros a2 b2; simpl. case_eq (find a2 l1). intros b F; case_eq (eqB_bool b2 b). intro b2_eq_b. generalize (merge_correct l1 l2). case (merge l1 l2). intros l H; case H; clear H. intros H1 H; case H; clear H. intros H2 H3. repeat split. assumption. intros a b'; case_eq (eq_bool a a2). intros a_eq_a2 H; injection H; clear H; intro H; subst b'. exists b; split. apply H1; rewrite <- F; apply eq_find_eq; assumption. assumption. intros a_diff_a2 F'; apply H2; assumption. intros a b' F'; case_eq (eq_bool a a2). intros a_eq_a2. generalize (H3 _ _ F'); rewrite (eq_find_eq eq_proof l1 a_eq_a2). intro FF; case FF; clear FF; intro F''. left; assumption. case F''; clear F''; intros F'' _; rewrite F in F''; discriminate. intro a_diff_a2; apply H3; assumption. intros [a [a' [b1 [b1' [[F' | F'] [F'' [a_eq_a' b1_diff_b1']]]]]]]; exists a; exists a'; exists b1; exists b1'; repeat split. left; assumption. right; assumption. assumption. assumption. do 2 right; assumption. right; assumption. assumption. assumption. intro b2_diff_b. exists a2; exists a2; exists b; exists b2; repeat split. left; assumption. left; reflexivity. generalize (eq_bool_ok a2 a2); case (eq_bool a2 a2). intros _; reflexivity. intro a2_diff_a2; apply False_rect; apply a2_diff_a2; destruct eq_proof as [R _ _]; apply R. assumption. intro F. generalize (merge_correct ((a2,b2) :: l1) l2). case (merge ((a2,b2) :: l1) l2); simpl. intros l H; case H; clear H. intros H1 H; case H; clear H. intros H2 H3. repeat split. intros a b F'; generalize (H1 a b); case_eq (eq_bool a a2). intro a_eq_a2; rewrite (eq_find_eq eq_proof l1 a_eq_a2) in F'; rewrite F in F'; discriminate. intros _ H1a; apply H1a; assumption. intros a b'; case_eq (eq_bool a a2). intros a_eq_a2 H; injection H; clear H; intro H; subst b'. exists b2; split. generalize (H1 a b2); rewrite a_eq_a2; intro H1a; apply H1a; reflexivity. 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. intros a_diff_a2 F'; exact (H2 a b' F'). intros a b F'; generalize (H3 a b F'); case_eq (eq_bool a a2). intros a_eq_a2 [F'' | FF]. right; split. rewrite (eq_find_eq eq_proof l1 a_eq_a2); assumption. assumption. case FF; intros F'' _; discriminate. intros _ H; exact H. intros [a [a' [b1 [b1' [[F' | F'] [F'' [a_eq_a' b1_diff_b1']]]]]]]. revert F'; case_eq (eq_bool a a2). intros a_eq_a2 F'; injection F'; clear F'; intro; subst b1. exists a2; exists a'; exists b2; exists b1'; repeat split. right; left; reflexivity. right; assumption. generalize (eq_bool_ok a2 a'); case (eq_bool a2 a'). intros _; reflexivity. intro a2_diff_a'; apply False_rect; apply a2_diff_a'. destruct eq_proof as [Re Te Se]. apply Te with a. apply Se; generalize (eq_bool_ok a a2); rewrite a_eq_a2; intro H; exact H. generalize (eq_bool_ok a a'); rewrite a_eq_a'; intro H; exact H. assumption. intros a_diff_a2 F'; exists a; exists a'; exists b1; exists b1'; repeat split. left; assumption. right; assumption. assumption. assumption. exists a; exists a'; exists b1; exists b1'; repeat split. do 2 right; assumption. right; assumption. assumption. assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)