Library Bitset.ops.insert

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

Definition insert {n}(bs: BITS n) k: BITS n := orB bs (shlBn #1 k).

Lemma insert_repr: forall n (bs: BITS n) (k: 'I_n) E, repr bs E ->
    repr (insert bs k) (k |: E).
Proof.
  move=> n bs k E HE.
  rewrite /repr -setP /eq_mem=> x.
  rewrite in_set getBit_set_true=> //.
  rewrite fun_if.
  case H: (x == k).
    +
      move/eqP: H ->.
      by rewrite eq_refl setU11.
    +
      rewrite ifF=> //.
      by rewrite in_setU1 H HE in_set.
Qed.