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

[Jesper Cockx]

Hi Vlad,

I just fixed issue #4995 this morning, this also means your example is no
longer accepted by the development version of Agda:

Failed to solve the following constraints:
>   Is empty: n ≡ suc (λ {_} → n) (blocked on _s_49)
>

-- Jesper

On Sat, Oct 17, 2020 at 11:39 PM Vlad Rusu <Vlad.Rusu at inria.fr> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201022/ea1a35bb/attachment.html>