Manuel Eberl

2016-09-26 11:21:27 UTC

Permalink

Hallo,Raw Message

I don't know awfully much about friends and corecursion, but in my

naïveté, I simply added "(friend)" to a reasonably friendly-looking

corecursive definition and expected it to work. Instead, it looped. A

minimal non-working example is the following:

type_synonym ae = "(real × real) stream"

corec (friend) add_ae :: "ae ⇒ ae" where

"add_ae f = ((fst (shd f), snd (shd f)) ## add_ae (stl f))"

This runs for about 3 seconds and then returns with the following error:

Tactic failed

The error(s) above occurred for the goal statement⌂:

rel_fun (rel_prod R (rel_pre_stream op = R))

(rel_pre_stream op = (rel_ssig_stream_v1 R))

(λf. ((fst (fst (snd f)), snd (fst (snd f))),

stream.v1.Oper

(stream.v1.Sig

(Inr

(case snd f of

(x1, x2) ⇒ stream.v1.VLeaf x2)))))

(λf. ((fst (fst (snd f)), snd (fst (snd f))),

stream.v1.Oper

(stream.v1.Sig

(Inr

(case snd f of

(x1, x2) ⇒ stream.v1.VLeaf x2)))))

The problem does not occur if I replace "(fst (shd f), snd (shd f))"

with the equivalent "shd f".

A similar, slightly less vacuous definition that is closer to my

original definition is the following:

corec (friend) add_ae :: "ae ⇒ ae ⇒ ae" where

"add_ae f g = ((fst (shd f) + fst (shd g), snd (shd f)) ## add_ae

(stl f) (stl g))"

That also causes a similar error, but it takes about 110 seconds to get

there. The command defining the function I originally had in mind has

not terminated yet.

Cheers,

Manuel