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

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.

• What is prop? And what is the end goal of all of this? I would be suprised to find out that coding finite sets of natural numbers with integers is a good solution to a problem that does not inherently ask for such coding. Dec 14, 2023 at 13:43
• In any case, you should first formulate a lemma that relates atoms_of_pos and unions. Once you have that, atoms_set_union should be more or less a special case of it. Dec 14, 2023 at 13:58
• @AndrejBauer you actually helped me fix my problem several months ago, I was trying to formulate sequent calculus in order to prove the interpolation theorem by induction. I completely threw away this idea and worked with infinite multisets as cedents. Dec 14, 2023 at 18:58
• Dang, I am reading old posts again. Dec 15, 2023 at 13:47

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.