[Agda] Proving equality of pairs

[Andreas Abel]

I pushed a patch that improves unification so now there is no yellow  
stuff anymore in the first definition...

On Sep 24, 2010, at 7:35 PM, Andreas Abel wrote:
> On Sep 24, 2010, at 6:53 PM, Brandon Moore wrote:
>> On Sept. 24, 2010, at 8:28:52 AM, Andreas Abel wrote:
>>> -- to get rid of the yellow stuff, you have to supply the hidden  
>>> argument A ofequality
>>> -- (or define a cartesian product type instead of using the  
>>> library's sigmatypes)
>>>
>>> no-yellow :
>>> (A B : Set)(x1 x2 : A)(y1 y2 : B) -> x1 ≡ x2 -> y1 ≡ y2 ->
>>> _≡_ {A = Σ A (λ _ → B)} (x1 , y1) (x2 , y2)
>>> no-yellow A B x1 .x1 y1 .y1 refl refl = refl
>>
>> I'm quite surprised this can't be inferred. I though Agda was using
>> higher order matching, which should be able to decide that
>> (λ _ → B) is the only possibility for the second argument to Σ
>
> Ok, lets look at it step by step.
>
> _,_ : (a : ?A) -> ?B a -> Sigma ?A ?B
>
> _,_ x1 : ?B x1 -> Sigma A ?B
> _,_ x1 y1 : Sigma A ?B  where ?B x1 = B.
>
> Similarly, we get ?B x2 = B.
>
> What is going on under the hood that meta-variables are modeled as  
> functions, applied to all bound variables in context.  So you get  
> really
>
> 1. (?B A B x1 x2 y1 y2) x1 = B
> 2. (?B A B x1 x2 y1 y2) x2 = B

These are non-linear patterns in the sense of Dale Miller's pattern  
unification.  However, since x1 and x2 are not free in B, they can be  
ignored, so we can solve this as

   ?B = \ A B x1 x2 y1 y2 x -> B

Happy hacking,
Andreas


On Sep 24, 2010, at 3:28 PM, Andreas Abel wrote:
> module EqProd where
>
> open import Relation.Binary.PropositionalEquality
> open import Data.Product
>
> -- just like this:
> product-congr :
> (A B : Set)(x1 x2 : A)(y1 y2 : B) -> x1 ≡ x2 -> y1 ≡ y2 ->
> (x1 , y1) ≡ (x2 , y2)
> product-congr A B x1 .x1 y1 .y1 refl refl = refl
>
> -- to get rid of the yellow stuff, you have to supply the hidden  
> argument A of equality
> -- (or define a cartesian product type instead of using the  
> library's sigma types)
>
> no-yellow :
> (A B : Set)(x1 x2 : A)(y1 y2 : B) -> x1 ≡ x2 -> y1 ≡ y2 ->
>  _≡_ {A = Σ A (λ _ → B)} (x1 , y1) (x2 , y2)
> no-yellow A B x1 .x1 y1 .y1 refl refl = refl
>
> On Sep 24, 2010, at 12:01 PM, David Leduc wrote:
>
>> Hi,
>>
>> Newbie's question again. Sorry!
>>
>> How would you prove the simple lemma below?
>> Is it already in the standard library?
>> Why the first comma becomes yellow when I load the file?
>>
>>
>> module test where
>>
>> open import Relation.Binary.PropositionalEquality
>> open import Data.Product
>>
>> product-congr :
>> (A B : Set)(x1 x2 : A)(y1 y2 : B) ->
>> x1 ≡ x2 -> y1 ≡ y2 -> (x1 , y1) ≡ (x2 , y2)
>> product-congr A B x1 x2 y1 y2 = λ p q → {!!}
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

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/