[Agda] again `with' vs `case'
Sergei Meshveliani
mechvel at botik.ru
Mon Aug 26 20:35:35 CEST 2013
People,
there is again a strange point about `case' :
a proof cong2-∈ for the congruence of Membership._∈_ by the list
argument
(for lib-0.7, Agda of darcs August 2013).
--------------------------------------------------------------------------
open import Level using (Level)
open import Function using (case_of_)
open import Relation.Binary using (Setoid; module Setoid)
open import Data.List using (List; []; _∷_)
open import Data.List.Any using (Any; module Any; module Membership)
open import Relation.Binary.List.Pointwise as ListPoint using ()
renaming (_∷_ to _∷p_)
cong2-∈ : ∀ {c l} {A : Setoid c l} →
let open Setoid A using (_≈_) renaming (Carrier to C)
_∈_ = Membership._∈_ A
_=l_ = Setoid._≈_ (ListPoint.setoid A)
in
(x : C) → (xs ys : List C) → xs =l ys → x ∈ xs → x ∈ ys
open Any
cong2-∈ {A = A} x (u ∷ _) (v ∷ _) (u=v ∷p =tail) (here x=u) =
here x=v
where
open Setoid A
x=v : x ≈ v
x=v = trans x=u u=v
cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) (there x∈xs) =
there (cong2-∈ x xs ys =tail x∈xs)
{- -------------
cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =
case x∈u-xs of \
{
(here x=u) → let x=v : x ≈ v
x=v = trans x=u u=v
in here x=v
; (there x∈xs) → there (cong2-∈ x xs ys =tail x∈xs)
}
where
open Setoid A
---------------------
-}
-----------------------------------------------------------------------------
* It is type-checked,
* the `case' variant repeats everything, and is not type-checked:
"Missing cases: cong2-∈ {_} {_} {_} _ ._ ._ ListPoint.[] _ "
If it rejects ListPoint.[] in the first variant, why does it need it
in the `case' variant?
Thanks,
------
Sergei
More information about the Agda
mailing list