[Agda] (no subject)

[Ernesto Copello]

Thanks very much for your quick response !

Ok I need to generalize R to the sized version of D. But don't you think
the next version of R is more specific ?

data R : D → D → Set where
    r1 : ∀{i}(n : ℕ) → R (d1 {i} n) (d1 {i} n)
    r2 : ∀{i}(d : D {i}) → R (op d) (op d) → R (d2 d) (d2 d)

I already check that this version works too.

I understand your version indirectly size the elements of D, sizing the
elements of R. While in this version I only size D elements not the hole
relation R. In this example only D must be sized, because of I am doing
induction in the length of D, not R.

In fact, I want to know why I have to give explicit information about the
size of the elements of D in R ? I belive that when no information was
given, then ∞ size was assumed, and ∞ unificates with any size. So I don't
understand the error : ∞ != .ι that gives Agda's compiler with the original
version of R.

Cheers,
Ernesto


On Wed, Jun 25, 2014 at 4:24 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> Hi Ernesto,
>
> you can generalize R to speak about the sized version of D:
>
>   data R : ∀{i} → D {i} → D {i} → Set where
>     r1 : ∀{i}(n : ℕ) → R {↑ i} (d1 n) (d1 n)
>     r2 : ∀{i}(d : D) → R {i} (op d) (op d) → R {↑ i} (d2 d) (d2 d)
>
> Then the following function termination-checks:
>
>   ρ-good :  {ι : Size} → Reflexive (R {ι})
>   ρ-good {x = d1 x} = r1 x
>   ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>
> Cheers,
> Andreas
>
> On 25.06.2014 15:04, Ernesto Copello wrote:
>
>>
>> {-# OPTIONS --sized-types #-}
>> module problem where
>>
>> open import Size
>> open import Data.Nat
>>
>> open import Relation.Binary
>> open import Relation.Binary.PropositionalEquality
>>
>> data D : {ι : Size} → Set where
>>    d1 : {ι : Size} → ℕ → D {↑ ι}
>>    d2 : {ι : Size} → D {ι} → D {↑ ι}
>>
>> -- d1 n, d2 (.. d2 (d1 n))
>>
>>
>> postulate
>>    op : {ι : Size} → D {ι} → D {ι}
>>    pr : {x : D} → op x ≡ x
>>
>> -- Some reflexive binary relation
>> data R : D → D → Set where
>>    r1 : (n : ℕ) → R (d1 n) (d1 n)
>>    r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)
>>
>>
>> -- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))
>>
>> good : D → D
>> good x with op x | pr {x}
>> ... | .x | refl = x
>>
>> -- We are not able to do the same as above with size information
>> annotations, the following commented code does not compile:
>>
>> -- problem : {ι : Size} → D {ι} → D
>> -- problem x with op x | pr {x}
>> -- ... | .x | refl = {! !}
>>
>> ρ-good : Reflexive R
>> ρ-good {x = d1 x} = r1 x
>> ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>>
>> -- To pass the termination checking algorithm, we add size information to
>> the type signature of the previous code, but another problem arises, and
>> now the proofs do not pass type checking.
>>
>> ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R
>> ρ-problem {x = d1 x} = {! r1 x!}
>> ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140625/5f27a5bf/attachment.html