[Agda] irrelevant fields and EqReasoning

[Noam Zeilberger]

On Wed, Jul 18, 2012 at 11:27 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi Noam,
>
> I agree with your analysis.
>
> As I see it, you have already answered your question (from your second mail)
> in your first mail, which was:
>
>
> On 16.07.12 4:59 PM, Noam Zeilberger wrote:
>> 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".
>
> Here you write that if you omit repetitive hidden arguments, you get
> unsolved metas.  But EqReasoning does exactly this, omitting redundant args
> to trans.
>
>   _∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
>   _ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

In fact, it seems the problem is not the hidden arguments that _∼⟨_⟩_
passes to trans (rewriting the function to pass them explicitly
doesn't get rid of the unsolved metas), but the hidden arguments it
takes itself, in particular y.  Passing the y's explicitly to _≈⟨_⟩_
in my term "Proof" gets rid of the unsolved metas...but of course it
also gets rid of the point of using EqReasoning in the first place.

The real problem seems to be that Agda has no way of seeing that the y
may be synthesized from a term of type "y IsRelatedTo z" built out of
_∼⟨_⟩_'s and _∎'s (a quick inspection will convince you that this is
possible).  I played for a bit with making this connection explicit by
replacing the binary relation "y IsRelatedTo z" with a unary relation
"RelatedTo z" together with a function returning the domain:

dom : ∀ {z} -> RelatedTo z -> Carrier

Then for example the type of _∼⟨_⟩_ can be expressed very nicely as:

_∼⟨_⟩_ : ∀ x {z} → x ∼ dom r → (r : RelatedTo z) → RelatedTo z

...except that of course this type isn't well-formed, since the order
of dependency is not left-to-right!

Swapping the order of the arguments will typecheck...

_∼⟨_⟩_ : ∀ x {z} → (r : RelatedTo z) → x ∼ dom r → RelatedTo z

and does manage to get rid of the unsolved metas in my original
example, but now it destroys the nice linear flow of EqReasoning.
Note that switching to a left-associative interpretation does not
help, since the following type also fails to be well-formed (quite
unfairly, in my opinion):

_∼⟨_⟩_ : ∀ {x} → (r : x RelatedTo) → cod r ∼ z → (z : Carrier) → x RelatedTo

Time to liberate dependent types from the shackles of left-to-right scoping!

Noam