Library Coqtail.Arith.Natsets

Require Import ZArith Omega MyNat Div2.

Finite and computable subsets of nat, by functions in nat bool

Ltac rem t x Hx :=
  pose (x := t); assert (Hx : x = t) by reflexivity;
    try rewrite <- Hx in *; clearbody x.

Ltac destruct_if t :=
  lazymatch t with
  | if ?t then _ else _
      let Eqb := fresh "Eqb" in
      let b := fresh "b" in
      rem t b Eqb; destruct b
  | ?u ?vdestruct_if u || destruct_if v

Ltac auto_if :=
  match goal with
  | |- ?Tdestruct_if T
  | H : ?T |- _destruct_if T

Ltac impossible := exfalso; discriminate || omega || tauto.

Ltac dumb_aux :=
  auto || auto with × || discriminate
  || intuition || tauto || omega.

Ltac dumb :=
  try solve
    [ impossible
    | subst; dumb_aux || (simpl in *; dumb_aux)
    | intros; dumb_aux || (simpl in *; dumb_aux) ].

Basic operations and types

Definition bset := natbool.

Definition singleton (x : nat) : bset :=
  fun yif eq_nat_dec x y then true else false.

Definition inter (P Q : bset) : bset := fun iandb (P i) (Q i).

Definition union (P Q : bset) : bset := fun iorb (P i) (Q i).

Bounded cardinal

Definition IBN : boolnat := fun b ⇒ (if b then 1 else 0)%nat.

Fixpoint count n P :=
  match n with
  | OO
  | S n ⇒ (IBN (P n) + count n P)%nat


Definition same (P Q : bset) : Prop := i, P i = Q i.

Fixpoint same_bool n P Q :=
  match n with
  | Otrue
  | S nif Bool.eqb (P n) (Q n) then same_bool n P Q else false

Lemma same_true n P Q : same_bool n P Q = true i, i < nP i = Q i.
  induction n; intros E i L.

    simpl in E.
    auto_if; dumb.
    destruct (eq_nat_dec i n); dumb.
    apply Bool.eqb_true_iff.
    subst; dumb.

Lemma same_false n P Q : same_bool n P Q = false{ i | i < n P i Q i }.
  induction n; simpl; intros I.

    remember (Bool.eqb (P n) (Q n)) as b.
    destruct b.
      destruct IHn as (i, (Li, Di)); eauto.
      destruct (Bool.eqb_false_iff (P n) (Q n)); eauto.

Lemma count_union_inter n P Q : (count n (union P Q) + count n (inter P Q) =
  count n P + count n Q)%nat.
  induction n; auto; simpl.
  unfold IBN, union, inter in ×.
  remember (P n) as Pn; remember (Q n) as Qn.
  destruct Pn; destruct Qn; simpl; omega.

Lemma not_empty P n : O < count n P{ i | i < n P i = true }.
  intros CP.
  induction n.
    simpl in CP; impossible.

    simpl in CP.
    rem (P n) Pn EPn; destruct Pn.
       n; auto.

      destruct IHn as (i, Hi); dumb.
       i; dumb.

Lemma count_union n P Q : count n (union P Q) =
  count n P + count n Q - count n (inter P Q).
  rewrite <- count_union_inter.
  auto with ×.

Lemma count_inter n P Q : count n (inter P Q) =
  count n P + count n Q - count n (union P Q).
  rewrite <- count_union_inter.
  auto with ×.

Lemma count_bound P n : count n P n.
  induction n.
    simpl; destruct (P n); dumb.

Lemma count_drawers : P Q n,
  n < count n P + count n Q{ i | i < n P i = true Q i = true }.
  intros P Q n L.
  destruct (not_empty (inter P Q) n) as (i, Hi).
    rewrite count_inter.
    pose proof count_bound (union P Q) n.

     i; intuition; unfold inter in *;
      destruct (P i); destruct (Q i); intuition.

Definition injective domain (f : natnat) := i j,
  i < domainj < domainf i = f ji = j.

Definition bounded domain bound (f : natnat) := i, i < domainf i < bound.

Fixpoint has_antecedent (f : natnat) domain y :=
  match domain with
  | Ofalse
  | S domainif eq_nat_dec (f domain) y then true else has_antecedent f domain y

