# [Agda] cancel-just-in≡

Sergei Meshveliani mechvel at botik.ru
Sat Dec 7 16:47:31 CET 2013

```Sorry, I find now the proof

cancel-just-in≡ {A} {x} {.x} PE.refl =  PE.refl

And again, a dotted pattern helps to prove  cong₁-gfilter  as well.

The only remaining question is of whether a proof of  cong₁-gfilter
below really needs recursion by the list construction.

On Sat, 2013-12-07 at 15:01 +0400, Sergei Meshveliani wrote:
> People,
> I am trying to prove the congruence of  Data.List.gfilter  by  _≗_
> and  _≡_.
>
> By the second argument  xs : List A,  it is proved simply by
> PE.cong (gfilter p)
>    where
>    open import Relation.Binary.PropositionalEquality as PE
>                                                      using (_≡_; _≗_)
>
> For the first argument, I have
>               xs : List A,   p p' : A -> Maybe B,  p≗p' : p ≗ p',
>
> and need to prove   gfilter p xs ≡ gfilter p' xs.
>
> PE.cong (\ p -> gfilter p xs) p≗p' PE.refl
>
> does not work here (need it?).
>
> Then, I try recursion by the list construction:
>
>   cong₁-gfilter (x ∷ xs) {p} {p'} p≗p' =  eq
>     where
>     ...
>
> And then, need to prove   just x ≡ just y → x ≡ y.
>
> I suspect that a dotted pattern must help, but fail.
> I write for testing:
>
>  cancel-just-in≡ : {A : Set} {x y : A} → let _≡A_ = _≡_ {A = A}
>                                              _≡m_ = _≡_ {A = Maybe A}
>                                          in
>                                          just x ≡m just y → x ≡A y
>
>  cancel-just-in≡ {A} {x} {y} jx=jy  with  just x | just y
>
>  ... | just x | .(just x) =  PE.refl
>
> The  development Agda of November 2013 (MAlonzo)
> reports
>
> Repeated variables in left hand side: x
> when scope checking the left-hand side
> cancel-just-in≡ {A} {x} {y} jx=jy in the definition of
> cancel-just-in≡
>
> 1) I do not see here any LHS variable repetition, because second  x  is
> after `with'.
> 2) How to prove  cancel-just-in≡ ?
> 3) How to prove  cong₁-gfilter ?
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

```

More information about the Agda mailing list