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
     - 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

Theorem filter_property : forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),     
filter test l = x :: lf -> test x = true.
induction l.
- intros. discriminate. 
- simpl. destruct (test x0) eqn:Etest. 
 + intros. injection H. intros. rewrite -> H1 in Etest. apply Etestx.
 + apply IHl.
  • $\begingroup$ 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. $\endgroup$ – Gilles 'SO- stop being evil' Oct 16 '20 at 11:13
  • $\begingroup$ @Gilles'SO-stopbeingevil' updated the proof text. $\endgroup$ – 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.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.