UlfNorell
commented
10 years ago From nils.anders.danielsson on August 29, 2013 05:09:58
I would expect the goal to become @⊥ ≡ ⊥@!?
That wouldn't be correct. Note, however, that some information is (by default) displayed differently in the development version. From the current release notes for 2.3.4:
-
Key bindings for controlling simplification/normalisation:
[TODO: Simplification should be explained somewhere.]
Commands like "Goal type and context" (C-c C-,) could previously be invoked in two ways. By default the output was normalised, but if a prefix argument was used (for instance via C-u C-c C-,), then no explicit normalisation was performed. Now there are three options:
- By default (C-c C-,) the output is simplified.
- If C-u is used exactly once (C-u C-c C-,), then the result is neither (explicitly) normalised nor simplified.
- If C-u is used twice (C-u C-u C-c C-,), then the result is normalised.
[TODO: As part of the release of Agda 2.3.4 the key binding page on the wiki should be updated.]
See issue 850 .
I am not entirely convinced that the new simplification is useful. What do you think? (Please post your answer, if any, on the other ticket's page.)
Status: Invalid
From stevan.a...@gmail.com on August 28, 2013 16:41:34
module Bug2 where
record Monad (M : Set → Set) : Set₁ where field return : ∀ {A} → A → M A >>= : ∀ {A} {B : M A → Set} (m : M A) → ((x : A) → M (B (return x))) → M (B m)
data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x
subst : ∀ {A : Set} {x y} (P : A → Set) → x ≡ y → P x → P y subst P refl p = p
postulate ext : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
data ⊥ : Set where
¬_ : Set → Set ¬ A = A → ⊥
¬¬-monad : Monad (λ A → ¬ ¬ A) ¬¬-monad = record { return = return ; >>= = >>= } where return : ∀ {A} → A → ¬ ¬ A return x ¬x = ¬x x
-- Both @¬x x@ and @m ¬x@ normalise to ⊥ in the goal below when using -- C-., but they don't normalise further in the goal nor when using -- C-n. I would expect the goal to become @⊥ ≡ ⊥@!? >>= : ∀ {A} {B : ¬ ¬ A → Set} (m : ¬ ¬ A) → ((x : A) → ¬ ¬ B (return x)) → ¬ ¬ B m >>= {B = B} m k ¬y = m (λ x → k x (λ y → ¬y (subst B (ext (λ ¬x → {!¬x x!})) y)))
Original issue: http://code.google.com/p/agda/issues/detail?id=890