Two-step induction of inductive predicate on Streams

Question

If I want to have an induction principle for nats from n to n+2, I can define and prove this lemma (from "Can I tell Coq to do induction from n to n+2?" on StackOverflow):

Lemma nat_ind2 (P : nat -> Prop) :
  P 0 -> P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros H0 H1 Hstep n.
  enough (P n /\ P (S n)) by easy.
  induction n; intuition.
Qed.

If I want to define in a similar way an induction principle for Exists from Coq.Lists.Streams, how should I do it? Looking at the definition of Exists_ind, I came up with the following principle. Is this the one I am looking for? Are all hypothesis necessary? Why is the base hypothesis different from the ones used in nat? is it because the type we are predicating on (Stream) is coinductive?

Lemma Exists_ind2 :
  forall (A : Type) (P P0 : Stream A -> Prop),
    (forall x : Stream A, P x -> P0 x) ->
    (forall x : Stream A, P x -> P0 (tl x)) -> (* is this hypothesis necessary? *)
    (forall x : Stream A, Exists P (tl (tl x)) -> P0 (tl (tl x)) -> P0 (tl x) -> P0 x) ->
    forall x : Stream A, Exists P x -> P0 x.

Answer 1

Do you mean the induction principle generated by the following definition ?

Inductive Exists2 (P: Stream A -> Prop) : Stream A -> Prop:=
  here: forall s, P s -> Exists2 P s
| next : forall x s, P s -> Exists2 P (Cons x s)
| next2 : forall x y s, Exists2 P s -> Exists2 P (Cons x (Cons y s)). 


About Exists2_ind. 

Or something similar ?

Answer 2

For anyone looking for a similar solution, here's how I solved the problem.

First solution

Define a inductive predicate Exists2 as suggested by @Pierre Castéran, and then prove that forall P s, Exists P s <-> Exists2 P s.

Inductive Exists2 (P: Stream A -> Prop) : Stream A -> Prop:=
  | Here2    : forall s, P s -> Exists2 P s
  | There2   : forall x s, P s -> Exists2 P (Cons x s)
  | Further2 : forall x y s, Exists2 P s -> Exists2 P (Cons x (Cons y s)). 

Lemma Exists_iff_Exists2 : forall (P : Stream A -> Prop) (s : Stream A), Exists P s <-> Exists2 P s.
Proof.
  intros P s. split; intro H.
  - enough (Exists2 P s /\ forall x, Exists2 P (Cons x s)) by easy.
    induction H as [s H | s H IHExists].
    + split.
      * apply Here2. apply H.
      * intro x. apply There2. apply H.
    + destruct s as [y s]. split.
      * apply IHExists.
      * intro x. apply Further2. apply IHExists.
  - induction H as [s H | x s H | x y s H IHExists2].
    + apply Here. apply H.
    + apply Further. apply Here. apply H.
    + apply Further. apply Further. apply IHExists2.
Qed.

When an two-step induction on some H : Exists P s, it's sufficient to apply Exists_iff_Exists2 in H. induction H.

Second solution

Prove the following lemma:

Lemma Exists_ind2:
  forall (A : Type) (P P0 : Stream A -> Prop),
    (forall s : Stream A, P s -> P0 s) ->
    (forall (x : A) (s : Stream A), P s -> P0 (Cons x s)) ->
    (forall (x y : A) (s : Stream A), Exists P s -> P0 s -> P0 (Cons x (Cons y s))) ->
    forall s : Stream A, Exists P s -> P0 s.
Proof.
  intros A P P0 Hbase Hbase' Hstep s H.
  enough (P0 s /\ forall a, P0 (Cons a s)) by easy.
  induction H as [s H | s H IHExists].
  + split.
    * apply Hbase. apply H.
    * intro x. apply Hbase'. apply H.
  + destruct s as [y s]. replace (tl (Cons y s)) with s by reflexivity. split.
    * apply IHExists.
    * intro x. apply Hstep.
      -- apply H.
      -- apply IHExists.
Qed.

This lemma is indeed identical to the Exists2_ind that is generated by the inductive definition of Exists2 of the previous solution, with the only difference that all occurrences of Exists2 are replaced with Exists.

The proof itself is identical to the one of the lemma of the first solution, with the difference that instead of applying Exists2's constructors we apply inductive hypothesis.

---

Maybe this problem is trivial for many, don't bash me.

Answer 3

By the way, both your solutions remind me of a similar discussion about the transitive closure of a binary relation. We wanted to be able to perform induction proofs on x R^* y in three modes: from left to right, from right to left, and from the "middle". This led to define three inductive predicates and prove their logical equivalence.

https://coq.inria.fr/distrib/current/stdlib/Coq.Relations.Relation_Operators.html

https://coq.inria.fr/distrib/current/stdlib/Coq.Relations.Operators_Properties.html