Skip to content

Instantly share code, notes, and snippets.

@msakai
Last active June 5, 2018 10:06
Show Gist options
  • Save msakai/fb01110e8b03379614a9b1c2463beb52 to your computer and use it in GitHub Desktop.
Save msakai/fb01110e8b03379614a9b1c2463beb52 to your computer and use it in GitHub Desktop.
Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# \ (f∪g)#'.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment