Subsets of list nat in coq

Question

I defined a recursive function for all subsets of nat_list in coq as

Fixpoint subsets (a: list nat) : (list (list nat)) :=
 match a with
  |[] => [[]]
  |h::t => subsets t ++ map (app [h]) (subsets t)
end.

I am trying to prove that

forall (a:list nat), In [] (subsets a).

I tried to induct on a. The base-case was straight forward. However in the induction case i tried to use the in-built theorem in_app_or.

Unable to unify "In ?M1396 ?M1394 \/ In ?M1396 ?M1395" with
"(fix In (a : list nat) (l : list (list nat)) {struct l} : Prop := 

match l with
| [] => False
| b :: m => b = a \/ In a m     
end)                                                         
[] (subsets t ++ map (fun m : list nat => h :: m) (subsets t))".

How do I prove such a theorem or get around such an issue?

Answer 1

The problem with in_app_or is that is has the following type:

forall (A : Type) (l m : list A) (a : A),
  In a (l ++ m) -> In a l \/ In a m

and application of lemmas to the goal works "backwards": Coq matches the consequent B of the implication A -> B with the goal, and if they can be unified, you are left with a new goal: you need to prove a (stronger) statement A. And in your case the A and B are in the wrong order (swapped), so you need to apply in_or_app instead:

in_or_app : forall (A : Type) (l m : list A) (a : A),
  In a l \/ In a m -> In a (l ++ m)

This is how your goal can be proved using in_or_app:

Goal forall (a:list nat), In [] (subsets a).
  intros.
  induction a; simpl; auto.
  apply in_or_app; auto.
Qed.