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

[Thorsten Altenkirch]

P.S. I realize that my definition of ~ is not right, it is just  
extensional equality (bisimulation) on partial CoNats. The relation I  
want is rather:

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
   τr : ∀ {m n} → (m ≈ ♭ n) → m ≈ τ n

I.e. you can change the number of τs by a finite amount.

It is easy to show that it is a congruence for +'  but Agda doesn't  
seem to like my proof of transitivity (even though I am quite sure it  
is transitiv).

On 25 Aug 2009, at 18:31, Thorsten Altenkirch wrote:

> 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.
>
> <Edsko-short.agda>
>
>
>
>
>
>
>
>
>
>
>
>


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 --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090826/f3dd8611/attachment.html