diff.v

Require Import List.
Require Import Bool.
Require Import Bool.Sumbool.

Ltac find_if :=
  match goal with
  | H:context[if ?X then _ else _] |- _ => destruct X as ()_eqn
  | |- context[if ?X then _ else _] => destruct X as ()_eqn
  end.

Ltac negb_tf :=
  repeat match goal with
  | H:negb _ = true  |- _ => apply negb_true_iff in H
  | H:negb _ = false |- _ => apply negb_false_iff in H
  | |- negb _ = true => apply negb_true_iff
  | |- negb _ = false => apply negb_false_iff
  end.

Section InBool.

Variable A : Type.
Hypothesis Aeq_dec : forall a b : A, {a = b} + {a <> b}.

Definition in_bool (a : A)(l : list A) : bool :=
  proj1_sig (bool_of_sumbool (in_dec Aeq_dec a l)).

Definition not_in_bool a l := negb (in_bool a l).

Lemma in_bool_impl_in : forall a l, in_bool a l = true -> In a l.
Proof.
unfold in_bool. intros a l H.
destruct (in_dec Aeq_dec a l); simpl in *; congruence.
Qed.

Lemma in_impl_in_bool : forall a l, In a l -> in_bool a l = true.
Proof.
unfold in_bool. intros a l H.
destruct (in_dec Aeq_dec a l); simpl in *; congruence.
Qed.

Lemma not_in_impl_in_bool : forall a l, in_bool a l = false -> ~ In a l.
Proof.
intros a l H.
apply <- not_true_iff_false in H.
auto using in_impl_in_bool.
Qed.

Lemma not_in_bool_impl_in : forall a l, ~ In a l -> in_bool a l = false.
Proof.
auto using not_true_is_false, in_bool_impl_in.
Qed.

Ltac toi :=
  match goal with
  | |- in_bool _ _ = true  => apply in_impl_in_bool
  | |- in_bool _ _ = false => apply not_in_bool_impl_in
  | _ => idtac
  end.

Ltac tob :=
  repeat match goal with
  | H:in_bool _ _ = true  |- _ => apply in_bool_impl_in in H
  | H:in_bool _ _ = false |- _ => apply not_in_impl_in_bool in H
  | _ => idtac
  end.

Ltac btoi := toi; tob.

Theorem in_bool_eq : forall a l, in_bool a (a :: l) = true.
Proof.
auto using in_impl_in_bool, in_eq.
Qed.

Theorem in_bool_cons : forall a b l, in_bool b l = true -> in_bool b (a :: l) = true.
Proof.
intros.
btoi. auto using in_cons.
Qed.

Theorem in_bool_nil : forall a, in_bool a nil = false.
Proof.
intros.
btoi. auto using in_nil.
Qed.

Lemma in_bool_inv : forall a b l, in_bool a (b :: l) = true -> a = b \/ in_bool a l = true.
Proof.
intros.
btoi.
destruct (in_inv H).
 intuition.
 
 right. toi. auto.
Qed.

Lemma in_bool_app_or : forall l m a,
  in_bool a (l ++ m) = true -> in_bool a l = true \/ in_bool a m = true.
Proof.
intros. btoi.
destruct (in_app_or l m a H).
 left. btoi. auto.
 right. btoi. auto.
Qed.

Lemma in_bool_or_app : forall l m a,
  in_bool a l = true \/ in_bool a m = true -> in_bool a (l ++ m) = true.
Proof.
intros.
destruct H; btoi; auto using in_or_app.
Qed.

Lemma filter_in_bool : forall x l f,
  in_bool x (filter f l) = true <-> in_bool x l = true /\ f x = true.
Proof.
split.
 intro H.
 btoi.
 apply filter_In in H.
 split; btoi; tauto.

 intro H.
 destruct H.
 btoi. apply filter_In. tauto.
Qed.

End InBool.


Section Diff.

Variable A : Type.
Hypothesis Aeq_dec : forall a b : A, {a = b} + {a <> b}.

Definition diff (xs ys : list A) := filter (fun a => not_in_bool A Aeq_dec a ys) xs.

Infix "\\" := diff (right associativity, at level 55).

Theorem diff_app_distr_r : forall xs ys zs, (xs ++ ys) \\ zs = (xs \\ zs) ++ (ys \\ zs).
Proof with simpl in *; try congruence.
intros xs ys zs.
induction xs...
 find_if...
Qed.

Theorem diff_app_diff : forall xs ys zs, xs \\ (ys ++ zs) = (xs \\ ys) \\ zs.
Proof with simpl in *; subst; try congruence.
intros xs ys zs.
induction xs...
 repeat find_if; unfold not_in_bool in *...
  find_if...
  unfold not_in_bool in Heqb1.
  negb_tf.
  apply <- not_true_iff_false in Heqb.
  exfalso.
  auto using in_bool_or_app.

  negb_tf.
  apply <- not_true_iff_false in Heqb.
  exfalso.
  auto using in_bool_or_app.

  find_if...
  unfold not_in_bool in *.
  negb_tf.
  apply in_bool_app_or in Heqb.
  destruct Heqb...
Qed.

Theorem diff_comm : forall xs ys zs, (xs \\ ys) \\ zs = (xs \\ zs) \\ ys.
Proof with simpl in *; subst; try congruence.
intros xs ys zs.
induction xs...
 find_if...
 find_if...
 find_if...
 find_if...
 find_if...
Qed.

Lemma diff_nil : forall xs, xs \\ nil = xs.
Proof with simpl in *; try congruence.
induction xs...
Qed.

Theorem app_diff_diff_app : forall xs ys zs ws,
  xs \\ ws = xs -> ys \\ zs = ys -> (xs ++ ys) \\ (zs ++ ws) = (xs \\ zs) ++ (ys \\ ws).
Proof with simpl in *; try congruence.
intros xs ys zs ws H H0.
rewrite diff_app_distr_r.
repeat rewrite diff_app_diff.
rewrite H0.
rewrite diff_comm.
rewrite H...
Qed.

Lemma in_diff : forall xs ys,
  (forall x, in_bool A Aeq_dec x ys = true -> in_bool A Aeq_dec x xs = false) -> xs \\ ys = xs.
Proof with simpl in *; try congruence.
intros xs ys H.
induction xs...
 find_if...
  f_equal.
  apply IHxs.
  intros x H0.
  apply H in H0.
  apply not_true_iff_false in H0.
  apply not_true_iff_false.
  auto using in_bool_cons.

  unfold not_in_bool in *.
  negb_tf.
  apply H in Heqb.
  apply not_true_iff_false in Heqb.
  exfalso. auto using in_bool_eq.
Qed.

End Diff.