[Agda] Proof of False

[Andrés Sicard-Ramírez]

Hi Dan,

This bug was fixed just 3 hours ago

http://code.google.com/p/agda/issues/detail?id=160&can=1&start=100


On Mon, May 11, 2009 at 9:26 AM, Dan Doel <dan.doel at gmail.com> wrote:
> Greetings,
>
> I was playing around a bit this morning, and noticed that Agda accepts the
> following.
>
> ---- snip ----
>
> module Injective where
>
> data _≡_ {a : Set} : a → a → Set where
>  ≡-refl : (x : a) → x ≡ x
>
> injective : ∀{a b} → (a → b) → Set
> injective f = ∀{x y} → f x ≡ f y → x ≡ y
>
> inj-all : ∀{a b} {f : a → b} → injective f
> inj-all {a} {b} {f} {.y} {y} (≡-refl .(f y)) = ≡-refl y
>
> ---- snip ----
>
> This appears to be a proof that all functions are injective (Agda even did
> most of the writing, as I only performed a C-c C-c on the left-hand proof, and
> filled in the obvious right-hand side). I showed it to a cohort, who verified
> that it was still accepted by a more recent snapshot than mine, and furnished
> me with the following:
>
> ---- snip ----
>
> data XY : Set where
>  X : XY
>  Y : XY
>
> const : {a b : Set} -> a -> b -> a
> const k n = k
>
> test-1 : injective (const X)
> test-1 = inj-all {XY} {XY} {const X}
>
> test-2 : X ≡ Y
> test-2 = test-1 (≡-refl (const X X))
>
> data bot : Set where
>
> test-3 : X ≡ Y -> bot
> test-3 ()
>
> test-4 : bot
> test-4 = test-3 test-2
>
> ---- snip ----
>
> which looks undesirable. :)
>
> Cheers,
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés