Logic: All definition and All_In theorem

Question

Here is the task:

Drawing inspiration from [In], write a recursive function [All] stating that some property [P] holds of all elements of a list [l]. To make sure your definition is correct, prove the [All_In] lemma below. (Of course, your definition should not just restate the left-hand side of [All_In].)

In was defined like this:

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x' = x \/ In x l'
  end.

At first I defined All in a similar manner:

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

But then I thought that this is incorrect because False at the end of conjunction will always give False.

We need to ignore the last nil element of the list if it is not empty (this doesn't work, just an idea):

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

Error, which I don't know how to solve:

Error: The term "l' = [ ]" has type "Prop" which is not a (co-)inductive type.

Then I revert to the first case:

  | x' :: l' => P x' /\ All P l'

and try to prove All_In theorem:

Lemma 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. split.
  - (* Left to right *)
    intros H. induction l as [| h t IHl].
    + simpl. simpl in H.

Now we are stuck:

T : Type
P : T -> Prop
H : forall x : T, False -> P x
============================
False

Because we have False in the conclusion, but there is no False hypothesis in the premises and the whole statement is a lie.

How to correctly define All?
What's wrong with my proof?

SCappella SCappella · Accepted Answer · 2019-04-26T21:02:11

All should take [] to True. This is essentially because of vacuous truth, but you can see how not doing that caused problems.

Not having All P [] be true also makes your lemma false. For all x, In x [] is false. But false implies anything, including P x, so we have forall x, In x [] -> P x. But if All P [] is false, then the two statements can't be equivalent.

Logic: All definition and All_In theorem

1 Answers