[Agda] (no subject)

[Andreas Abel]

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/