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

Question

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.

Answer 1

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.

Using the notation you've used to state the principle of induction, P(n) has the form “Q(n) implies R(n)” (where Q(n) is “the result of filter is a non-empty list” and R(n) is “the first element passes the test”). It would be strange if P(0) was vacuously true, but that's not what's going on here: what's going on is that R(0) is vacuously true, because Q(0) is impossible. The base case P(0) is possible. It happens to have the form of an implication where the premise is impossible, but that's just happenstance.