all_forallb

all.v

(** **** Exercise: 3 stars (all_forallb) *)
(** Inductively define a property [all] of lists, parameterized by a
    type [X] and a property [P : X -> Prop], such that [all X P l]
    asserts that [P] is true for every element of the list [l]. *)

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=
  | all_nil : all X P []
  | all_cons : forall (x : X) (xs : list X),
                 P x -> all X P xs -> all X P (x :: xs).

Inductive all_and (X : Type) (P : X -> Prop) : list X -> Prop :=
  | all_and_nil : all_and X P []
  | all_and_cons : forall (x : X) (xs : list X),
                     P x /\ all_and X P xs -> all_and X P (x :: xs).

Theorem all__all_and : forall (X : Type) (P : X -> Prop) (xs : list X),
                         all X P xs -> all_and X P xs.
Proof.
  intros.
  induction xs as [|y ys].
  Case "xs = []".
    apply all_and_nil.
  Case "xs = y::ys".
    apply all_and_cons.
    inversion H.
    split.
    SCase "left".
      apply H2.
    SCase "right".
      apply IHys. apply H3.
Qed.

Theorem all_and__all : forall (X : Type) (P : X -> Prop) (xs : list X),
                         all_and X P xs -> all X P xs.
Proof.
  intros.
  induction xs as [|y ys].
  Case "xs = []".
    apply all_nil.
  Case "xs = y::ys".
    inversion H.
    inversion H1.
    apply all_cons.
    apply H3.
    apply IHys.
    apply H4.
Qed.