Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.

minimal_hitting_sets.v

From mathcomp Require Import ssreflect fintype finset seq ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(******************************************************************************

Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.

Checked with Coq 8.8.0 and MathComp 1.7.0.

References:

* T. Imai, "One-line hack of knuth's algorithm for minimal hitting set
  computation with ZDDs," vol. 2015-AL-155, no. 15, Nov. 2015, pp. 1-3.
  [Online]. Available: <http://id.nii.ac.jp/1001/00145799/>.

*******************************************************************************)



(******************************************************************************)

Section Minimality.

Variable U : finType.
Variable p : {set U} -> bool.
Hypothesis p_monotone : forall (A B : {set U}), (A \subset B) -> p A -> p B.

(* ssreflect的にはこれもboolで定義したほうが良い? *)
Definition Minimal (X : {set U}) :=
  p X /\ (forall (Y : {set U}), p Y -> Y \subset X -> Y = X).

Definition Irreducible (X : {set U}) :=
  p X && all (fun x => ~~ p (X :\ x)) (enum X).


Lemma Irreducible_to_Minimal (X : {set U}) : Irreducible X -> Minimal X.
case /andP => pX irrX.
apply: conj => //.
move=> Y pY Y_sub_X.
apply /eqtype.eqP.

move: (Y_sub_X).
rewrite subEproper.
move /orP.
case => //.
move=> Y_proper_X.

have [x x_in_X x_notin_Y] : exists2 x, x \in X & x \notin Y.
-move: Y_proper_X.
 move/ properP.
 case.
 move=> _.
 by [].

have Y_sub_Xx : Y \subset X :\ x.
-apply /subsetP.
 move=> y y_in_Y.
 apply /setD1P.
 apply: conj.
 +apply /negP.
  move /eqtype.eqP.
  move=> y_eq_x.
  move: x_notin_Y.
  move /negP.
  apply /negP.
  rewrite -y_eq_x.
  by apply: y_in_Y.
 +move: Y_sub_X.
  move /subsetP.
  apply.
  by apply: y_in_Y.

have pXx : p (X :\ x).
-by apply: (p_monotone Y_sub_Xx) pY.

have not_pXx : ~ p (X :\ x).
-apply /negP.
 move: irrX.
 move/ allP.
 apply.
 rewrite mem_enum.
 by apply: x_in_X.

by [].
Qed.


Lemma Minimal_to_Irreducible (X : {set U}) : Minimal X -> Irreducible X.
Proof.
case => pX minX.
apply /andP.
apply: conj => //.
apply /allP.
move=> x.
rewrite mem_enum.
move=> x_in_X.
apply /negP => pXx.

have Xx_sub_X : (X :\ x) \subset X.
-apply /subsetP.
 move=> x0.
 move /setD1P.
 by case.

have Xx_eq_X : X :\ x = X.
-by apply: (minX (X :\ x) pXx Xx_sub_X).

have: X :\ x :!=: X.
-apply: proper_neq.
 by apply: properD1.

apply /idP.
apply /eqtype.eqP.
by apply: Xx_eq_X.
Qed.


Fixpoint shrink_iter (X : {set U}) (xs : seq U) : {set U} :=
  match xs with
  | [::] => X
  | x :: xs' =>
      if p (X :\ x) then
        shrink_iter (X :\ x) xs'
      else
        shrink_iter X xs'
  end.

Definition shrink X := shrink_iter X (enum X).

Lemma shrink_iter_subset : forall xs X, shrink_iter X xs \subset X.
Proof.
move=> xs.
elim: xs => //.
move=> a xs IH X.
rewrite /=.
case: (p (X :\ a)).
+by apply: subset_trans (IH (X :\ a)) (subsetDl X [set a]).
+by apply: IH.
Qed.

Lemma shrink_subset : forall X, shrink X \subset X.
Proof.
move=> X.
apply: shrink_iter_subset.
Qed.

Lemma shrink_iter_p : forall xs X, p X -> p (shrink_iter X xs).
Proof.
move=> xs.
elim: xs => //.
move=> a xs IH X pX.
rewrite /=.
case: (@idP (p (X :\ a))).
+move=> pXa.
 by apply: IH pXa.
+move=> not_pXa.
 by apply: IH pX.
Qed.

Lemma shrink_p : forall X, p X -> p (shrink X).
Proof.
move=> X.
apply: shrink_iter_p.
Qed.

Lemma shrink_iter_irreducible
  : forall a xs (a_in_xs : a \in xs) X (pX : p X) (a_in_shrink_X_xs : a \in shrink_iter X xs),
      ~~ p (shrink_iter X xs :\ a).
Proof.
move=> a xs.
elim: xs => //.
move=> x xs IH a_in_xxs X pX a_in_shrink_X_xxs.
move: a_in_xxs.
rewrite in_cons.
move /orP; case.
-move /eqtype.eqP => a_eq_x.
 case: (@idP (p (X :\ a))).
 +rewrite a_eq_x.
  move=> pXx.
  apply /negP => _.
  move: a_in_shrink_X_xxs.
  rewrite a_eq_x.
  have lem : shrink_iter X (x :: xs) = shrink_iter (X :\ x) xs.
  *by rewrite /shrink_iter (pXx : p (X :\ x) = true).
  rewrite lem.
  move=> H. (* H : x \in shrink_iter (X :\ x) xs *)
  have: x \in (X :\ x).
  *move: (shrink_iter_subset xs (X :\ x)).
   move /subsetP.
   apply.
   by apply: H.
  move /setDP.
  case => _.
  apply /idP.
  by apply: set11.
 +rewrite a_eq_x.
  move=> not_pXx.
  apply /negP => H. (* H : p (shrink_iter X (x :: xs) :\ x) *)
  apply: not_pXx.
  have lem : shrink_iter X (x :: xs) :\ x \subset (X :\ x).
  *apply: setSD.
   by apply: shrink_iter_subset.
  apply: (p_monotone lem).
  by apply: H.
-move=> a_in_xs.
 case: (@idP (p (X :\ x))).
 +move=> pXx.
  apply /negP.
  move=> H. (* p (shrink_iter X (x :: xs) :\ a) *)
  have lem : shrink_iter X (x :: xs) = shrink_iter (X :\ x) xs.
  *by rewrite /shrink_iter pXx.
  have a_in_shrink_Xx_xs : a \in shrink_iter (X :\ x) xs.
  *move: a_in_shrink_X_xxs; by rewrite lem.
  move: (IH a_in_xs (X :\ x) pXx a_in_shrink_Xx_xs).
  move /negP.
  apply /negP.
  rewrite -lem.
  by apply: H.
 +move /negP /negbTE => not_pXx.
  apply /negP => H. (* H : p (shrink_iter X (x :: xs) :\ a) *)
  have lem: shrink_iter X (x :: xs) = shrink_iter X xs.
  *by rewrite /shrink_iter not_pXx.
  have a_in_shrink_X_xs : a \in shrink_iter X xs.
  *rewrite -lem.
   by apply: a_in_shrink_X_xxs.
  move: (IH a_in_xs X pX a_in_shrink_X_xs).
  move /negP.
  apply /negP.
  rewrite -lem.
  by apply: H.
Qed.

Lemma shrink_irreducible : forall X, p X -> Irreducible (shrink X).
Proof.
move=> X pX.
apply /andP.
apply: conj.
-by apply: shrink_p.
-apply /allP.
 move=> a.
 rewrite mem_enum => a_in_shrink_X.
 apply: shrink_iter_irreducible.
 +rewrite mem_enum.
  move: (shrink_subset X).
  move /subsetP.
  apply.
  by apply: a_in_shrink_X.
 +by [].
 +by apply: a_in_shrink_X.
Qed.

Lemma shrink_minimal : forall X, p X -> Minimal (shrink X).
Proof.
move=> X pX.
apply: Irreducible_to_Minimal.
by apply: shrink_irreducible.
Qed.

End Minimality.

(******************************************************************************)

Section HittingSets.

Variable U : finType.

Definition hit (A B : {set U}) : bool
  := (A :&: B) :!=: set0.

Definition is_hitting_set (F : {set {set U}}) (A : {set U}) : bool
  := all (hit A) (enum F).

Lemma is_hitting_set_monotone (F : {set {set U}}) (A B : {set U}) (A_sub_B : A \subset B)
  : is_hitting_set F A -> is_hitting_set F B.
Proof.
move=> H.
rewrite /is_hitting_set.
apply: sub_all.
Existential 1 := (hit A).
-rewrite /subpred.
 move=> x.
 rewrite /hit.
 have: A :&: x \subset B :&: x.
 +by apply: setSI A_sub_B.
 by apply: subset_neq0.
-by apply: H.
Qed.

Lemma is_hitting_set_weaken (F G : {set {set U}}) (F_sub_G : F \subset G) (A : {set U})
  : is_hitting_set G A -> is_hitting_set F A.
