# Library GraphTheory.set_tac

From mathcomp Require Import all_ssreflect.

Require Import preliminaries.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

# Simple Experimental Tactic for finite sets

We use a simple "tableau style" tactic for finite sets. We start by turning the goal into the form A1, ..., An |- False and then derive facts from the Ai until a constdiction is obtained or no more rules are applicable.

Section SetTac.
Variables (T : finType) (A B C : {set T}).

Lemma set_tac_subUl: A :|: B \subset C A \subset C B \subset C.
Proof. rewrite subUset. by case/andP. Qed.

Lemma set_tac_subIr: A \subset B :&: C A \subset B A \subset C.
Proof. rewrite subsetI. by case/andP. Qed.

Lemma set_tac_subIl x :
x \in A x \in B A :&: B \subset C x \in C.
Proof. movexA xB /subsetP. apply. by rewrite inE xA xB. Qed.

End SetTac.

Lemma setIPn (T : finType) (A B : {set T}) (x:T) :
reflect (x \notin A x \notin B) (x \notin A :&: B).
Proof. rewrite !inE negb_and. exact: orP. Qed.

Lemma setUPn (T : finType) (A B : {set T}) (x:T) :
reflect (x \notin A x \notin B) (x \notin A :|: B).
Proof. rewrite !inE negb_or. exact: andP. Qed.

Ltac notHyp b := assert_fails (assert b by assumption).

Ltac extend H T := notHyp H; have ? : H by T.

Ltac convertible A B := assert_succeeds (assert (A = B) by reflexivity).

NOTE: since Ltac is untyped, we need to provide the coercions usually hidden, e.g., is_true or SetDef.pred_of_set.
TOTHINK: For some collective predicates, in particular for paths, the coercion to a predicates can take several different forms. This means that rules involving _ \subset _ should match up to conversion to not miss instances. Similarly, we need to perform a full conversion check when testing whether a given fact is already present. Otherwise, the "same" fact might be added multiple times
NOTE: The only rules that introduce hypotheses of the form _\subset _ are those eliminating equalities between sets. Since these remove their hypotheses, the trivial subset assumption [set _] \subset A can be modified in place

Local Notation pos := SetDef.pred_of_set.

TODO:
• reverse propagation for subset
• dealing with setT and set0
• dealing with existential hypotheses + A != B (possibly do the A != set0 case separately) + ~~ (A \subset B) (this is never generated, do as init?)

Ltac no_inhabitant A :=
match goal with [ _ : ?x \in _ A |- _ ] ⇒ fail 1 | _idtac end.

Ltac set_tab_close :=
match goal with
| [H : is_true (?x == ?y) |- _ ] ⇒
assert_fails (have: x = y by []);
move/eqP : (H) ⇒ ?; subst
| [H : is_true (_ \in _ set0) |- _] ⇒ by rewrite in_set0 in H

| [H : is_true (?x \in pos (?A :&: ?B)) |- _] ⇒
first [notHyp (x \in A)|notHyp(x \in B)]; case/setIP : (H) ⇒ [? ?]
| [H : is_true (?x \in _ (?A :\: ?B)) |- _] ⇒
first [notHyp (x \in A)|notHyp(x \notin B)]; case/setDP : (H) ⇒ [? ?]
| [H : is_true (?x \notin _ (?A :|: ?B)) |- _] ⇒
first [notHyp (x \notin A)|notHyp(x \notin B)]; case/setUPn : (H) ⇒ [? ?]
| [H : is_true (?x \in pos (~: ?A)) |- _] ⇒
extend (x \notin A) ltac:(move: H; rewrite in_setC)
| [H : is_true (?x \notin pos (~: ?A)) |- _] ⇒
extend (x \in A) ltac:(move: H; rewrite in_setC negbK)

| [H : is_true (?x \in _ [set _ in ?p]) |- _ ] ⇒
extend (x \in p) ltac:(move: H; rewrite inE)
| [H : is_true (?x \notin _ [set _ in ?p]) |- _ ] ⇒
extend (x \notin p) ltac:(move: H; rewrite inE)

| [H : is_true (?x \in _ [set ?y]) |- _ ] ⇒
assert_fails (have: x = y by []);
move/set1P : (H) ⇒ ?;subst
| [H : is_true (?x \notin _ [set ?y]) |- _ ] ⇒
extend (x != y) ltac:(move: H ; rewrite inE)

| [ H : ?A = ?B |- _] ⇒
first [notHyp (A \subset B)|notHyp(B \subset A)];
have/andP[? ?]: (A \subset B) && (B \subset A) by
(move/eqP : (H); rewrite eqEsubset; apply)
| [ H : is_true (pos (?A :|: ?B) \subset ?C) |- _] ⇒
first[notHyp (A \subset C)|notHyp (B \subset C)];
case/set_tac_subUl : (H) ⇒ [? ?]
| [ H : is_true (?A \subset pos (?B :&: ?C)) |- _] ⇒
first[notHyp (A \subset B)|notHyp (A \subset C)];
case/set_tac_subIr : (H) ⇒ [? ?]
| [ H : is_true (pos [set ?x] \subset ?A) |- _] ⇒
extend (x \in A) ltac:(move: (H); rewrite sub1set; apply)