Fixpoint number_of_pals_____OUT (f : natnat) domain x :=
  match domain with
  | O ⇒ 0
  | S domain(if eq_nat_dec (f domain) (f x) then 1 else 0) + number_of_pals_____OUT f domain x

image f dom is the set f({0, ..., dom-1})
Definition image (f : natnat) domain : bset := has_antecedent f domain.

Lemma image_true f dom y :
  image f dom y = true{ i | i < dom f i = y }.
  induction dom; intros A; dumb.
  destruct (eq_nat_dec (f dom) y) as [E|E].
     dom; eauto.

    destruct IHdom as (i, Hi).
      simpl in A.
      auto_if; dumb.

       i; dumb.

Lemma image_false : f domain y,
  image f domain y = false x, x < domainf x = yFalse.
  intros f dom; induction dom; intros y T x Bx Exy.
    inversion Bx.

    simpl in T.
    auto_if; dumb.
      apply (IHdom y T x); dumb.
      cut (x dom); dumb.

Lemma image_true_pr f dom y :
   i, i < domy = f iimage f dom y = true.
  intros i L E.
  remember (image f dom y) as b; symmetry in Heqb.
  destruct b; [ reflexivity | exfalso ].
  exfalso; eapply image_false; eauto.

Lemma image_false_pr f dom y :
  ( i, i < domy f i) → image f dom y = false.
  intros NE.
  remember (image f dom y) as b; symmetry in Heqb.
  destruct b; [ exfalso | reflexivity ].
  destruct (image_true _ _ _ Heqb) as (n, Hn).
  specialize (NE n); intuition.

Fixpoint sum n f := match n with OO | S nf n + sum n f end.

Definition is_duplicate f n := IBN (has_antecedent f n (f n)).

Definition is_duplicate_outside f bound n :=
  if lt_dec bound (f n) then IBN (has_antecedent f n (f n)) else O.

TODO unifier l'ordre des variables bound/domain

Fixpoint count_outside domain bound f :=
  match domain with
  | OO
  | S domain(if lt_dec (f domain) bound then 1 else 0) + count_outside domain bound f

Lemma image_injective_plus_one : domain f,
  same (image f (S domain)) (union (image f domain) (singleton (f domain))).
  intros dom f i.
  unfold union, singleton.
  simpl; auto_if; auto with ×.

Lemma count_same S T : same S T n, count n S = count n T.
  intros E n; induction n; simpl; dumb.
  rewrite E; dumb.

Lemma count_same_bounded S T n : ( i, i < nS i = T i) → count n S = count n T.
  intros E; induction n; simpl; dumb.
  repeat (f_equal; dumb).

Lemma count_union_singleton P a n :
  P a = falsea < n
    count n (union P (singleton a)) = S (count n P).
  intros Ma L.
  induction n; dumb.
  unfold union, singleton; simpl.
  destruct (eq_nat_dec a n).
    subst; rewrite Ma; simpl.
    f_equal; apply count_same_bounded; intros i Li.
    auto_if; dumb.

    rewrite plus_n_Sm, <- IHn; dumb.
    repeat f_equal; auto with ×.

Lemma count_image_injective_plus_one : domain f bound,
  injective (S domain) fbounded (S domain) bound f
    count bound (image f (S domain)) = S (count bound (image f domain)).
  intros dom f M If Bf.
  pose proof image_injective_plus_one dom f as HS.
  erewrite count_same; [ | eassumption ].
  rewrite count_union_singleton; dumb.
    apply image_false_pr; intros i L E.
    apply If in E; dumb.

Lemma injective_S dom f : injective (S dom) finjective dom f.
  intros If i j Bi Bj.
  apply If; dumb.

Lemma bounded_S dom M f : bounded (S dom) M fbounded dom M f.
  intros If i Bi.
  apply If; dumb.

Lemma count_image_injective : domain bound f,
  injective domain fbounded domain bound f
    count bound (image f domain) = domain.
  intros dom M f Injf Bf.
  induction dom.
    simpl; clear.
    induction M; auto.

    rewrite count_image_injective_plus_one; dumb.
    rewrite IHdom; dumb.
      apply injective_S; auto.
      apply bounded_S; auto.