# Injectivity of type constructors is partially back. Agda refutes excluded middle #1406

Closed
opened this Issue Aug 8, 2015 · 1 comment

Projects
None yet
2 participants

### GoogleCodeExporter commented Aug 8, 2015

 Concerns: Agda master (not maint) ```-- Andreas, 2015-01-16 -- Agda with K again is inconsistent with classical logic -- {-# OPTIONS --without-K #-} open import Common.Level open import Common.Prelude open import Common.Equality cast : {A B : Set} (p : A ≡ B) (a : A) → B cast refl a = a data HEq {α} {A : Set α} (a : A) : {B : Set α} (b : B) → Set (lsuc α) where refl : HEq a a mkHet : {A B : Set} (eq : A ≡ B) (a : A) → HEq a (cast eq a) mkHet refl a = refl -- Type with a big forced index. (Allowed unless --without-K.) -- This definition is allowed in Agda master since 2014-10-17 -- https://github.com/agda/agda/commit/9a4ebdd372dc0510e2d77e726fb0f4e6f56781e8 -- However, probably the consequences of this new feature have not -- been grasped fully yet. data SING : (F : Set → Set) → Set where sing : (F : Set → Set) → SING F -- The following theorem is the culprit. -- It needs K. -- It allows us to unify forced indices, which I think is wrong. thm : ∀{F G : Set → Set} (a : SING F) (b : SING G) (p : HEq a b) → F ≡ G thm (sing F) (sing .F) refl = refl -- Note that a direct matching fails, as it generates heterogeneous constraints. -- thm a .a refl = refl -- However, by matching on the constructor sing, the forced index -- is exposed to unification. -- As a consequence of thm, -- SING is injective which it clearly should not be. SING-inj : ∀ (F G : Set → Set) (p : SING F ≡ SING G) → F ≡ G SING-inj F G p = thm (sing F) _ (mkHet p (sing F)) -- The rest is an adaption of Chung-Kil Hur's proof (2010) data Either {α} (A B : Set α) : Set α where inl : A → Either A B inr : B → Either A B data Inv (A : Set) : Set1 where inv : (F : Set → Set) (eq : SING F ≡ A) → Inv A ¬ : ∀{α} → Set α → Set α ¬ A = A → ⊥ -- Classical logic postulate em : ∀{α} (A : Set α) → Either A (¬ A) Cantor' : (A : Set) → Either (Inv A) (¬ (Inv A)) → Set Cantor' A (inl (inv F eq)) = ¬ (F A) Cantor' A (inr _) = ⊤ Cantor : Set → Set Cantor A = Cantor' A (em (Inv A)) C : Set C = SING Cantor ic : Inv C ic = inv Cantor refl cast' : ∀{F G} → SING F ≡ SING G → ¬ (F C) → ¬ (G C) cast' eq = subst (λ F → ¬ (F C)) (SING-inj _ _ eq) -- Self application 1 diag : ¬ (Cantor C) diag c with em (Inv C) | c diag c | inl (inv F eq) | c' = cast' eq c' c diag _ | inr f | _ = f ic -- Self application 2 diag' : Cantor C diag' with em (Inv C) diag' | inl (inv F eq) = cast' (sym eq) diag diag' | inr _ = _ absurd : ⊥ absurd = diag diag'``` This development was fathered by my surprise that I could prove ` inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m` but not by directly matching on the heterogeneous equality (which Agda refuses as Fin n = Fin m does not yield n = m), but by first matching on i and j, which exposes n and m in the constructor patterns and makes then available for unification. ``` inj-Fin-≅ {i = zero} {zero} ≅refl = refl -- matching on ≅refl succeeds! inj-Fin-≅ {i = zero} {suc j} () inj-Fin-≅ {i = suc i} {zero} () inj-Fin-≅ {i = suc i} {suc j} p = {!p!} -- Splitting on p succeeds!``` This is weird. A fix would be to not generate any unification constraints for forced constructor arguments, for instance ``` fzero : (n : Nat) -> Fin (suc n) fzero n : Fin (suc n) =?= fzero m : Fin (suc m)``` would not simplify to `n =?= m : Nat`. This change might break developments using heterogeneous equality, as did the fix of issue #292. Original issue reported on code.google.com by `andreas....@gmail.com` on 17 Jan 2015 at 10:59

### GoogleCodeExporter commented Aug 8, 2015

 Fixed by 06c6e1c. Standard library compiles fine. Original comment by `andreas....@gmail.com` on 19 Jan 2015 at 2:28 Changed state: Fixed Added labels: Forcing

Closed

Closed

Closed

Closed