Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]unfolding a corecursive function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]unfolding a corecursive function


chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]unfolding a corecursive function
  • Date: Mon, 10 Jul 2006 08:28:27 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Keiko Nakata wrote:

Hello, I have been struggling to prove "unfold" lemma for a corecursive function. Please help me with any advice.


Hello,
Here is a adaptation of the example in Section 13.4 of the Coq'Art "Unfolding Techniques" to your example.
Hope this helps,

Best regards,

Pierre



Inductive Lab : Set := T | C.
Inductive triple (A B C: Set) : Set := tpl : A -> B -> C -> triple A B C.

CoInductive Trace : Set := Cons : Lab -> Trace -> Trace.

Definition Trace_decompose (t : Trace) : Trace :=
match t with Cons l t => Cons l t end.

Lemma Trace_decompose_lemma : forall t, t = Trace_decompose t.
Proof.
intro t; case t;trivial.
Qed.

Ltac Trace_unfold term := apply trans_equal with
(1:= Trace_decompose_lemma term).

Parameter Env : Set.
Parameter Proc : Set.

(* Given an environment E and a process p,
"trs E p" returns a new environment, a label and a new process,
i.e., trs gives one step transition. *)
Parameter trs : Env -> Proc -> triple Env Lab Proc.

CoFixpoint trace_of (E: Env) (p: Proc) : Trace := match trs E p with
| tpl E1 l1 p1 => Cons l1 (trace_of E1 p1) end.

(* I cannot prove this lemma *)
Lemma unfold_trace_of :
forall (E: Env) (p: Proc), trace_of E p =
match trs E p with | tpl E1 l1 p1 => Cons l1 (trace_of E1 p1) end.
intros.
Trace_unfold (trace_of E p).
simpl .
case (trs E p).
auto.
Qed.







Archive powered by MhonArc 2.6.16.

Top of Page