[Agda] without-K problem
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jun 20 08:39:00 CEST 2012
On 18.06.12 9:18 PM, Guillaume Brunerie wrote:
> Hi all,
>
> For what it’s worth, I cannot reproduce the bug using the following
> definition of the identity types:
>
> data _≡_ {A : Set} : A → A → Set where
> refl : {x : A} → x ≡ x
>
> But I can reproduce it using the following definition (which is the one
> used in the standard library):
>
> data _≡_ {A : Set} (x : A) : A → Set where
> refl : x ≡ x
Yes, it seems --without-K should also forbid data definitions where a
parameter variable ("x") is free in a index position.
Otherwise, index variables can be "hidden" in parameter positions and
are not spotted by --without-K when it checks whether a split is legal.
But then, of course, --without-K is no longer a local check and
--without-K modules may only import --without-K modules.
Cheers,
Andreas
> 2012/6/18 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk
> <mailto:psztxa at exmail.nottingham.ac.uk>>
>
> Hi Nisse,
>
> I noticed that a weak version of K is provable even though the
> without-K flag is set:
>
> {-# OPTIONS --without-K #-}
> module K-bug where
>
> open import Relation.Binary.PropositionalEquality
>
> weakK : {A : Set}{a b : A}(p q : a ≡ b)(α β : p ≡ q) → α ≡ β
> weakK refl .refl refl refl = refl
>
> This would imply that all types have dimension of at most 3. I don't
> think it is provable with J.
>
> A simpler term which is provable but shouldn't was found by my
> student Nicolai:
>
> weak2 : {A : Set} {a : A} (α : refl {x = a} ≡ refl) → α ≡ refl
> weak2 refl = refl
>
> It seems to me that these patterns satisfy the specification of
> without-K (I.e. the condition is too weak).
>
> Do you see a fix?
>
> Cheers,
> Thorsten
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list