[Agda] irrelevant fields and EqReasoning
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Jul 16 17:17:57 CEST 2012
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/
More information about the Agda
mailing list