[Agda] another possible without-K problem

drl at cs.cmu.edu drl at cs.cmu.edu
Wed Jul 10 18:17:20 CEST 2013 

I'm a bit confused about what you mean by p and q here.  Do you mean
"how do you prove that bool is an hset?"  You can prove that the
identity type at bool is equivalent to the recursive equality predicate 
(Eq True True = Unit, Eq True False = Void, etc.) using an encode-decode
argument.  See 
http://www.cs.cmu.edu/~drl/pubs/ls13pi1s1/ls13pi1s1.pdf
for the analogous argument for coproducts.  

Then you know that for all b1,b2, b1 == b2 is equivalent to an hprop, so
you can use the fact that hprop(X) respects equivalence (either by using
univalence, or by spelling out the proof explicitly for hprop(X)).

This proof will use J + large elims.    

-Dan
 

On Jul10, Andreas Abel wrote:
> Ah, so how do you prove then that p and q are the same equality proof, with 
> only J?
>
> On 10.07.2013 17:01, Altenkirch Thorsten wrote:
>>
>>
>> On 10/07/2013 15:52, "Dan Licata" <drl at cs.cmu.edu> wrote:
>>
>>> Is this a bug or a design decision?  It seems like this example is in
>>> accord with the description of without-K in the release notes, but
>>> that allowing matching when the indices are constructors has some
>>> interesting consequences.
>>
>> You are right since in the example S1 is just an inductive type this isn't
>> really a problem.
>>
>> Is this still possible if one "hides" the fact that S1 is inductively
>> defined?
>> I guess this is more the problem that the current implementation of HITs
>> is a bit of a hack.
>>
>> Disjointness was always built into pattern matching and it is hard to see
>> how to avoid this.
>> One only needs a microscopic universe, Bool with T : Bool -> Type to
>> justify this.
>>
>> Thorsten
>>
>>> In particular, it means that, in a core
>>> theory without universes, without-K pattern matching cannot be
>>> compiled to J, because you can prove disjointness (and injectivity) of
>>> constructors, and that bool is an hset (code below), just using
>>> pattern matching on the identity type.  As far as I know, disjointness
>>> and the hset-ness of bool require a universe/large elims to prove.  Of
>>> course, Agda has universes, and it is possible that without-K pattern
>>> matching could be compiled to J + uses of large elims to code up these
>>> constructions on constructors.  But I would personally prefer it if
>>> without-K pattern matching did not build these things in, because it
>>> means we need to use two hacks (rather than just one :) ) to implement
>>> higher inductives.
>>>
>>> -Dan
>>>
>>> -- checks in Agda 2.3.2.1
>>> {-# OPTIONS --without-K #-}
>>>
>>> module WithoutK where
>>>
>>>   data Nat : Set where
>>>     Z : Nat
>>>     S : Nat -> Nat
>>>
>>>   data Bool : Set where
>>>     True : Bool
>>>     False : Bool
>>>
>>>   data Void : Set where
>>>
>>>   data _==_ {A : Set} (x : A) : A -> Set where
>>>     Refl : x == x
>>>
>>>   injective : {m n : Nat} -> S m == S n -> m == n
>>>   injective Refl = Refl
>>>
>>>   disjoint : {m : Nat} -> S m == Z -> Void
>>>   disjoint ()
>>>
>>>   bool-hset : (b : Bool) -> (p : b == b) -> p == Refl
>>>   bool-hset True Refl = Refl
>>>   bool-hset False Refl = Refl
>>>
>>>
>>>
>>> On Wed, Jul 10, 2013 at 5:56 AM, Altenkirch Thorsten
>>> <psztxa at exmail.nottingham.ac.uk> wrote:
>>>> This looks like a bug – please add it to the bug tracker.
>>>>
>>>> We really need to understand what we are doing when checking wether
>>>> pattern
>>>> satisfy the —without-K condition. It seems that Conor's work on
>>>> translating
>>>> pattern matching to eliminators (with J and K) would be a good starting
>>>> point.
>>>>
>>>> At the same time we know that many types support UIP by structure.
>>>> Michael
>>>> Hedberg showed that all types with a decidable equality support UIP and
>>>> it
>>>> is not hard to see that this can be extended to stable equality (non-not
>>>> closed). (Little puzzle: without extensionality – are there any types
>>>> which
>>>> have stable but not decidable equality ?)
>>>>
>>>> We also want to quantify over all HSets (I.e. types with UIP) and so on.
>>>>
>>>> Thorsten
>>>>
>>>> From: Jason Reed <jcreed at gmail.com>
>>>> Date: Tue, 9 Jul 2013 16:31:22 +0100
>>>> To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
>>>> Subject: [Agda] another possible without-K problem
>>>>
>>>> I'm experiencing something that I think is a violation of the intent of
>>>> the
>>>> --without-K flag, similar to what Thorsten was talking about in
>>>> https://lists.chalmers.se/pipermail/agda/2012/004104.html.
>>>>
>>>> The following file checks fine for me under current darcs Agda:
>>>>
>>>> <<<begin>>>
>>>> {-# OPTIONS --without-K #-}
>>>>
>>>> module Test where
>>>>
>>>> data S1 : Set where
>>>>      base : S1
>>>>
>>>> module test where
>>>>     data _≡_ {A : Set} (a : A) : A → Set where
>>>>      refl : a ≡ a
>>>>
>>>>     bad : (p q : base ≡ base) -> p ≡ q
>>>>     bad refl refl = refl
>>>>
>>>> module test2 where
>>>>     data _≡_ {A : Set} : A → A → Set where
>>>>         refl : {x : A} → x ≡ x
>>>>
>>>>     bad : (p q : base ≡ base) -> p ≡ q
>>>>     bad refl refl = refl
>>>> <<<end>>>
>>>>
>>>> Note that this covers both the possible definitions of the identity type
>>>> mentioned by Guillaume in
>>>> https://lists.chalmers.se/pipermail/agda/2012/004105.html
>>>>
>>>> Any ideas what should be done here? Does the K-check need to be further
>>>> strengthened when there aren't parameters around? Am I misunderstanding
>>>> something trivial?
>>>>
>>>>
>>>> This message and any attachment are intended solely for the addressee
>>>> and
>>>> may contain confidential information. If you have received this message
>>>> in
>>>> error, please send it back to me, and immediately delete it.   Please
>>>> do not
>>>> use, copy or disclose the information contained in this message or in
>>>> any
>>>> attachment.  Any views or opinions expressed by the author of this
>>>> email do
>>>> not necessarily reflect the views of the University of Nottingham.
>>>>
>>>> This message has been checked for viruses but the contents of an
>>>> attachment
>>>> may still contain software viruses which could damage your computer
>>>> system,
>>>> you are advised to perform your own checks. Email communications with
>>>> the
>>>> University of Nottingham may be monitored as permitted by UK
>>>> legislation.
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> 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
>>
>
>
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/

More information about the Agda mailing list