coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Need help with coinductive proof

From: Edsko de Vries <edskodevries AT gmail.com>
To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
Cc: Coq Club <coq-club AT pauillac.inria.fr>, Agda List <agda AT lists.chalmers.se>
Subject: Re: [Coq-Club] Need help with coinductive proof
Date: Thu, 27 Aug 2009 16:09:01 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=xYmBDgHvXOFhGK+qf1k4wketZg+TVBTNOhcT9nSrQwZVnE9e+pYKDYD0vi1OEzbZdn qu5Fqp3zWuiS3IFrAXO5V2VLQpBFRIkSZdg/d6nvJTXE61zRhqSKOAL+iBqZyoSx+bSK TGmgVFX2Own9o4UVIl8RSP7RSOzvCoCk1OBkw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm very sorry to keep replying to myself. I was reading through the proof that Keiko sent when I realized that I could complete my symmetry proof without doing induction on d, but using some sort of double coinduction?

Lemma bisim_sym : forall m n,
� bisim m n -> bisim n m
with bisim'_sym : forall d m n,
� bisim' d m n -> bisim' d n m.
Proof.
(* first *)
� intros.
� inversion H ; clear H ; subst.
� apply (@bisim_delay d).
� apply bisim'_sym.
� assumption.
(* second *)
� intros.
� inversion H ; clear H ; subst.
(* weak_tau_left *)
� apply weak_tau_right.
� apply bisim'_sym.
� assumption.
(* weak_tau_right *)
� apply weak_tau_left.
� apply bisim'_sym.
� assumption.
(* strong_coZ *)
� apply strong_coZ.
(* strong_tau *)
� apply strong_tau.
� apply bisim_sym.
� assumption.
(* strong_coS *)
� apply strong_coS.
� apply bisim_sym.
� assumption.
Qed.

Not sure this is going to solve the rest of my difficulties, but we'll see ;)

Edsko

Re: [Coq-Club] Need help with coinductive proof, (continued)