[Agda] rewrite vs. with

[David Leduc]

Thank you Jean-Philippe!

It works in this example because "proj1 t" appears explicitly in my
goal at the biginning and thus I can rewrite it. However in my
development (too big to be posted here), the term to be rewritten only
appear in the goal after I have filled it partly (i.e., I have
replaced the initial hole by a term with holes). That's when I'd like
to rewrite.

In Coq, I can do a rewrite at any time. What should/can I do in Agda?

On Tue, Sep 28, 2010 at 12:31 PM, Jean-Philippe Bernardy
<bernardy at chalmers.se> wrote:
> You should first abstract on the term (use 'with' on it) and then use
> with on the witness of equality.
> These two operations are conveniently packaged for you in the form of
> the 'rewrite' lhs:
>
> g A t B f b1 b2 rewrite eq t = ?
>
> Cheers,
> JP.
>
> On Tue, Sep 28, 2010 at 7:07 AM, David Leduc
> <david.leduc6 at googlemail.com> wrote:
>> Hi,
>>
>> Sorry, it's again a newbie question.
>> In the code below, I'd like to replace the hole in g with f b1 b2.
>> The problem is that f takes two arguments of the same type,
>> but the type of b1 and b2 are only provably equal (with Lemma eq).
>> In Coq I would use the tactic rewrite.
>> In Agda, I guess I should use a "with" but it does not work in this case.
>> I get the following error message:
>>
>>  Cannot pattern match on constructor refl, since the inferred
>>  indices [proj1 t'] cannot be unified with the expected indices
>>  [proj2 t'] for some t', A'
>>  when checking that the expression ? has type A
>>
>> What can I do?
>>
>> --------------------------------
>>
>> module test where
>>
>> open import Relation.Binary.PropositionalEquality
>>
>> data T (A : Set) : Set where
>>  makeT : (a1 a2 : A) -> a1 ≡ a2 -> T A
>>
>> proj1 : {A : Set} -> T A -> A
>> proj1 (makeT a _ _) = a
>>
>> proj2 : {A : Set} -> T A -> A
>> proj2 (makeT _ a _) = a
>>
>> eq : {A : Set}(t : T A) -> proj1 t ≡ proj2 t
>> eq (makeT _ _ p) = p
>>
>> g : (A : Set)(t : T A)(B : A -> Set)(f : B (proj1 t) -> B (proj1 t) -> A)
>>  (b1 : B (proj1 t))(b2 : B (proj2 t)) -> A
>> g A t B f b1 b2 with eq t
>> ...| p = {!!}
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>