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)
  | _ => ∅
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))
Definition atoms_of_set (s: finset): finset :=
    match s with
    | ∅ => ∅
    | pos p => atoms_of_pos p 0 

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.


1 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.

  • $\begingroup$ I fixed the ambiguity in the question, the problem is by inducting on postive the induction hypothesis is unusable since its about a completely different finset, generalizing over atoms_of_pos third argument doesn't work either since it's incremental and we can't have reverse induction on nat. $\endgroup$ Jul 16 at 20:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.