Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

[Chun Tian (binghe)]

Hi Konrad,

thanks for pointing me to balanced_mapTheory, where I found some useful 
LIST_REL related theorems, but the "fromList" is not what I can use.

After another look into listTheory, I think my previous alist built by MAP2 can 
be also done by ZIP. So I'm going to use ZIP for now.

--Chun

Il 07/08/19 20:05, Konrad Slind ha scritto:
> See also examples/balanced_bst/balanced_mapTheory, which has a "fromList" 
> construct.
> That does have the requirement of having the domain type capable of being 
> ordered.
> 
> Konrad.
> 
> 
> On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe)  > wrote:
> 
> Hi,
> 
> I wonder what's the most natural/native way to express a finite_map or 
> alist, using a key list and a value list (assuming their lengths are the 
> same, and the key list is all distinct)?
> 
> My current idea is to use MAP2 to build an alist of type ``:('a # 'b) 
> list``:
> 
>         MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)
> 
> then (if needed), `alist_to_fmap` will lead me to a finite_map. But 
> shouldn't it be already provided by a definition in alistTheory (or 
> finite_mapTheory) that I just didn't find out?
> 
> --Chun
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

[Konrad Slind]

See also examples/balanced_bst/balanced_mapTheory, which has a "fromList"
construct.
That does have the requirement of having the domain type capable of being
ordered.

Konrad.


On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe) 
wrote:

> Hi,
>
> I wonder what's the most natural/native way to express a finite_map or
> alist, using a key list and a value list (assuming their lengths are the
> same, and the key list is all distinct)?
>
> My current idea is to use MAP2 to build an alist of type ``:('a # 'b)
> list``:
>
> MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)
>
> then (if needed), `alist_to_fmap` will lead me to a finite_map. But
> shouldn't it be already provided by a definition in alistTheory (or
> finite_mapTheory) that I just didn't find out?
>
> --Chun
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] How to express a finite_map or alist using a key list and a value list?

[Chun Tian (binghe)]

Hi,

I wonder what's the most natural/native way to express a finite_map or alist, 
using a key list and a value list (assuming their lengths are the same, and the 
key list is all distinct)?

My current idea is to use MAP2 to build an alist of type ``:('a # 'b) list``:

MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)

then (if needed), `alist_to_fmap` will lead me to a finite_map. But shouldn't 
it be already provided by a definition in alistTheory (or finite_mapTheory) 
that I just didn't find out?

--Chun



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info