[Agda] irrelevant fields and EqReasoning

[Andreas Abel]

Hi Noam,

irrelevant fields may produce more unsolved metas, since from

   record { irr = a } == record { irr = b }

you cannot conclude that a is equal to b.  In case a is a meta, no 
constraints are generated for a.

Sometimes a irrelevant meta can be solved by instance search.  However, 
only if a value of the type of the meta is directly in scope.  (These 
are the rules of instance search currently.)

There is a bit of discussion on this on

   http://code.google.com/p/agda/issues/detail?id=351

Cheers,
Andreas

On 16.07.2012 16:59, Noam Zeilberger wrote:
> I'm seeing some strange behavior while trying to use EqReasoning
> (Relation.Binary.EqReasoning from the standard library) to build
> proofs of equality of records containing irrelevant fields, and I was
> wondering if someone has an idea of what could be going on.
> (Apologies for a slightly vague question, but I'm having trouble
> coming up with a small example of the behavior in question.)
>
> So, following EqReasoning, the general shape of these proofs is
>
>    Proof = begin x0 ≈⟨ e1 ⟩ x1 ≈⟨ e2 ⟩ x2 ... ≈⟨ en ⟩ xn ∎
>
> where the xi are terms of a common type, and the ei are proofs of
> equality ei : x(i-1) ≈ xi.  In my case, the xi are terms of a record
> type Foo containing an irrelevant field "bar", and ≈ is a certain
> equivalence relation on Foo (not defined as propositional equality).
>
> The strange behavior is that type-checking Proof yields various
> unsolved metas of type "bar".  If I rewrite Proof using explicit
> application of transitivity
>
>    Proof' = trans≈ {i = x0} {j = x1} {k = xn} e1 $
>                 trans≈ {i = x1} {j = x2} {k = xn} e2 $
>                 ...
>                 trans≈ {i = x(n-2)} {j = x(n-1)} {k = xn} e(n-1) $
>                 en
>
> then the unsolved metas go away.  On the other hand, if I try to
> remove some of the redundancy in Proof' (e.g., by leaving the j's or
> the k's implicit) then again there are unsolved metas of type "bar".
>
> Any ideas?
>
> thanks,
> Noam
> _______________________________________________
> 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/