Proof.
move=> A_hit_G.
apply /allP.
move=> X.
rewrite mem_enum.
move=> X_in_F.
move: A_hit_G.
move /allP.
apply.
rewrite mem_enum.
move: F_sub_G.
move /subsetP.
apply.
by apply: X_in_F.
Qed.


(*
is_minimal_hitting_set を Minimal で定義し、 minimal_hitting_sets を Irreducible
で定義してしまっているので、相互に変換が必要になってしまっていて良くない。
*)

Definition is_minimal_hitting_set (F : {set {set U}}) : {set U} -> Prop
  := Minimal (is_hitting_set F).

Definition minimal_hitting_sets (F : {set {set U}}) : {set {set U}}
  := [set A | Irreducible (is_hitting_set F) A].

Lemma mhs_unpack F A : A \in minimal_hitting_sets F -> is_minimal_hitting_set F A.
Proof.
move=> A_in_mhsF.
apply: Irreducible_to_Minimal.
-by apply: is_hitting_set_monotone.
-rewrite -in_set.
 by apply: A_in_mhsF.
Qed.

Lemma mhs_pack F A : is_minimal_hitting_set F A -> A \in minimal_hitting_sets F.
Proof.
move=> A_minhit_F.
rewrite in_set.
apply: Minimal_to_Irreducible.
apply: A_minhit_F.
Qed.


Definition nosupset (F G : {set {set U}}) : {set {set U}} :=
  [set A | (A \in F) && all (fun (B : {set U}) => ~~ (B \subset A)) (enum G) ].

Notation "A :↘: B" := (nosupset A B)
  (at level 50, left associativity) : set_scope.


Lemma lemma (F G : {set {set U}}) (B : {set U}) (B_in_mhsF : B \in minimal_hitting_sets F)
  : (all (fun (A : {set U}) => ~~(A \subset B)) (enum (minimal_hitting_sets (F :|: G))))
  = (B \notin minimal_hitting_sets (F :|: G)).
Proof.
apply /idP /idP.
-move /allP.
 move=> L.
 apply /negP.
 move /mhs_unpack.
 move=> B_minhit_FG.
 have: ~~(B \subset B).
 +apply: L.
  *rewrite mem_enum.
   apply: mhs_pack.
   by apply: B_minhit_FG.
  *move /negP.
   apply /negP.
   by [].
-move /negP.
 move=> not_B_minhit_FG.
 apply /allP.
 move=> A.
 rewrite mem_enum.
 move /mhs_unpack.
 move=> A_minhit_FG.
 apply /negP.
 move=> A_sub_B.
 apply: not_B_minhit_FG.
 apply: mhs_pack.
 have s_minhit_F : is_minimal_hitting_set F (shrink (is_hitting_set F) A).
 +apply: shrink_minimal.
  *by apply: is_hitting_set_monotone.
  *move: (proj1 A_minhit_FG) => A_hit_FG.
   apply: (@is_hitting_set_weaken F (F :|: G)).
   *apply /subsetP => x x_in_A.
    apply /setUP.
    by apply: or_introl.
   *by apply: A_hit_FG.
 have s_sub_A : shrink (is_hitting_set F) A \subset A.
 +by apply: shrink_subset.
 have A_hit_F : is_hitting_set F A.
 +apply: (is_hitting_set_monotone s_sub_A).
  move: s_minhit_F.
  by case.
 have A_eq_B : A = B.
 +by apply: proj2 (mhs_unpack B_in_mhsF) A A_hit_F A_sub_B.
 rewrite -A_eq_B.
 by apply: A_minhit_FG.
Qed.


(* f# ↘ (f∪g)# = f# ＼ (f∪g)# *)
Theorem main_theorem (F G : {set {set U}})
  : minimal_hitting_sets F :↘: minimal_hitting_sets (F :|: G)
  = minimal_hitting_sets F :\: minimal_hitting_sets (F :|: G).
Proof.
apply /setP.
move=> B.
apply /idP /idP.
-rewrite in_set.
 case /andP => B_in_mhsF H.
 apply /setDP.
 apply: conj.
 +by apply: B_in_mhsF.
 +by rewrite -(lemma G B_in_mhsF).
-move /setDP.
 case.
 move=> B_in_mhsF B_notin_mhsFG.
 rewrite in_set.
 apply /andP.
 apply: conj.
 +by apply: B_in_mhsF.
 +by rewrite (lemma G B_in_mhsF).
Qed.

End HittingSets.