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

[Thorsten Altenkirch]

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.

-------------- next part --------------
Skipped content of type multipart/mixed