Search code examples
coq

"False" in goal: is that a an indication I am doing something wrong?

I am trying to prove following (https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html):

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop
  := match l with
  | [] => False
  | x::xs => P x \/ All P xs
  end.

Theorem All_In :
  forall T (P : T -> Prop) (l : list T),
    (forall x, In x l -> P x) <-> All P l.
Proof.
intros T P l.
destruct l.
- split.
  simpl. intros.

This gives:

2 goals
T : Type
P : T -> Prop
H : forall x : T, False -> P x
______________________________________(1/2)
False
______________________________________(2/2)
All P [ ] -> forall x : T, In x [ ] -> P x

Couple of questions:

  • does having "False" in goal indicates that my proof went wrong (or maybe my All definition is incorrect) ?

  • What shall I do with H ? I can't destruct it, can't apply it, neither use it to rewrite; it also has x which isn't in context...

EDIT: okey looks like a Proposition is automatically True, when there is no elements on which it can be applied, that didn't occur to me: https://en.wikipedia.org/wiki/Vacuous_truth

EDIT2: oh wow, my All was completely wrong. The exercise says: Drawing inspiration from [In], write a recursive function [All], I was a little too much inspired by that In. Solved.

Solution

    1. Having False as your goal is normal in certain circumstances, for example when you want to prove ~ P. This is because that is just an abbreviation for P -> False, and the obvious thing to do is introduce P, obtaining, for example, p : P as a hypothesis and False as your goal. Once you have False as your goal, you must look for a contradiction arising from your context.

    2. In this particular case, there doesn't seem to be any contradiction in your context, which is a sign that perhaps something indeed went wrong. In general, this can be due to wrong definitions, wrong lemmas, or wrong proof steps. Since your proof is quite short and you are in the base case, it is a priori unlikely the proof is the culprit. You seem to already not be very confident in your definition of All, so I would urge you to reconsider it. Hint: you are struggling to prove the base step, so look for a problem in the definition of the base case. Does every element of the empty list have property P?