[Agda] Proving equality of pairs

[Andreas Abel]

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/