[Agda] list head eq

[Bradley Hardy]

Sergei,

The reason Agda isn’t able to infer that they’re the same is that it can’t look under function calls for things like that, even when the function does something obvious like `map proj₁`. As far as Agda is concerned, an arbitrary function might be doing anything at all, so it isn’t reasonable to search for unification under the result.

You should be able to make the two unify by proving a lemma with a type like:

lem : forall x y ps -> head (map proj₁ ((x , y) ∷ ps)) ≡ x

and rewriting using the resulting equality. You might need to do something with `inspect` as well to be able to remember that that pattern `x ∷ _` actually came from `map proj₁ ps`.

I hope this helps,

Brad

> On 3 May 2016, at 11:48, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 
> Please, what is wrong here?
> (Agda 2.5.1, ghc-7.10.2)
> 
> --------------------------------------------------------------------
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> open import Data.Nat     using (ℕ)
> open import Data.List    using (List; []; _∷_; map)
> open import Data.Product using (_×_; proj₁; _,_)
> 
> postulate  g : (x y : ℕ) → x ≡ y → ℕ
> 
> f : List (ℕ × ℕ) → ℕ
> f ps  with  ps | map proj₁ ps
> 
> ... | ((x , _) ∷ ps') | .x ∷ _ =  g x x PE.refl	   -- .x  ?
> ... | _               | _      =  0
> 
> f2 : List (ℕ × ℕ) → ℕ
> f2 ps  with ps | map proj₁ ps
> 
> ... | ((x , _) ∷ ps') | y ∷ _ =  g x y x≡y
>                                    where
>                                    x≡y : x ≡ y
>                                    x≡y = PE.refl   -- ?? 
> ... | _               | _     =  0
> ------------------------------------------------------------------
> 
> 
> Why ".x"  is rejected in  f ?
> 
> If  (x , _) is the head of  ps  and  y  the head of (map proj₁ ps), 
> then  x  is identical to  y.  How to explain this to Agda  in terms of
> patterns, like above?
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda