[Agda] slightly wrong sized datatype definition leads to proof of False

[Frédéric Blanqui]

Hello. I see many problems with sized types in Agda. Is it really just a 
matter of implementation? Some issues are several years old and haven't 
been fixed yet. I am curious: where are described the theoretical 
grounds of the current implementation?

Le 19/10/2020 à 11:15, Manuel Bärenz a écrit :
> Thanks for finding this. I guess this is in a longer tradition of
> problems with the sized types implementation, see e.g.
> https://github.com/agda/agda/issues/2820,
> https://github.com/agda/agda/issues/3026,
> https://github.com/agda/agda/issues/1428.
>
> I don't understand whether it has overlap with existing issues. You
> don't use the infinity size, nor equality. So maybe it's a new kind of
> issue, coming from interaction of sizes with inductive types?
>
> Anyways, I guess it makes sense to report at https://github.com/agda/agda?
>
> On 17.10.20 23:38, Vlad Rusu wrote:
>> The following code shows how a slightly wrong use of sized types in a
>> definition of natural numbers leads to a proof of  ⊥.
>>
>> --------------{-# OPTIONS --sized --safe  #-}
>> open import Relation.Binary.PropositionalEquality as Eq
>> open import Data.Empty using (⊥; ⊥-elim)
>> open import Size
>>
>>
>> -------------- auxiliary--------------
>> →-elim : ∀ {A B : Set}  → (A → B)  → A  → B
>> →-elim L M = L M
>> -- a trick found on the Web_
>> data [Size<_] (i : Size) : Set where
>>    box : Size< i → [Size< i ]
>> unbox : ∀ {i} → [Size< i ] → Size< i
>> unbox (box j) = j
>>
>> --size eliminators
>> size-elim :  (P : Size → Set) → (∀ i → ((j : [Size< i ]) → P (unbox
>> j)) → P i) →  ∀ i → P i
>> size-elim P Hind i = Hind _ λ { (box j) → size-elim P Hind j }
>> size-elimproved : (P : Size → Set) → (∀ i → ((j : (Size< i)) → P j ) →
>> P i) →  ∀ i → P i
>> size-elimproved P Hind i = →-elim (λ {Hind' → size-elim P Hind' i })
>>                          λ {i' Hind' → Hind i' (λ { j' → Hind' (box
>> j')  }) }
>> ------------ end auxiliary-----------
>>
>> -- one might think that the following is a definition natural numbers
>> using some Size arguments
>> data ℕ  {s : Size} :  Set where
>>   zero :  ℕ
>>   suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>>
>> -- the definition is slightly wrong ("suc" should not contain
>> ()-parentheses) and leads to a proof of ⊥
>>
>> -- introducing foo, a certain natural number
>> foo : ℕ
>> foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _
>>
>> -- foo is a successor to itself
>> bar : foo ≡ suc foo
>> bar = refl
>>
>> -- which is forbidden
>> baz : ∀ (n : ℕ) → (n ≡ suc λ { _ } → n   ) → ⊥
>> baz _ ()
>>
>> --hence...
>> zut : ⊥
>> zut = baz foo bar
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda