[Agda] cancel-just-in≡

[Sergei Meshveliani]

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
>