[Agda] Proving equality of pairs

[Andreas Abel]

On Sep 25, 2010, at 3:06 AM, Brandon Moore wrote:
> I see how that is fixed. I don't understand the example with  
> heterogeneous
> inequality.
> I thought i understood why inference does not succeed, but it turns  
> out
> providing
> just one of the implicit arguments to _≅_ is sufficient.
>
> In each pair the first type argument is easily found to be A, an in  
> each pair
> the
> second type argument to Σ gives rise to unification problem, so we  
> have
> ?B1 A B x1 x2 y1 y2 x1 = B x1
> ?B2 A B x1 x2 y1 y2 x2 = B x2
>
> The first has solutions ?B1 _ _ _ _ _ _ = B and ?B1 _ _ x1 _ _ _ =  
> (λ _ → B x1)
> The second has solutions ?B1 _ _ _ _ _ _ = B and ?B1 _ _ _ x2 _ _ =  
> (λ _ → B x2)
>
> I don't see how constraining one or the other fixes enough for the
> definition to go through.

The reason is that there is also an equation between ?B1 and ?B2,  
namely,

   ?B1 A B x1 x1 y1 y1 x = ?B2 A B x1 x1 y1 y1 x

So giving a solution for one solves the other.

What Agda actually produces (with option-v tc.meta:20) is essentially  
the constraints:

term _26 A B x1 x2 y1 y2 x1 := B x1
term _33 A B x1 x2 y1 y2 x2 := B x2
term _33 A B x1 x1 y1 y1 x  := _26 A B x1 x1 y1 y1 x

After doing a free-variable analysis we could arrive at

term _26 _ B x1 _ _ _ x1 := B x1
term _33 _ B _ x2 _ _ x2 := B x2
term _33 _ B _ x1 _ _ x  := _26 _ B x1 _ _ _ x

Equating _33 and _26 shows that the 2nd eq. is redundant

term _26 _ B x2 _ _ _ x2 := B x2

But still there are two solutions

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

At the end of declaration product-congr, Agda could solve
aggressively, since these metavars are scoped withing the declaration,
so Agda could choose just one of the solutions.

However, the algorithm must take all constraints into consideration,
that might not be straightforward to implement in general.

> open import Relation.Binary.HeterogeneousEquality
> open import Data.Product

> product-congr :
>  (A : Set)(B : A -> Set)(x1 x2 : A)(y1 : B x1)(y2 : B x2)
>    -> x1 ≅ x2 -> y1 ≅ y2
>    -> (x1 , y1) ≅ (x2 , y2)
> product-congr A B x1 .x1 y1 .y1 refl refl = refl

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/