CODEWITHSUNDEEP
coqproofcoinduction
pjm
pjm

Reputation: 279

Coinductive principle for streams

I am trying to prove the following principle for stream predicates (defined in the standard library).

From Coq Require Import Streams.

Lemma mystream_ind :
  forall A (P : Stream A -> Prop),
    (forall s, ForAll P (tl s) -> ForAll P s) ->
    forall s, ForAll P s.
Proof.
  intros A P H.
  cofix Cof.
  destruct s as [a s].
  constructor; auto.
  destruct (H (Cons a s) (Cof s)); auto.
  Fail Guarded.
Abort.

From my understanding of the syntactical guard conditions imposed by cofix, I will never be able to complete the proof this way because in the proof term, Cof s must appear under H, which is not a constructor nor a match, etc.

Is there another way to do it in Coq? I defined ForAll as an explicit fixpoint with paco and tried to prove the principle, without success (I couldn't instantiate H at all).

EDIT: this lemma is not provable as False can be derived from it by taking P := fun s => False (thank you Maëlan).

Upvotes: 2

Views: 156

Answers (0)

Related Questions