Library Bitset.ops.keep_min

From Ssreflect
     Require Import ssreflect ssrbool eqtype ssrnat seq fintype ssrfun.
From MathComp
     Require Import tuple finset.
From Bits
     Require Import bits ssrextra.tuple.
Require Import spec min.

Definition keep_min {n} (bs: BITS n): BITS n
  := andB bs (negB bs).

Lemma keep_min_repr:
  forall n (bs: BITS n) E x, repr bs E -> x \in E ->
    repr (keep_min bs) [set [arg min_(k < x in E) k]].
Proof.
  move=> n bs.
  rewrite /keep_min.
  have ->: andB bs (negB bs) = setBit #0 (index true bs) true.
  elim: n bs=> [bs|n IHn /tupleP[b bs]].
  +
    by rewrite tuple0.
  +
    case: b.
    -
      by rewrite /negB /incB /invB /andB /=
                 liftUnOpCons !tuple.beheadCons liftBinOpCons andbT
                 -/andB -/invB andB_invB fromNat0.
    -
      by rewrite /negB /incB /invB /andB /=
                 liftUnOpCons tuple.theadCons !tuple.beheadCons liftBinOpCons andbF
                 -/andB -/invB -/incB -/negB IHn.
  move=> E x HE Hx.
  rewrite (index_repr n bs x E)=> //.
  by apply singleton_repr.
Qed.