The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Edsko,

I am copying the Coq club back in - hope this is ok. I also cc it to the Agda list since I find it easier to answer the question in Agda (the background to the discussion can be found in the coq club archive).

Suppose we have a function (count f) on streams which returns (f x1 + f x2 + ...); then we want to prove a lemma that

 h . count f ~ count (h . f)

for any morphism h (except of course that we don't want to prove this for lists but prove it polytypically; for an informal statement of this lemma, see Hinze's habilitationsschrift, http://www.iai.uni-bonn.de/~ralf/publications/habilitation.pdf, p 102, Section 4.3.2).

It seems to me that to prove this you basically need to show that + preserves ~. 

I implemented the relation I think you want to define in Agda using mixed induction/coinduction. First I define partial conatural numbers:

data CoNat' : Set where

  zero : CoNat'

  1+_ : ∞ CoNat' → CoNat'

  τ :  ∞ CoNat' → CoNat'

Here the recursive occurences marked with ∞ are coinductive. This is basically your type conat with the add constructor omitted. I call it CoNat' to make a difference to ordinary CoNat (without the τ ).

I define addition on partial coNaturals:

_+'_ : CoNat' → CoNat' → CoNat'

zero +' n = n

(1+ m) +' n = 1+ (♯ (♭ m) +' n)

(τ m) +' n = τ (♯ (♭ m) +' n)

To read this one has to know that ♭is "delay" and ♯ is "forcing". See our paper. 

Instead of defining the equality directly I define a preorder corresponding to "more defined" (Agda allows to reuse constructors hence I use the same name for the congruences rules).

data _⊑_ :  CoNat' → CoNat' → Set where

  zero : zero ⊑ zero

  1+_ :  ∀ {m n} → ∞ (♭ m ⊑ ♭ n) → 1+ m ⊑ 1+ n

  τ :  ∀ {m n} → ∞ (♭ m ⊑ ♭ n) → τ m ⊑ τ n

  τl : ∀ {m n} → (♭ m ⊑ n) → τ m ⊑ n

This is a mixed inductive/coinductive definition, a see the paper which was already mentioned by Nisse:

http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

The idea is that you can a less defined value may have a finite delay, hence here we use an inductive argument. However, we still need that 1+ and τ are congruences and hence their arguments have to be coinductive.

It is straightforward to show that ⊑ is a preorder:

refl⊑ : ∀ {m} → m ⊑ m

refl⊑ {zero} = zero

refl⊑ {1+ n} = 1+ (♯ (refl⊑ {♭ n}))

refl⊑ {τ n} = τ (♯ (refl⊑ {♭ n}))

trans⊑ : ∀ {l m n} → l ⊑ m → m ⊑ n → l ⊑ n

trans⊑ zero zero = zero

trans⊑ (1+ p) (1+ q) = 1+ (♯ trans⊑ (♭ p) (♭ q))

trans⊑ (τ p) (τ q) = τ (♯ trans⊑ (♭ p) (♭ q))

trans⊑ (τ p) (τl q) = τl (trans⊑ (♭ p) q)

trans⊑ (τl p) q = τl (trans⊑ p q)

Also it is not hard to show that +'  preserves ⊑:

cong+' : ∀ {m m' n n'} → m ⊑ m' → n ⊑ n' → (m +' n) ⊑ (m' +' n')

cong+' zero q = q

cong+' (1+ p) q = 1+ (♯ cong+' (♭ p) q)

cong+' (τ p) q = τ ((♯ cong+' (♭ p) q))

cong+' (τl p) q = τl (cong+' p q)

The relation ~ I think you want to define is simply the symmetric closure of ⊑ (and hence an equivalence relation). And cong+' implies that ~ is a congruence wrt +' which is sufficent to prove your result I think.

It shouldn't be too hard to translate this into Coq - the mixed inductive/coinductive definition you have to replace with a nested coinductive - inductive definition. You may have to spend some time to derive the appropriate induction and coinduction principles because they are not generated automatically afaik.

Or use Agda... :-)

Cheers,

Thorsten

P.S. Here is the Agda file:

This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

Attachment: Edsko-short.agda
Description: Binary data