Decider for lists In Fixpoint

Question

I am relatively new to coq and i am not sure how to procede here.

I want to write a decidability function for the In Fixpoint of the list library like this:

Program Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => ~ In s l
  | head :: tail => 
    if eq_dec s head
    then In s l
    else InDec s tail
  end.

This is in a section where K is a Type and has this property:

Context `{EqDec K}.

where

Class EqDec A : Type := {
  eq_dec: forall a1 a2 : A, {a1 = a2} + {a1 <> a2}
  }.

How i understood it, {In s l} + {~ In s l} is a Type and In s l is a Prop, which causes this not to work, but i am not sure why exactly. What do i need to change, so i can use InDec in if expressions and why is In s l not a member of {In s l} + {~ In s l}?

I thought {In s l} + {~ In s l} would create a Type with inhabitants In s l and ~ In s l.

Answer 1

Your "function definition" does not make any sense. It is as if you wanted to define addition like this:

Fixpoint add (n:nat) (m:nat) : nat := 
match n, m with
  0,   m => nat (* instead of [m] *)
| S n, m => nat (* instead of [S (add n m)] *)
end

Which does not actually define a function. You need to specify which number is to be returned, but you are just telling Coq that a number is to be returned. This does not make sense.

Instead, you should define your function like this:

Obligation Tactic := idtac. (* for didactic reasons *)
Program Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => right _
  | head :: tail => 
    if eq_dec s head
    then left _
    else match InDec s tail with
      left Hl => left _
    | right Hr => right _ end
  end.
(* prove that if l = Nil, the element is not in the list *)
Next Obligation. intros s l _ []. Qed.
(* prove that if s = head, the element is in the list *)
Next Obligation. intros s l head tail _ Heq. left. symmetry. apply Heq. Qed.
(* prove that the recusion steps work *)
Next Obligation.
  intros InDex s l head tail _ Hne rr Hl _.
  right. apply Hl.
Qed.
Next Obligation.
  intros InDex s l head tail _ Hne rr Hr _.
  intros [H1|H2].
    + apply Hne. symmetry. apply H1.
    + apply Hr, H2.
Qed.

Note that instead of writing e.g. ~In s l in the first case (where the list is empty), which is a type, we actually have to give a proof (i.e. a term having that type). Also note that what we need to prove there is {In s nil} + {~In s nil}, and the first step is figuring out that we are in the right case, hence we use the constructor right. Actually proving that ~In s nil is then left as an obligation (since we are using Program) with an underscore, so that this goal can be solved afterwards using tactics. In concreto, it is the first obligation.

Remember that in Coq, you need to prove things. It is not enough to simply "return true" for your decider, you need to return a proof that you have made the correct choice. This also entails proving that the result of the recursive call is applicable here.

PS: To answer your final question, namely

I thought {In s l} + {~ In s l} would create a Type with inhabitants In s l and ~ In s l.

Nope. {In s l} + {~ In s l} has two kinds of inhabitants: on the one hand, for each p : In s l, we have left p : {In s l} + {~ In s l}. Similarly, for each q : ~ In s l, we have right q : {In s l} + {~ In s l}.

In general, A + B gives you an inhabitant for each A, and one for each B. But you need the inhabitants of A and B first.