Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]unfolding a corecursive function


chronological Thread 
  • From: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]unfolding a corecursive function
  • Date: Mon, 10 Jul 2006 14:59:08 +0900 (JST)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

I am to define a simple transition system.

(* Labels are either T or C *)
Inductive Lab : Set := T | C.
Inductive triple (A B C: Set) : Set := tpl : A -> B -> C -> triple A B C.

(* Traces are streams of labels *)
CoInductive Trace : Set :=  Cons : Lab -> Trace -> Trace.

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.
 

By the way, I cannot use the interactive search index of coq-club.
I always get an answer "Found 0 matches in 0 files.".
How can I use it properly ? 

With best regards,
Keiko Nakata.





Archive powered by MhonArc 2.6.16.

Top of Page