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

[Manuel Bärenz]

We should discuss this as well at AIM today after the talk.

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