[Agda] Agda master is anti-classical, injective type constructors
are back
Andrea Vezzosi
sanzhiyan at gmail.com
Sat Jan 17 19:56:33 CET 2015
I don't think we should change the meaning of a ~= b, which should be
given by the natural eliminator for that inductive type, like J is for
homogeneous equality. All of this orthogonal from whether K is there
or not.
The fact that one needs to know n == m to make sensible use of (i :
Fin n) ~= (j : Fin m) is, or should be, already there, because the
latter only gives us Fin n == Fin m.
(Fin might not be the best example, because it's provably injective
from the eliminators: I wouldn't expect pattern matching to figure
that out automatically but I wouldn't mind if it did.)
The SING case is similar, we should only get something like (eq : SING
F == SING G) and (cast eq (sing F) == sing G).
In other words, (a : A) ~= (b : B) -> A == B ought to be provable, and
not the culprit.
A variation of your inj-Fin shows that --without-K is also
inconsistent with univalence at the moment, since this is accepted:
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 ()
It's easy to get a proof of (zero : Fin 2) ~= (suc zero : Fin 2) by
univalence, allowing a closed proof of ⊥.
A argument of type "zero ≅ suc i" is not absurd.
Cheers,
Andrea
On Sat, Jan 17, 2015 at 12:07 PM, Andreas Abel <abela at chalmers.se> wrote:
> 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
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: FinEq.agda
Type: application/octet-stream
Size: 984 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150117/03e84ea1/FinEq-0001.obj
More information about the Agda
mailing list