How to prove commutation of a recursive function over a finite set encoded with binary nat in coq

Question

I needed to define some things in finite set, the original library seemed too complex so I took my friend's advice and I used a library he was developing for this purpose. The library uses BinNat library to encode members of the set. the basic definitions are as below

Definition finset := N.
Definition union : finset -> finset -> finset := lor.
Infix "∪" := union (left associativity, at level 62).

Definition intersection : finset -> finset -> finset := land.
Infix "∩" := intersection (left associativity, at level 62).

Definition diff : finset -> finset -> finset := ldiff.
Infix "\" := diff (left associativity, at level 63).

Definition mem : nat -> finset -> bool := fun n s => testbit_nat s n.
Infix "∈" := mem (at level 60).

once you prove basic relations and theorems everything is a piece of cake. for what I was doing I had to define a finite set of propositions so I assumed following axioms.

Axiom prop_to_nat: prop -> nat.
Axiom nat_to_prop: nat -> prop.

Axiom prop_to_prop: forall p, nat_to_prop(prop_to_nat(p)) = p.
Axiom nat_to_nat: forall n, prop_to_nat(nat_to_prop(n)) = n.

So here comes the problem, I need to define a function which returns atoms of a set of props so I did this.

Fixpoint atoms_of (p : prop) : finset :=
  match p with
  | ^x_a => {{a}}
  | p1 ∧ p2 => (atoms_of p1) ∪ (atoms_of p2)
  | p1 ∨ p2 => (atoms_of p1) ∪ (atoms_of p2)
  | p1 ⊃ p2 => (atoms_of p1) ∪ (atoms_of p2)
  | _ => ∅
  end.
Fixpoint atoms_of_pos (p: positive) (n : nat): finset :=
    match p with
        | xH => atoms_of(nat_to_prop(n))
        | xO p' => atoms_of_pos p' (S n)
        | xI p' => atoms_of(nat_to_prop(n)) ∪ (atoms_of_pos p' (S n))
    end.
Definition atoms_of_set (s: finset): finset :=
    match s with
    | ∅ => ∅
    | pos p => atoms_of_pos p 0 
    end.

and finally I need to prove some functionality over these functions for example I need to prove

Lemma atoms_set_union: forall s1 s2, atoms_of_set (s1 ∪ s2) = (atoms_of_set s1) ∪ (atoms_of_set s2).
 

but I'm stuck here, BinNat only adds bits to it's right (like constructing 101 from 10) so it's really hard to prove by induction since each time the number is totally different. before I throw away everything I've done I wanted to ask if anyone knows how to do this.

Answer 1

BinNat only adds digits to it's left so it's really hard to prove by induction since each time the number is totally different.

This reads like there is a misconception that induction on a binary natural (N, positive) will be like induction on a Peano natural (nat), which is not a good way to reason about binary representation. In fact, induction on positive is the way to go. It will be case-splitting on the bits of the number, similarly to how atoms_of_pos is defined.