From mathcomp Require Import ssreflect ssrbool eqtype seq choice.
From libs Require Import edone bcase base fset.

Set Implicit Arguments.

Section TabRules.

  Variable T: choiceType.

  Lemma properSub (A B : {fset T}): A `<` B = (A `<=` B) && ~~ (B `<=` A).
  Proof. rewrite properEneq eqEsub. by case (A`<=`B), (B`<=`A). Qed.
  Lemma sepI (A B : {fset T}) : A `&` B = [fset x in A | x \in B].
  Proof. by rewrite /fsetI. Qed.
  Lemma sepD (A B : {fset T}) : A `\` B = [fset x in A | x \notin B].
  Proof. by rewrite /fsetD. Qed.

  Definition compSetOps := (sepI, sepD, properSub).

  Lemma prop_dn s : ~~ ~~ s → s.   Proof. exact (@ negbNE s). Qed.

  Lemma prop_conj s t : s && t → s ∧ t.   Proof. apply: andP. Qed.

  Lemma prop_negDisj s t : ~~ (s || t) → ~~ s ∧ ~~ t.   Proof. rewrite negb_or. apply: andP. Qed.

  Lemma prop_negImpl s t : ~~ (s ==> t) → s ∧ ~~ t.   Proof. rewrite negb_imply. apply: andP. Qed.


  Lemma satr_eqSym (a b : T) : a == b → b == a.   Proof. by rewrite eq_sym. Qed.

  Lemma satr_memSgt (a b : T) : a \in [fset b] → a == b.   Proof. by rewrite in_fset1. Qed.

  Lemma satr_nmemSgt (a b : T) : a \notin [fset b] → a != b.   Proof. by rewrite in_fset1. Qed.

  Lemma satr_sgtSub (a:T) (A : {fset T}) : [fset a] `<=` A → a \in A.   Proof. by rewrite fsub1. Qed.

  Lemma satr_eqP (A B : {fset T}) : A == B → (A `<=` B) ∧ (B `<=` A).   Proof. rewrite eqEsub. apply: andP. Qed.

  Lemma satr_nmemU (a:T) (A B : {fset T}) : a \notin A `|` B → a \notin A ∧ a \notin B.   Proof. rewrite in_fsetU negb_or. apply: andP. Qed.

  Lemma pow_mem (A B : {fset T}) : A \in (powerset B) → A `<=` B.   Proof. by rewrite powersetE. Qed.

  Lemma satr_memSub (a:T) (A B : {fset T}) : a \in A → A `<=` B → a \in B.   Proof. move ⇒ P Q. apply: (@subP T A) ⇒ //. Qed.

  Lemma satr_nmemSup (a:T) (A B : {fset T}) : a \notin A → B `<=` A → a \notin B.   Proof. move ⇒ P Q. case R: (a \in B) ⇒ //. by rewrite (subP Q) in P. Qed.

  Lemma satr_eqMem (a b : T) (A : {fset T}) : a == b → b \in A → a \in A.   Proof. intros P Q. by rewrite -(eqP P) in Q. Qed.

  Lemma satr_eqTrans (a b c : T) : a == b → b == c → a == c.   Proof. intros P Q. by rewrite -(eqP P) in Q. Qed.

  Lemma satr_notSub (A B : {fset T}) : ~~ (A `<=` B) → ∃ a, (a \in A) ∧ (a \notin B).   Proof. move ⇒ P. move: (subPn A B P) ⇒ {P} [a P Q]. by ∃ a. Qed.

  Lemma pow_nmem (A B : {fset T}) : A \notin (powerset B) → ∃ x, (x \in A) ∧ (x \notin B).   Proof. rewrite powersetE ⇒ P. apply (satr_notSub A B P). Qed.

  Lemma prop_disj s t : s || t → s ∨ t.   Proof. apply: orP. Qed.

  Lemma prop_impl s t : s ==> t → ~~ s ∨ t.   Proof. rewrite implybE. apply: orP. Qed.

  Lemma prop_negConj s t : ~~ (s && t) → ~~ s ∨ ~~ t.   Proof. rewrite negb_and. apply: orP. Qed.

  Lemma satr_memU (a:T) (A B : {fset T}) : a \in A `|` B → a \in A ∨ a \in B.   Proof. rewrite in_fsetU. apply: orP. Qed.

  Lemma satr_neqP (A B : {fset T}) :
    A != B → ∃ x, (x \in A ∧ x \notin B) ∨ (x \in B ∧ x \notin A).   Proof.
    rewrite eqEsub negb_and ⇒ P. move: (orP P) ⇒ {P} [P|P].
    - move: (satr_notSub A B P) ⇒ {P} [x [P Q]]. ∃ x; by left.
    - move: (satr_notSub B A P) ⇒ {P} [x [P Q]]. ∃ x; by right.
  Qed.

  Lemma clos_posNeg (s : bool) : s → ~~ s → False.   Proof. by case s. Qed.

  Lemma clos_neqxx (a : T) : a != a → False.   Proof. by rewrite eqxx. Qed.

  Lemma clos_memEmp (a : T) : a \in fset0 → False.   Proof. by rewrite in_fset0. Qed.

  Lemma subst_memSep (y:T) (A : {fset T}) (p : T → bool) : y \in sep A p → (y \in A) ∧ (p y).   Proof. rewrite in_sep. apply: andP. Qed.

  Lemma subst_nmemSep (y:T) (A : {fset T}) (p : T → bool):
    y \notin [ fset x in A | p x] → y \notin A ∨ ~~ p y.   Proof. rewrite in_sep ⇒ P . apply: orP. by rewrite -negb_and. Qed.

  Lemma cut_eq (a b : T) : a == b ∨ a != b.
  Proof. case (a == b); first by left. right. by apply negbT. Qed.
  Lemma cut_mem a (A: {fset T}) : a \in A ∨ a \notin A.   Proof. case (a \in A); first by left. right. by apply negbT. Qed.

  Lemma cut_sub (A B : {fset T}) : A `<=` B ∨ ~~ (A `<=` B).   Proof. case (A `<=` B); first by left. right. by apply negbT. Qed.

End TabRules.

Ltac extend X PX :=
  let V := fresh "H" in
  let X := constr:(is_true X) in
  match goal with
    | _: X |- _ ⇒ fail 1
    | _ ⇒ have V: X by apply PX
  end.

Ltac extend_conj A B PX :=
  let U := fresh "H" in
  let V := fresh "H" in
  let A := (eval simpl in (is_true A)) in
  let B := (eval simpl in (is_true B)) in
  match goal with
    | _: A, _: B |- _ ⇒ fail 1
    | _ ⇒ have [U V]: A ∧ B by apply PX
  end.

Ltac extend_disj A B PX :=
  let V := fresh "H" in
  let A := (eval simpl in (is_true A)) in
  let B := (eval simpl in (is_true B)) in
  match goal with
    | _: A |- _ ⇒ fail 1
    | _: B |- _ ⇒ fail 1
    | _ ⇒ have [V | V]: A ∨ B by apply PX
  end.

Ltac extend_conj_ex A B PX :=
  let X := fresh "x" in
  let U := fresh "H" in
  let V := fresh "H" in
  match goal with
    | _: is_true(?x \in A), _: is_true (?x \notin B) |- _ ⇒ fail 1
    | _ ⇒ have [X [U V]]: ∃ x, (x \in A) ∧ (x \notin B) by apply PX
  end.

Ltac extend_disconj_ex A B PX :=
  let X := fresh "x" in
  let U := fresh "H" in
  let V := fresh "H" in
  match goal with
    | _: is_true(?x \in A), _: is_true(?x \notin B) |- _ ⇒ fail 1
    | _: is_true(?x \in B), _: is_true(?x \notin A) |- _ ⇒ fail 1
    | _ ⇒ have [X [[U V] | [U V]]]:
             ∃ x, (x \in A ∧ x \notin B) ∨ (x \in B ∧ x \notin A)
               by apply PX
  end.

Ltac closebranch :=
  match goal with
  | H0: is_true (?s), H1: is_true(~~ ?s) |- _ ⇒ apply (@ clos_posNeg s); first exact H0; exact H1
  | H0: is_true (?a != ?a) |- _ ⇒ apply (@ clos_neqxx _ a); exact H0
  | H0: is_true (?a \in fset0) |- _ ⇒ apply (@ clos_memEmp _ a); exact H0
  end.

Ltac nonbranching :=
  match goal with
  
  | _: is_true(~~ ~~ ?s) |- _ ⇒ extend s (prop_dn s)
  | _: is_true(?s && ?t) |- _ ⇒ extend_conj s t (prop_conj s t)
  | _: is_true(~~ (?s || ?t)) |- _ ⇒ extend_conj (~~ s) (~~ t) (prop_negDisj s t)
  | _: is_true(~~ (?s ==> ?t)) |- _ ⇒ extend_conj s (~~ t) (prop_negImpl s t)
  | _: is_true(?a == ?b) |- _ ⇒ extend (b == a) (satr_eqSym a b)
  | _: is_true(?a \in [fset ?b]) |- _ ⇒ extend (a == b) (satr_memSgt _ a b)
  | _: is_true(?a \notin [fset ?b]) |- _ ⇒ extend (a != b) (satr_nmemSgt _ a b)
  | _: is_true([fset ?a] `<=` ?A) |- _ ⇒ extend (a \in A) (satr_sgtSub a A)
  | _: is_true(?A == ?B) |- _ ⇒ extend_conj (A `<=` B) (B `<=` A) (satr_eqP A B)
  | _: is_true(?a \notin ?A `|` ?B) |- _ ⇒ extend_conj (a \notin A) (a \notin B) (satr_nmemU a A B)
  | _: is_true(?A \in (powerset ?B)) |- _ ⇒ extend (A `<=` B) (pow_mem A B)
  
  | _: is_true(?a \in ?A), _: is_true(?A `<=` ?B) |- _ ⇒ extend (a \in B) (satr_memSub a A B)
  | _: is_true(?a \notin ?A), _: is_true(?B `<=` ?A) |- _ ⇒ extend (a \notin B) (satr_nmemSup a A B)
  | _: is_true(?a == ?b), _: is_true(?b \in ?A) |- _ ⇒ extend (a \in A) (satr_eqMem a b A)
  | _: is_true(?a == ?b), _: is_true(?b == ?c) |- _ ⇒ extend (a == c) (satr_eqTrans _ a b c)
  
  | _: is_true(~~ (?A `<=` ?B)) |- _ ⇒ extend_conj_ex A B (satr_notSub A B)
  | _: is_true(?A \notin (powerset ?B)) |- _ ⇒ extend_conj_ex A B (pow_nmem A B)
  
  | _: is_true(?a \in sep ?A ?p) |- _ ⇒ extend_conj (a \in A) (p a) (subst_memSep a A p)
  end.

Ltac branching :=
  match goal with
  | _: is_true(?s || ?t) |- _ ⇒ extend_disj s t (prop_disj s t)
  | _: is_true(?s ==> ?t) |- _ ⇒ extend_disj (~~ s) t (prop_impl s t)
  | _: is_true(~~ (?s && ?t)) |- _ ⇒ extend_disj (~~ s) (~~ t) (prop_negConj s t)
  
  | _: is_true(?a \in ?A `|` ?B) |- _ ⇒ extend_disj (a \in A) (a \in B) (satr_memU a A B)
  | _: is_true(?A != ?B) |- _ ⇒ extend_disconj_ex A B (satr_neqP A B)
  
  | _: is_true(?a \notin sep ?A ?p) |- _ ⇒ extend_disj (a \notin A) (~~ (p a)) (subst_nmemSep a A p)
  end.

Ltac cutrules :=
  match goal with
  | _: context[?a], _: context[?A] |- _ ⇒ extend_disj (a \in A) (a \notin A) (cut_mem a A)
  | _: context[?A], _: context[?B] |- _ ⇒ extend_disj (A `<=` B) (~~(A `<=` B)) (cut_sub A B)
  | _: context[?A], _: context[?B] |- _ ⇒ extend_disj (A == B) (A != B) (cut_eq _ A B)
  end.

Ltac reverywhere X :=
  repeat rewrite X;
  repeat match goal with
           | H: _ |- _ ⇒ rewrite X in H
         end.

Ltac genSubst :=
  repeat (
      let V := fresh "su" in
      match goal with
        | H: is_true(?x == ?y) |- _ ⇒
          match goal with
            | _: x = y |- _ ⇒ fail 1
            | _ ⇒ move: (eqP H) ⇒ V
          end
        | x := _ |- _ ⇒ subst x
      end
    ); subst.

Ltac clearNonbools :=
  repeat(
      match goal with
      | H : _ |- _ ⇒
        match type of H with
        | is_true _ ⇒ fail 1
        | _ = _ ⇒ fail 1
        | _ ⇒ clear H
        end
      end
    ).

Lemma semiDN (b:bool) : ¬ ~~ b → b.
Proof. case: b ⇒ _ //. Qed.

Lemma eq2bool (T : eqType) (a b : T) : a = b → a == b.
Proof. move ⇒ H. by rewrite H. Qed.

Ltac oDN :=
  let V := fresh "H" in
  match goal with
  | |- is_true _ ⇒ apply semiDN; hnf ⇒ V
  | |- _ = _ ⇒ apply:eqP; apply semiDN; hnf ⇒ V
  | |- False ⇒ idtac
  end.

Ltac eq2bool :=
  let V := fresh "H" in
  match goal with
  | H: _ = _ |- _ ⇒ move:(eq2bool _ H) ⇒ V
  | _ ⇒ idtac
  end.

Ltac preproc :=
  repeat (let V := fresh "H" in move ⇒ V);
  oDN;
  eq2bool;
  reverywhere compSetOps;
  clearNonbools.

Ltac core :=
  repeat(
      genSubst;
      repeat nonbranching;
      try closebranch;
      genSubst;
      try branching;
      try closebranch
    ).

Ltac fset_dec :=
  preproc;
  repeat(
      try closebranch;
      core;
      try cutrules
    ).

Ltac fset_nocut := preproc; try closebranch; core.

Ltac invert X :=
  match X with
    | (?x, ?y) ⇒
      match x with
        | (?x0, ?x1) ⇒ let z := invert (x0, (x1, y)) in constr:(z)
      end
    | _ ⇒ constr:(X)
  end.

Ltac fset_decu X :=
  let Y := invert X in
  match Y with
    | (?x, ?xs) ⇒ unfold x in *; fset_decu xs
    | ?x ⇒ unfold x in *; fset_dec
  end.

Ltac fset_nocutu X :=
  let Y := invert X in
  match Y with
    | (?x, ?xs) ⇒ unfold x in *; fset_nocutu xs
    | ?x ⇒ unfold x in *; fset_nocut
  end.