# Why discriminate the base case allows me to complete the induction proof?

I have a successful completed proof which used induction. but I essentially proved the goal on the base case by tactic discriminate. Why is this induction proof still stands?

the principle of induction tells us induction involves three steps:

     - show that the P(O) holds, (* O stands for the first item *);
- show that, for any n, if P(n) holds, then so does
P(next(n));
- conclude that P(n) holds for all n.


but if I finished proving subgoal P(O) by discriminate, that is, confirmed the subgoal is impossible, how does that constitue as a holding base case?

Here's the proof in question:

Fixpoint filter {X:Type} (test: X->bool) (l:list X) : (list X) :=
match l with
| [] => []
| h :: t =>
if test h then h :: (filter test t)
else filter test t
end.

Theorem filter_property : forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),
filter test l = x :: lf -> test x = true.
Proof.
induction l.
- intros. discriminate.
- simpl. destruct (test x0) eqn:Etest.
+ intros. injection H. intros. rewrite -> H1 in Etest. apply Etestx.
+ apply IHl.
Qed.

• If you've proved the base case, you have a proof of the best case, no matter how you proved it… I think it's going to be hard to help you in vague terms like this. You should post the specific proof you don't understand. – Gilles 'SO- stop being evil' Oct 16 '20 at 11:13
• @Gilles'SO-stopbeingevil' updated the proof text. – Sajuuk Oct 16 '20 at 14:39

You want to prove that if the result of of filter test l is a non-empty list, then its first element passes test. You're using induction on l.
The base case for the induction is the empty list []. For the base case, you need to prove that if filter test [] = x :: lf then test x = true. In order to prove this, you assume that filter test [] = x :: lf, and prove that this hypothesis is a contradiction. Indeed it is: there is no value of x and lf that makes filter test [] = x :: lf true, because filter test [] is the empty list. So, for the base case, for any x and any lf, the proposition filter test l = x :: lf -> test x = true is true.