Computing the subsets of natural numbers in AGDA

1
votes

I'm using AGDA to do some classical mathematical proofs. I'd like to prove that the number of subsets of a set of cardinality n is equal to 2^n (i.e pow (2, n)). To do so, my strategy would be the following :

1) Write a function sub n, that, given each natural, it returns a list of all the possible subsets of naturals less or equal to n.

2) Write two functions "length " and "pow ", that separately compute the length of the list and 2^n

3) Put the 3 functions together to prove the statement.

However, I'm having troubles to solve point 1 ). My idea is to make the function return a list of type "list Nat", but I am having some problem to implement the recursion. Basically my idea for the inductive step is to associate to each subset of "n" two new subsets : itself and the subset obtained adding "n+1".

Do you think it is an effective strategy? And moreover, how can I solve my troubles with point 1? Thanks

1
functional-programmingsubsetagdaset-theoryproof-of-correctness

1 Answers

2
votes

By the way, I have solved my problem using the strategy I proposed. To define the function that compute the number of subsets I use the standard map function and an additional auxiliary function add-to-list:

add-to-list : ℕ → List ℕ  → List ℕ 
add-to-list n x  = n  ∷ x


subℕ : ℕ → List ( List ℕ )
subℕ zero = [ 0 ] ∷ []
subℕ (suc x) = subℕ x ++ ( map ( add-to-list  x ) ( subℕ x ) )

Then, I prove the two following elementary lemmas:

l-aux : ∀ {A : Set } { x y : List A } → ( length ( x ++ y ) )≡( ( length x ) + ( length  y ))
l-aux {A} {[]} {y} = refl
l-aux {A} {x ∷ x₁} {y} rewrite l-aux {A} { x₁} {y} = refl

l-aux-1 : ∀ {A : Set } { x : List A } { f : A → A } → ( length ( map f x ) ) ≡ ( length x )
l-aux-1 {A} {[]} {f} = refl
l-aux-1 {A} {x ∷ x₁} {f} rewrite l-aux-1 {A} { x₁} {f} = refl

And the proof is reduced to elementary recursion :

number-of-subsets : ∀ ( n : ℕ ) → ( length ( subℕ n ) ) ≡ ( pow 2 n )
number-of-subsets zero = refl
number-of-subsets (suc n ) rewrite l-aux {List ℕ} {subℕ n} { map ( add-to-list n ) (subℕ n)} | l-aux-1 {List ℕ} {subℕ n} {add-to-list n } |  number-of-subsets n | +0 (pow 2 n )  = refl