[Agda] with - refl strangeness

[Andreas Abel]

There is nothing strange, Agda just behaves as it should.  You need to 
match on the list in the proof of reflexivity, since you also match on 
in the definition of equality.

This checks:

record Foo : Set where
   constructor foo
   field  list : List ℕ

_=fo_ : Rel Foo 0L
s =fo s'  with  Foo.list s

... | []     =  []       =l Foo.list s'  -- (I)
... | x ∷ xs =  (x ∷ xs) =l Foo.list s'

-- ... | xs =  xs =l Foo.list s'         -- (II)

-- _=fo_ =  _=l_ on Foo.list             -- (III)

foRefl : Reflexive _=fo_
foRefl {foo []}      = lRefl
foRefl {foo (x ∷ l)} = lRefl


On 02.06.13 8:12 PM, Sergei Meshveliani wrote:
> open import Level    using ()  renaming (zero to 0L)
> open import Function using (_$_;_on_)
> open import Relation.Binary using
>       (Rel; IsEquivalence; module IsEquivalence; Setoid; module Setoid;
>        DecSetoid; module DecSetoid; module DecTotalOrder; IsDecTotalOrder
>       )
> open import Relation.Binary.Core using
>                                   (Reflexive; Symmetric; Transitive)
> open import Data.Nat as Nat using (ℕ; _<_) renaming
>                                             (decTotalOrder to natDTO)
> open import Data.List as Ls using (List; []; _∷_)
> open import Relation.Binary.List.Pointwise as ListPoint using()
>                                           renaming (setoid to listSetoid)
>
>
> nDecSetoid = DecTotalOrder.Eq.decSetoid natDTO
> nSetoid    = DecSetoid.setoid nDecSetoid
>
> lSetoid = listSetoid nSetoid            -- for  List ℕ
> lEquiv  = Setoid.isEquivalence lSetoid
> open Setoid lSetoid using () renaming (_≈_ to _=l_)
> open IsEquivalence lEquiv renaming
>                            (refl to lRefl; sym to lSym; trans to lTrans)
>
> record Foo : Set where
>                   field  list : List ℕ
>
> _=fo_ : Rel Foo 0L
> s =fo s'  with  Foo.list s
>
> ... | []     =  []       =l Foo.list s'  -- (I)
> ... | x ∷ xs =  (x ∷ xs) =l Foo.list s'
>
> -- ... | xs =  xs =l Foo.list s'         -- (II)
>
> -- _=fo_ =  _=l_ on Foo.list             -- (III)
>
> foRefl : Reflexive _=fo_
> foRefl = lRefl

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/