[Agda] A puzzle with "with"
Josh Ko
joshs at mail2000.com.tw
Wed Jun 24 17:05:35 CEST 2009
Hi,
A=20trick=20explained=20in=20the=20following=20old=20thread=20should=20be=20=
helpful:
=20=20http://thread.gmane.org/gmane.comp.lang.agda/145
I=20filled=20in=20a=20clause=20and=20it=20seems=20to=20work=20fine.
=20=20sorted_insert=20:=20(x=20:=20A)=20->=20(xs=20:=20List=20A)=20->=20Sort=
ed=20xs=20->=20Sorted=20(insert=20x=20xs)
=20=20sorted_insert=20x=20[]=20_=20=3D=20sorted_cons=20x
=20=20sorted_insert=20x=20(y=20∷=20ys)=20prf=20with=20inspect=20(Order=
.comp=20o=20x=20y)
=20=20sorted_insert=20x=20(y=20∷=20ys)=20prf=20|=20t=20with-=A1=DD=20p=
=20with=20Order.comp=20o=20x=20y=20|=20q
=20=20sorted_insert=20x=20(y=20∷=20ys)=20prf=20|=20.(Order.comp=20o=20=
x=20y)=20with-=A1=DD=20refl=20|=20Lt=20|=20q=20=3D
=20=20=20=20sorted_cons2=20x=20y=20ys=20prf=20(biimply=20(Order.isLtComp=20o=
=20x=20y)=20fwd=20q)
=20=20sorted_insert=20x=20(y=20∷=20ys)=20prf=20|=20.(Order.comp=20o=20=
x=20y)=20with-=A1=DD=20refl=20|=20Eq=20|=20q=20=3D=20{!!}
=20=20sorted_insert=20x=20(y=20∷=20ys)=20prf=20|=20.(Order.comp=20o=20=
x=20y)=20with-=A1=DD=20refl=20|=20Gt=20|=20q=20=3D=20{!!}
--=20JK
-----Original=20message-----
From:James=20McKinna=20<james.mckinna at cs.ru.nl>
To:agda=20<agda at lists.chalmers.se>
Date:Wed,=2024=20Jun=202009=2014:40:58=20+0200
Subject:[Agda]=20A=20puzzle=20with=20"with"=20
Dear=20Agda=20list,
We=20have=20a=20puzzle=20concerning=20the=20use,=20semantics,=20and=20implem=
entation=20of=20"with"=20in=20Agda.=20
Please=20find=20attached=20a=20source=20file=20with=20holes,=20which=20we=20=
cannot=20fill.=20We=20think=20the=20problem=20lies=20in=20the=20fact=20that=20=
in=20pattern=20matching=20clauses,=20the=20typechecker=20is=20either=20doing=
=20to=20much=20reduction,=20or=20else=20not=20enough,=20to=20make=20"obvious=
"=20conversions=20between=20types=20OK.=20
Context:
We=20(myself=20and=20Cezary=20Kaliszyk)=20are=20trying=20to=20prove=20some=20=
easy=20things=20about
insertion=20sorting.
We=20have=20the=20usual=20three-way=20comparison=20type=20and=20a=20record=20=
signature=20for=20sorting
which=20says=20that=20the=20things=20we=20wish=20to=20sort=20fit=20well=20wi=
th=20the=20comparison
function.
Now=20we=20write=20"insert"=20in=20the=20usual=20way=20...=20with=20a=20"wit=
h"=20on=20the
call=20to=20the=20comparison=20function.
We've=20tried=20this=20both=20with=20and=20without=20the=20use=20of=20"inspe=
ct".
In=20every=20case=20we=20get=20complaints=20from=20the=20type-checker,=20eit=
her
that=20it=20can't=20refine=20the=20type,=20or=20that=20a=20feature=20is=20no=
t=20implemented
yet,=20or=20that=20pattern-matching=20instantiates=20the=20wrong=20part=20of=
=20the=20type.
In=20the=20attached=20file,
=20in=20sorted_insert,=20at=20hole=20{=20}0=20we=20need=20a=20term=20of=20ty=
pe
=20=20=20=20Sorted(x::y::ys),=20in=20order=20to=20construct=20one=20we=20nee=
d
=20=20=20=20the=20result=20of=20"comp"=20(in=20order=20to=20apply=20sorted_c=
ons2)
=20=20=20=20but=20without=20"inspect"=20we=20do=20not=20have=20it.
=20in=20sorted_insert2,=20at=20hole=20{=20}3=20we=20used=20inspect,=20but
=20=20=20=20instead,=20the=20type=20fails=20to=20reduce=20to=20Sorted(x::y::=
ys).
=20in=20sorted_insert3=20we=20tried=20to=20combine=20the=20two=20"with"s,
=20=20=20=20but=20the=20expected=20type=20and=20the=20type=20of=20"p"=20are
=20=20=20=20mismatched=20up=20to=20the=20equality=20p.=20Pattern-matching
=20=20=20=20has=20instantiated=20the=20type=20on=20the=20lhs=20but=20not=20o=
n=20the=20rhs.
=20in=20sorted_insert4=20if=20we=20try=20to=20use=20"subst"=20on=20the=20mis=
sing
=20=20=20=20equation,=20we=20get
=20=20=20=20"Not=20implemented:=20type=20checking=20of=20with=20application"=
.
So,=20we=20are=20now=20very=20confused=20about=20the=20implementation=20and
semantics=20of=20"with"=20in=20Agda.=20Can=20you=20please=20explain
how=20one=20might=20solve=20such=20a=20problem=20and=20learn=20how=20to=20av=
oid=20it=20in=20the=20future.
Regards,
Cezary=20and=20James.
module=20ulf=20where=20
open=20import=20Data.List
open=20import=20Data.Bool
open=20import=20Relation.Binary.PropositionalEquality
data=20Compare=20:=20Set=20where
=20=20Lt=20:=20Compare
=20=20Eq=20:=20Compare
=20=20Gt=20:=20Compare
infixl=2071=20_<->_
data=20_<->_=20(A=20B=20:=20Set)=20:=20Set=20where
=20=20biimply=20:=20(A=20->=20B)=20->=20(B=20->=20A)=20->=20(A=20<->=20B)
biimply_fwd=20:=20{A=20B=20:=20Set}=20->=20(A=20<->=20B)=20->=20(A=20->=20B)=
biimply_fwd=20(biimply=20f=20_)=20=3D=20f
record=20Order=20:=20Set1=20where
=20=20field
=20=20=20=20A=20:=20Set
=20=20=20=20Comp=20:=20A=20->=20A=20->=20Set
=20=20=20=20comp=20:=20A=20->=20A=20->=20Compare
=20=20=20=20isLtComp=20:=20(a=20b=20:=20A)=20->=20(comp=20a=20b=20�&#=
65533;=20Lt)=20<->=20Comp=20a=20b
=20=20=20=20isEqComp=20:=20(a=20b=20:=20A)=20->=20(comp=20a=20b=20�&#=
65533;=20Eq)=20<->=20(a=20��=20b)
=20=20=20=20isGtComp=20:=20(a=20b=20:=20A)=20->=20(comp=20b=20a=20�&#=
65533;=20Gt)=20<->=20Comp=20a=20b
=20=20=20=20isTrans=20:=20{a=20b=20c=20:=20A}=20->=20Comp=20a=20b=20->=20Com=
p=20b=20c=20->=20Comp=20a=20c
module=20Sort=20(o=20:=20Order)=20where
=20=20A=20=3D=20Order.A=20o
=20=20insert=20:=20A=20->=20List=20A=20->=20List=20A
=20=20insert=20x=20[]=20=3D=20x=20��=20[]
=20=20insert=20x=20(y=20��=20ys)=20with=20(Order.comp=20o=20x=20=
y)
=20=20...=20=20=20=20=20=20=20=20=20=20=20=20=20=20|=20Lt=20=3D=20x=20ᦙ=
3;�=20(y=20��=20ys)
=20=20...=20=20=20=20=20=20=20=20=20=20=20=20=20=20|=20Eq=20=3D=20y=20ᦙ=
3;�=20(insert=20x=20ys)
=20=20...=20=20=20=20=20=20=20=20=20=20=20=20=20=20|=20Gt=20=3D=20y=20ᦙ=
3;�=20(insert=20x=20ys)
=20=20sort=20:=20List=20A=20->=20List=20A
=20=20sort=20[]=20=20=20=20=20=20=20=20=3D=20[]
=20=20sort=20(x=20��=20xs)=20=3D=20insert=20x=20(sort=20xs)
=20=20data=20Sorted=20:=20List=20A=20->=20Set=20where
=20=20=20=20sorted_nil=20:=20Sorted=20[]
=20=20=20=20sorted_cons=20:=20(x=20:=20A)=20->=20Sorted=20(x=20�ʏ=
33;=20[])
=20=20=20=20sorted_cons2=20:=20(x=20y=20:=20A)=20->=20(ys=20:=20List=20A)=20=
->=20Sorted=20(y=20��=20ys)=20->=20(Order.Comp=20o=20x=20y)=20=
->=20Sorted=20(x=20��=20(y=20��=20ys))
=20=20insert_lt=20:=20(x=20y=20:=20A)=20->=20(ys=20:=20List=20A)=20->=20Sort=
ed=20(y=20��=20ys)=20->=20(Order.comp=20o=20x=20y=20�&#=
65533;=20Lt)=20->=20Sorted=20(x=20��=20(y=20��=20=
ys))
=20=20insert_lt=20x=20y=20ys=20yysp=20xyp=20=3D=20sorted=20x=20cons2=20y=20y=
s=20yysp=20(biimply_fwd=20(Order.isLtComp=20o=20x=20y)=20xyp)
=20=20sorted_insert=20:=20(x=20:=20A)=20->=20(xs=20:=20List=20A)=20->=20Sort=
ed=20xs=20->=20Sorted=20(insert=20x=20xs)
=20=20sorted_insert=20x=20[]=20_=20=3D=20sorted_cons=20x
=20=20sorted_insert=20x=20(y=20��=20ys)=20prf=20with=20Order.c=
omp=20o=20x=20y
=20=20sorted_insert=20x=20(y=20��=20ys)=20prf=20|=20Lt=20=3D=20=
{!=20=20!}
=20=20sorted_insert=20x=20(y=20��=20ys)=20prf=20|=20Eq=20=3D=20=
{!=20!}
=20=20sorted_insert=20x=20(y=20��=20ys)=20prf=20|=20Gt=20=3D=20=
{!=20!}
=20=20sorted_insert2=20:=20(x=20:=20A)=20->=20(xs=20:=20List=20A)=20->=20Sor=
ted=20xs=20->=20Sorted=20(insert=20x=20xs)
=20=20sorted_insert2=20x=20[]=20_=20=3D=20sorted_cons=20x
=20=20sorted_insert2=20x=20(y=20��=20ys)=20prf=20with=20inspec=
t=20(Order.comp=20o=20x=20y)
=20=20sorted_insert2=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert2=20x=20(y=20��=20ys)=20prf=20|=20Eq=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert2=20x=20(y=20��=20ys)=20prf=20|=20Gt=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert3=20:=20(x=20:=20A)=20->=20(xs=20:=20List=20A)=20->=20Sor=
ted=20xs=20->=20Sorted=20(insert=20x=20xs)
=20=20sorted_insert3=20x=20[]=20_=20=3D=20sorted_cons=20x
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20with=20inspec=
t=20(Order.comp=20o=20x=20y)
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20with=20Order.comp=20o=20x=20y
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20|=20Lt=20=3D=20insert_lt=20x=20y=20ys=20prf=20{!=20p=
!}
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20|=20Eq=20=3D=20{!=20!}
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20|=20Gt=20=3D=20{!=20!}
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Eq=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert3=20x=20(y=20��=20ys)=20prf=20|=20Gt=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert4=20:=20(x=20:=20A)=20->=20(xs=20:=20List=20A)=20->=20Sor=
ted=20xs=20->=20Sorted=20(insert=20x=20xs)
=20=20sorted_insert4=20x=20[]=20_=20=3D=20sorted_cons=20x
=20=20sorted_insert4=20x=20(y=20��=20ys)=20prf=20with=20inspec=
t=20(Order.comp=20o=20x=20y)
=20=20sorted_insert4=20x=20(y=20��=20ys)=20prf=20|=20Lt=20with=
-��=20p=20=3D=20{!=20subst=20(Sorted=20(insert=20x=20(y=20A=
533;�=20ys)=20|=20Lt))=20(Sorted=20(insert=20x=20(y=20��=
;=20ys)=20|=20Order.comp=20o=20x=20y))=20(sym=20p)=20?=20!}
=20=20sorted_insert4=20x=20(y=20��=20ys)=20prf=20|=20Eq=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_insert4=20x=20(y=20��=20ys)=20prf=20|=20Gt=20with=
-��=20p=20=3D=20{!=20!}
=20=20sorted_sort=20:=20(x=20:=20List=20A)=20->=20Sorted=20(sort=20x)
=20=20sorted_sort=20[]=20=3D=20sorted_nil
=20=20sorted_sort=20(x=20��=20[])=20=3D=20sorted_cons=20x
=20=20sorted_sort=20(x=20��=20(y=20��=20ys))=20w=
ith=20(sorted_sort=20(y=20��=20ys))
=20=20sorted_sort=20(x=20��=20(y=20��=20[]))=20|=
=20sorted_cons=20.y=20=3D=20sorted_insert=20x=20(y=20��=20[])=20=
sorted=20y=20cons
=20=20sorted_sort=20(x=20��=20(y=20��=20(z=20=
5533;�=20zs)))=20|=20w=20=3D=20sorted_insert=20x=20(insert=20y=20(ins=
ert=20z=20(sort=20zs)))=20w
_______________________________________________
Agda=20mailing=20list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list