Heterogeneous pattern matching incompatible with univalence [Re: [Agda] Agda master is anti-classical, injective type constructors are back]

[Andreas Abel]

I fixed the problem I reported (anti-classicality), but the 
incompatibility with univalence as reported by Andrea is still open, see:

   https://code.google.com/p/agda/issues/detail?id=1408

{-# OPTIONS --without-K #-}

open import Data.Fin
open import Relation.Binary.HeterogeneousEquality -- only using the type
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Empty
open import Data.Unit

OffDiag : ∀ {n m} → Fin n → Fin m → Set
OffDiag zero    zero    = ⊥
OffDiag (suc _) (suc _) = ⊥
OffDiag _       _       = ⊤

inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → OffDiag i j → ⊥
inj-Fin-≅ {i = zero}  {zero} eq ()
inj-Fin-≅ {i = zero}  {suc j} ()
inj-Fin-≅ {i = suc i} {zero} ()
inj-Fin-≅ {i = suc i} {suc j} p ()

cast : ∀ {α} → {A B : Set α} (p : A ≡ B) (a : A) → B
cast refl a = a

intro : ∀ {A B : Set}{a b} → (eq : A ≡ B) → cast eq a ≡ b → a ≅ b
intro refl refl = refl

-- we can get these from univalence
postulate
   swap : Fin 2 ≡ Fin 2
   swap-lemma : cast swap zero ≡ suc zero

bottom : ⊥
bottom = inj-Fin-≅ (intro swap swap-lemma) _

On 18.01.2015 15:58, Andrea Vezzosi wrote:
> According to "A few constructions on constructors" the types don't
> need to be strictly equal, but in addition of having the same shape
> you need equality constraints for all the arguments of the family.
>
> For example the following collection of constraints simplifies to
> false even when e1 and e2 are not unifiable:
> (e1 : Nat =?= e2 : Nat) & (zero : Fin (suc e1) =?= suc i : Fin (suc e2))
>
> while (zero : Fin (suc e1) =?= suc i : Fin (suc e2)) alone is undecided.
>
> Cheers,
> Andrea
>
> On Sun, Jan 18, 2015 at 3:38 PM, Andreas Abel <abela at chalmers.se> wrote:
>> The answer to your question can be found here:
>> https://code.google.com/p/agda/issues/detail?id=292
>>
>> Originally, equality of types was not checked at all (clearly buggy), then
>> equality of types was checked, but that fix was considered to restrictive.
>> We settled in the middle: it is sufficient that the types have the same
>> shape, i.e., both are instances of the Fin type.
>>
>> Cheers,
>> Andreas
>>
>>
>> On 17.01.2015 23:03, Matthieu Sozeau wrote:
>>>
>>> Hi,
>>>
>>>     I'm curious here:
>>>
>>>     fzero n : Fin (suc n) =?= fzero m : Fin (suc m) -> n =?= m
>>>
>>> How come this is not postponed due to the fact that the types are
>>> different?
>>> -- Matthieu
>>>
>>> 2015-01-17 16:37 GMT+05:30 Andreas Abel <abela at chalmers.se>:
>>>>
>>>> This concerns only the unreleased Agda master development branch.
>>>>
>>>> Using heterogeneous equality and big forced indices in a data type SING,
>>>> I
>>>> manage to prove injectivity of type constructor
>>>>
>>>>     SING : (Set -> Set) -> Set
>>>>
>>>> The rest follows Chung-Kil Hur's refutation of excluded middle, as
>>>> published
>>>> in January 2010 on the Coq and Agda lists.
>>>>
>>>> My 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 would break a lot of developments using heterogeneous
>>>> equality,
>>>> as did the fix of issue 292
>>>> (https://code.google.com/p/agda/issues/detail?id=292).  In particular,
>>>> heterogeneous equality would not imply the equality of the types, but the
>>>> equality of the types has to be given in order to sensibly work with
>>>> heterogeneous equality.  In case of Fin, one would work with telescopes
>>>>
>>>>     {n m : Nat} (p : n == m) {i : Fin n} {j : Fin m} (q : i ~= j)
>>>>
>>>> rather than being able to derive p from q.
>>>>
>>>> This is Conor McBride's proposal for heterogeneous equality, if I am not
>>>> mistaken.
>>>>
>>>> RFC,
>>>> Andreas
>>>>
>>>> --
>>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>>>
>>>> Department of Computer Science and Engineering
>>>> Chalmers and Gothenburg University, Sweden
>>>>
>>>> andreas.abel at gu.se
>>>> http://www2.tcs.ifi.lmu.de/~abel/
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>
>>>
>>>
>>
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Department of Computer Science and Engineering
>> Chalmers and Gothenburg University, Sweden
>>
>> andreas.abel at gu.se
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/