| [H : is_true (in_mem ?x (mem ?A)), S : is_true (subset (mem ?A') (mem ?B)) |- _] ⇒
convertible (mem A) (mem A');
extend (x \in B) ltac:(move/(subsetP S) : (H) ⇒ ?)

| [H : is_true (?x \in ?B), D : is_true [disjoint ?A & ?B] |- _] ⇒
notHyp (x \notin A); have ? : x \notin A by rewrite (disjointFl D H)
| [H : is_true (?x \in ?A), D : is_true [disjoint ?A & ?B] |- _] ⇒
notHyp (x \notin B); have ? : x \notin B by rewrite (disjointFr D H)

| [ H : is_true (?A != set0) |- _] ⇒
no_inhabitant A; case/set0Pn : H ⇒ [? ?]

| [ xA : is_true (?x \in _ ?A), xB : is_true (?x \in _ ?B),
H : is_true (_ (?A :&: ?B) \subset ?D) |- _] ⇒
notHyp (x \in D); have ? := set_tac_subIl xA xB H
end.

Ltac set_tab_branch :=
match goal with
| [H : is_true (?x \in pos (?A :|: ?B)) |- _] ⇒
notHyp (x \in A); notHyp (x \in B); case/setUP : (H) ⇒ [?|?]
| [ H : is_true (?x \notin pos (?A :&: ?B)) |- _] ⇒
notHyp (x \notin A); notHyp (x \notin B); case/setIPn : (H) ⇒ [?|?]
end.

Note that the rules on disjointness and subset do not restricted to the type {set _}

Ltac set_init :=
match goal with
| [ |- _,_ ] ⇒ intro;set_init
| [ |- _ _] ⇒ intro;set_init
| [ |- is_true (~~ _) ] ⇒ apply/negP ⇒ ?
| [ |- is_true _] ⇒ apply: contraTT isT ⇒ ?
| [ |- _ ] ⇒ idtac
end.

Ltac clean_mem :=
repeat match goal with
[ H : _ |- _ ] ⇒ rewrite !mem_mem in H
end; rewrite !mem_mem.

Tactics intened to be redefined when combining sets with set-like structures (e.g., paths in graphs)

Ltac set_tac_close_plus := fail.
Ltac set_tac_branch_plus := fail.

Ltac eqxx := match goal with
| [ H : is_true (?x != ?x) |- _ ] ⇒ by rewrite eqxx in H
end.

Use theory rules (plus) before set rules
Ltac set_tac_step := first [eqxx
|contrab
|set_tac_close_plus
|set_tab_close
|set_tac_branch_plus
|set_tab_branch].

Ltac set_tac := set_init; subst; repeat set_tac_step.

Use typeclass inference to trigger set_tac using rewrite lemmas

Class setBox (P : Prop) : Prop := SetBox { setBoxed : P }.
Hint Extern 0 (setBox _) ⇒ apply SetBox; set_tac : typeclass_instances.

Lemma inD (T : finType) (x : T) (A : pred T) `{setBox (x \in A)} : x \in A.
Proof. by case: H. Qed.

Lemma inD_debug (T : finType) (x : T) (A : pred T) : (x \in A) x \in A.
Proof. by []. Qed.

Lemma notinD (T : finType) (x : T) (A : pred T) `{setBox (x \notin A)} : x \notin A.
Proof. by case: H. Qed.

Lemma notinD_debug (T : finType) (x : T) (A : pred T) : (x \notin A) x \notin A.
Proof. by []. Qed.

Goal (T:finType) (S V1 V2 : {set T}) x b, x \in S S = V1 :&: V2 b || (x \in V1).
Proof. move ⇒ ×. by rewrite inD orbT. Qed.

Goal (T:finType) (A B : {set T}) x b, x \in B B \subset A (x \in A) || b.
Proof. moveT A B x b H D. by rewrite inD. Qed.

Goal (T:finType) (A B : {set T}) x b, x \in B [disjoint A & B] (x \notin A) || b.
Proof. moveT A B x b H D. by rewrite notinD. Qed.

Goal (T:finType) (A B : {set T}) x b, x \in A [disjoint A & B] b || (x \notin B).
Proof. moveT A B x b H D. by rewrite notinD orbT. Qed.

Goal (T:finType) (A B : {set T}) x b, x \notin A x \in A :|: B b || (x \in B).
Proof. move ⇒ ×. by rewrite inD orbT. Qed.

NOTE: This does not require backward propagation of \subset since x \in B is assumed
Goal (T:finType) (A B : {set T}) x b, x \notin A B \subset A (x \notin B) || b.
Proof. moveT A B x b H D. by rewrite notinD. Qed.

Goal (T:finType) (A B : {set T}) x, x \in A A = B x \in B.
Proof. by set_tac. Qed.

Goal (T:finType) (A B : {set T}) x, x \in A A == B x \in B.
Proof. by set_tac. Qed.