Re: [Hol-info] Extension of Co-algebraic Datatype

2018-07-11 Thread Chun Tian (binghe)
Hi Waqar,

I think you’re looking for a datatype package in which induction and 
coinduction types can be mixed naturally. This is currently not possible in 
HOL4, but it’s not the fault of Higher Order Logic itself. According to Andrei 
Popescu et al. [1] it’s in theory possible to port or (re)implement their BNF 
work in HOL4 as it doesn’t depend on Isabelle's type extensions to Higher Order 
Logic. However this is a huge work, nobody is doing this porting, as far as I 
know, although it is supposed to be a huge contribution once it’s done.

—Chun

[1] Traytel, D., Popescu, A.: Foundational, compositional (co) datatypes for 
higher-order logic: Category theory applied to theorem proving. 2012 27th 
Annual IEEE Symposium on Logic in Computer Science. 596–605 (2012).

> Il giorno 03 lug 2018, alle ore 17:09, Waqar Ahmad via hol-info 
>  ha scritto:
> 
> Hi,
> 
> In Isabelle, besides coinduction, the normal induction procedure on 
> lazylist/stream datatype appears to be allowed.. Can a same behaviour is 
> possible with the 'a llist type in HOL4.
> 
> Secondly, unlike lazy list, the "stream" are defined without having the empty 
> "LNIL". I see a similar formalization in  HOL example directory 
> "...examples/Crypto/TEA/lazy_teaScript.sml"
> 
> 
> val RoundFun_def =
>  Define
>`RoundFun (s: state) = SOME (Round s, FST (Round s))`;
> 
> val StreamG_def = new_specification
>  ("StreamG",
>   ["StreamG"],
>   ISPEC ``RoundFun`` llist_Axiom_1);
> 
> I defined it using LUNFOLD as
> 
> StreamD xs = LUNFOLD (λn. SOME (THE (LTL n),THE (LHD n))) x
> 
> Is it possible, that when an induction scheme is applied, the base case 
> (LNIL) can be discharged/skipped? I'm aware of llist_bisumulation, which is 
> extremely useful in proving that two lazy lists are equal. However, in many 
> cases, its not applicable
> 
> 
> 
> On Sun, May 13, 2018 at 6:19 AM  <mailto:michael.norr...@data61.csiro.au>> wrote:
> If you want the coinductively defined streams predicate over lllist, you can 
> write
> 
> 
> 
> >  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> > s)`;
> 
> <>
> 
> <>
> 
> val it =
> 
>(⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
> 
> ⊢ ∀A streams'.
> 
>   (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
> 
>   ∀a0. streams' a0 ⇒ streams A a0,
> 
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
> 
> 
> 
> I think the last theorem of the triple is the cases theorem you want.
> 
> 
> 
> Note that if you are going to define Stream with
> 
> 
> 
>   Stream L = LFILTER (\n. T) L
> 
> 
> 
> You might as well write the equivalent
> 
> 
> 
>   Stream L = L
> 
> 
> 
> Best wishes,
> 
> Michael
> 
> 
> 
> 
> 
> 
> 
> From: Waqar Ahmad <12phdwah...@seecs.edu.pk <mailto:12phdwah...@seecs.edu.pk>>
> Date: Saturday, 12 May 2018 at 05:45
> To: "Norrish, Michael (Data61, Acton)"  <mailto:michael.norr...@data61.csiro.au>>
> Cc: hol-info  <mailto:hol-info@lists.sourceforge.net>>
> Subject: Re: [Hol-info] Extension of Co-algebraic Datatype
> 
> 
> 
> Thanks!. I understand that the working of LNIL and LCONS constructors since 
> I'm exploring "llistTheory" for quite some time. To be very clear, I'm in the 
> process of porting "stream theory" form Isabelle  
> <>https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html 
> <https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html> 
> which is formalized as coinductive "stream":
> 
> 
> 
> codatatype (sset: 'a) stream =
> 
>   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
> 
> for
> 
>   map: smap
> 
>   rel: stream_all2
> 
> 
> 
>  I can see that its datatype is very similar to lazy list (llistTheory) 
> datatype so rather defining a new type I defined a function that returns the 
> same 'a llist-typed (lazy) list as given to its input:
> 
> 
> 
> ∀​​L. Stream L = LFILTER (λ​​n. T) L:
> 
> 
> 
> type_of ``stream``;
> 
> 
> 
>  ``:α​​ llist -> α​​ llist``:
> 
> 
> 
> 
> 
> Later in Isabelle "stream theory", a coinductive set "streams" is defined 
> based on "stream" datatype as:
> 
> 
> 
> coinductive_set
> 
>   streams :: "'a set ⇒​​  'a stream set"
> 
>   for A :: "'a set"
> 
> where
> 
>   Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-07-11 Thread Waqar Ahmad via hol-info
Hi,

In Isabelle, besides coinduction, the normal induction procedure on
lazylist/stream datatype appears to be allowed.. Can a same behaviour is
possible with the 'a llist type in HOL4.

Secondly, unlike lazy list, the "stream" are defined without having the
empty "LNIL". I see a similar formalization in  HOL example directory
"...examples/Crypto/TEA/lazy_teaScript.sml"


val RoundFun_def =
 Define
   `RoundFun (s: state) = SOME (Round s, FST (Round s))`;

val StreamG_def = new_specification
 ("StreamG",
  ["StreamG"],
  ISPEC ``RoundFun`` llist_Axiom_1);

I defined it using LUNFOLD as

StreamD xs = LUNFOLD (λn. SOME (THE (LTL n),THE (LHD n))) x

Is it possible, that when an induction scheme is applied, the base case
(LNIL) can be discharged/skipped? I'm aware of llist_bisumulation, which is
extremely useful in proving that two lazy lists are equal. However, in many
cases, its not applicable



On Sun, May 13, 2018 at 6:19 AM  wrote:

> If you want the coinductively defined streams predicate over lllist, you
> can write
>
>
>
> >  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A
> (LCONS a s)`;
>
> <>
>
> <>
>
> val it =
>
>(⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
>
> ⊢ ∀A streams'.
>
>   (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
>
>   ∀a0. streams' a0 ⇒ streams A a0,
>
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
>
>
>
> I think the last theorem of the triple is the cases theorem you want.
>
>
>
> Note that if you are going to define Stream with
>
>
>
>   Stream L = LFILTER (\n. T) L
>
>
>
> You might as well write the equivalent
>
>
>
>   Stream L = L
>
>
>
> Best wishes,
>
> Michael
>
>
>
>
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Saturday, 12 May 2018 at 05:45
> *To: *"Norrish, Michael (Data61, Acton)" 
> *Cc: *hol-info 
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks!. I understand that the working of LNIL and LCONS constructors
> since I'm exploring "llistTheory" for quite some time. To be very clear,
> I'm in the process of porting "stream theory" form Isabelle
> https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
> is formalized as coinductive "stream":
>
>
>
> codatatype (sset: 'a) stream =
>
>   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
>
> for
>
>   map: smap
>
>   rel: stream_all2
>
>
>
>  I can see that its datatype is very similar to lazy list (llistTheory)
> datatype so rather defining a new type I defined a function that returns
> the same 'a llist-typed (lazy) list as given to its input:
>
>
>
> *∀**​*​L. Stream L = LFILTER (*λ​*​n. T) L:
>
>
>
> type_of ``stream``;
>
>
>
>  ``:*α​*​ llist -> *α​*​ llist``:
>
>
>
>
>
> Later in Isabelle "stream theory", a coinductive set "streams" is defined
> based on "stream" datatype as:
>
>
>
> coinductive_set
>
>   streams :: "'a set *⇒**​​ * 'a stream set"
>
>   for A :: "'a set"
>
> where
>
>   Stream[intro!, simp, no_atp]: "[[a *∈**​*​ A; s *∈**​*​ streams A]] ⟹ a
> ## s *∈**​*​ streams A"
>
> end
>
>
>
> Using llistTheory functions, I'm able to define a similar function as:
>
>
>
> *∀**​*​A. streams A = IMAGE (*λ​*​a. Stream a) {llist_abs (*λ​*​n. SOME
> x) | x *∈**​*​ A}:
>
>
>
> type_of ``streams``;
>
>
>
>  ``:('a -> bool) -> 'a llist -> bool``:
>
>
>
> However, by using shallow embedding approach, I'm not able to use some
> essential properties that are accompanied when a new coinductive datatype
> is defined. For instance, if a streams datatype is define, I may have this
> property of form:
>
>
>
> streams.cases (Isabelle):
>
>
>
> a *∈**​*​ streams A *⇒**​*​ (? a s. a = a ##s *⇒**​​ a **∈**​​ A **⇒*
> *​​ s **∈**​​  *streams A *⇒**​*​ P) *⇒**​*​ P
>
>
>
> I'm having the issues of defining these types in HOL4. Is there any way
> that I can replicate the same in HOL4?
>
>
>
>
>
> On Mon, May 7, 2018 at 8:49 PM,  wrote:
>
> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist.   (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stre

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-15 Thread Michael.Norrish
There is no documentation I’m afraid, except that the interface and behaviour 
is basically exactly the same as for IndDefLib, which is described in the 
DESCRIPTION manual.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 16 May 2018 at 06:11
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Great!. This is exactly what I want. Thanks for helping me out...:) I located 
the file  "CoIndDefLib" in the HOL folder "src/IndDef".. Is there any 
documentation available regarding this file?

On Sun, May 13, 2018 at 6:04 AM, 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael



From: Waqar Ahmad <12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Saturday, 12 May 2018 at 05:45

To: "Norrish, Michael (Data61, Acton)" 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>
Cc: hol-info 
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀​​L. Stream L = LFILTER (λ​​n. T) L:

type_of ``stream``;

 ``:α​​ llist -> α​​ llist``:


Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒​​  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a ## s ∈​​ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀​​A. streams A = IMAGE (λ​​a. Stream a) {llist_abs (λ​​n. SOME x) | x ∈​​ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈​​ streams A ⇒​​ (? a s. a = a ##s ⇒​​ a ∈​​ A ⇒​​ s ∈​​  streams A ⇒​​ P) 
⇒​​ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?


On Mon, May 7, 2018 at 8:49 PM, 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>
Cc: hol-info 
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation.

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-15 Thread Waqar Ahmad via hol-info
Great!. This is exactly what I want. Thanks for helping me out...:) I
located the file  "CoIndDefLib" in the HOL folder "src/IndDef".. Is there
any documentation available regarding this file?

On Sun, May 13, 2018 at 6:04 AM, <michael.norr...@data61.csiro.au> wrote:

> If you want the coinductively defined streams predicate over lllist, you
> can write
>
>
>
> >  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A
> (LCONS a s)`;
>
> <>
>
> <>
>
> val it =
>
>(⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
>
> ⊢ ∀A streams'.
>
>   (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
>
>   ∀a0. streams' a0 ⇒ streams A a0,
>
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
>
>
>
> I think the last theorem of the triple is the cases theorem you want.
>
>
>
> Note that if you are going to define Stream with
>
>
>
>   Stream L = LFILTER (\n. T) L
>
>
>
> You might as well write the equivalent
>
>
>
>   Stream L = L
>
>
>
> Best wishes,
>
> Michael
>
>
>
>
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Saturday, 12 May 2018 at 05:45
>
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks!. I understand that the working of LNIL and LCONS constructors
> since I'm exploring "llistTheory" for quite some time. To be very clear,
> I'm in the process of porting "stream theory" form Isabelle
> https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
> is formalized as coinductive "stream":
>
>
>
> codatatype (sset: 'a) stream =
>
>   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
>
> for
>
>   map: smap
>
>   rel: stream_all2
>
>
>
>  I can see that its datatype is very similar to lazy list (llistTheory)
> datatype so rather defining a new type I defined a function that returns
> the same 'a llist-typed (lazy) list as given to its input:
>
>
>
> *∀**​*​L. Stream L = LFILTER (*λ​*​n. T) L:
>
>
>
> type_of ``stream``;
>
>
>
>  ``:*α​*​ llist -> *α​*​ llist``:
>
>
>
>
>
> Later in Isabelle "stream theory", a coinductive set "streams" is defined
> based on "stream" datatype as:
>
>
>
> coinductive_set
>
>   streams :: "'a set *⇒**​​ * 'a stream set"
>
>   for A :: "'a set"
>
> where
>
>   Stream[intro!, simp, no_atp]: "[[a *∈**​*​ A; s *∈**​*​ streams A]] ⟹ a
> ## s *∈**​*​ streams A"
>
> end
>
>
>
> Using llistTheory functions, I'm able to define a similar function as:
>
>
>
> *∀**​*​A. streams A = IMAGE (*λ​*​a. Stream a) {llist_abs (*λ​*​n. SOME
> x) | x *∈**​*​ A}:
>
>
>
> type_of ``streams``;
>
>
>
>  ``:('a -> bool) -> 'a llist -> bool``:
>
>
>
> However, by using shallow embedding approach, I'm not able to use some
> essential properties that are accompanied when a new coinductive datatype
> is defined. For instance, if a streams datatype is define, I may have this
> property of form:
>
>
>
> streams.cases (Isabelle):
>
>
>
> a *∈**​*​ streams A *⇒**​*​ (? a s. a = a ##s *⇒**​​ a **∈**​​ A **⇒*
> *​​ s **∈**​​  *streams A *⇒**​*​ P) *⇒**​*​ P
>
>
>
> I'm having the issues of defining these types in HOL4. Is there any way
> that I can replicate the same in HOL4?
>
>
>
>
>
> On Mon, May 7, 2018 at 8:49 PM, <michael.norr...@data61.csiro.au> wrote:
>
> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist.   (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stream type, does this mean you want a constructor
> for stream of type
>
>
>
>   (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *&q

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-13 Thread Michael.Norrish
If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael



From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 12 May 2018 at 05:45
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀​​L. Stream L = LFILTER (λ​​n. T) L:

type_of ``stream``;

 ``:α​​ llist -> α​​ llist``:


Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒​​  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a ## s ∈​​ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀​​A. streams A = IMAGE (λ​​a. Stream a) {llist_abs (λ​​n. SOME x) | x ∈​​ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈​​ streams A ⇒​​ (? a s. a = a ##s ⇒​​ a ∈​​ A ⇒​​ s ∈​​  streams A ⇒​​ P) 
⇒​​ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?


On Mon, May 7, 2018 at 8:49 PM, 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>
Cc: hol-info 
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a 
constructor of type

(α -> bool) -> α​​ llist



On Sun, May 6, 2018 at 8:39 PM, 
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In particular, write down the type of the “general” destructor

  myType -> F(myType)

For lazy lists, this is

  α llist -> (α # α llist) option

For the co-algebraic numbers it’s

  num -> num option

For arbitrarily (but finite)-branching trees, it’s

  Tree -> Tree list

(If you change list to llist you get possibly infinitely branching trees.)

In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s 
“predecessor”; in the trees it’s “children”.  Because the types are 
co-algebraic each might be iterable an infinite number of times.  (The 
corresponding destructors in

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-11 Thread Waqar Ahmad via hol-info
 Thanks!. I understand that the working of LNIL and LCONS constructors
since I'm exploring "llistTheory" for quite some time. To be very clear,
I'm in the process of porting "stream theory" form Isabelle
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory)
datatype so rather defining a new type I defined a function that returns
the same 'a llist-typed (lazy) list as given to its input:

∀​​L. Stream L = LFILTER (λ​​n. T) L:

type_of ``stream``;

 ``:α​​ llist -> α​​ llist``:


Later in Isabelle "stream theory", a coinductive set "streams" is defined
based on "stream" datatype as:

coinductive_set
  streams :: "'a set *⇒​​ * 'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a ## s
∈​​ streams
A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀​​A. streams A = IMAGE (λ​​a. Stream a) {llist_abs (λ​​n. SOME x) | x ∈​​
A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some
essential properties that are accompanied when a new coinductive datatype
is defined. For instance, if a streams datatype is define, I may have this
property of form:

streams.cases (Isabelle):

a ∈​​ streams A ⇒​​ (? a s. a = a ##s ⇒​*​ a *∈​*​ A *⇒​​* s *∈​​  streams A
 ⇒​​ P) ⇒​​ P

I'm having the issues of defining these types in HOL4. Is there any way
that I can replicate the same in HOL4?


On Mon, May 7, 2018 at 8:49 PM, <michael.norr...@data61.csiro.au> wrote:

> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist.   (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stream type, does this mean you want a constructor
> for stream of type
>
>
>
>   (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α​*​*​*​ -> bool) -> *α​*​ llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM, <michael.norr...@data61.csiro.au> wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
>   myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
>   α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
>   num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
>   Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”.  Because the types are
> co-algebraic each might be iterable an infinite number of times.  (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types?  I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 Ma

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-06 Thread Waqar Ahmad via hol-info
Thanks for the explanation. Let me state it clearly. Can I write down a
constructor of type

(α -> bool) -> α​​ llist



On Sun, May 6, 2018 at 8:39 PM,  wrote:

> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
>   myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
>   α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
>   num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
>   Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”.  Because the types are
> co-algebraic each might be iterable an infinite number of times.  (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types?  I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info 
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info 
> *Cc: *Waqar Ahmad 
> *Subject: *[Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Hi,
>
>
>
> Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
> is developed based on the co-algebraic datatype. I understand that the
> datatype *'a llist  *is derived as a subset of  the option type *:num ->
> 'a option. * Now, I want to define a new datatype based on datatype 'a
> llist. For instance,
>
>
>
> P of  'a llist
>
>
>
> such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially
> the similar datatype as *'a llist*  but having different properties. In
> shallow embedding, I can define it by using filter function of llistTheory
> as:
>
>
>
>
>
> val Stream = Define `Stream L =  LFILTER (\n:'a. T) L`;
>
>
>
> One way of defining the co-inductive datatype *stream* is to follow the
> same procedure as described in "llistTheory", which is quite cumbersome. Is
> there any alternate way similar to that of package "Hol_datatype"?
>
>
>
> Secondly, Is it possible to define a co-inductive datatype that takes a
> set type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
> similar function, in shallow embedding, I can think of is:
>
>
>
> val streams_def = Define
>
> `streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
>
>
>
> where the function streams is of type (:num -> 'a option) ->bool -> 'a
> llist-> bool
>
>
>
> In some cases, the function *streams* doesn't suffice for modeling the
> correct behavior of streams related properties..
>
>
>
> Any suggestion or thoughts would be highly helpful...
>
>
>
>
>
>
>
>
>
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
> [image:
> http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>


-- 
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-06 Thread Michael.Norrish
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In particular, write down the type of the “general” destructor

  myType -> F(myType)

For lazy lists, this is

  α llist -> (α # α llist) option

For the co-algebraic numbers it’s

  num -> num option

For arbitrarily (but finite)-branching trees, it’s

  Tree -> Tree list

(If you change list to llist you get possibly infinitely branching trees.)

In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s 
“predecessor”; in the trees it’s “children”.  Because the types are 
co-algebraic each might be iterable an infinite number of times.  (The 
corresponding destructors in the algebraic types are always well-founded.)

What are the co-algebras for your desired types?  I don’t think I’ve understood 
what you want, but it superficially appears as if you want dependent types, 
where you combine the type with some term-level predicate. That sort of thing 
is impossible to capture within a HOL type.

Finally, I’m afraid that there is no general tool for defining co-algebraic 
types in HOL4 at the moment.

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info 
Cc: Waqar Ahmad 
Subject: [Hol-info] Extension of Co-algebraic Datatype

Hi,

Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which is 
developed based on the co-algebraic datatype. I understand that the datatype 'a 
llist  is derived as a subset of  the option type :num -> 'a option.  Now, I 
want to define a new datatype based on datatype 'a llist. For instance,

P of  'a llist

such that P: 'a llist -> 'a stream, where 'a stream is essentially the similar 
datatype as 'a llist  but having different properties. In shallow embedding, I 
can define it by using filter function of llistTheory as:


val Stream = Define `Stream L =  LFILTER (\n:'a. T) L`;

One way of defining the co-inductive datatype stream is to follow the same 
procedure as described in "llistTheory", which is quite cumbersome. Is there 
any alternate way similar to that of package "Hol_datatype"?

Secondly, Is it possible to define a co-inductive datatype that takes a set 
type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A similar 
function, in shallow embedding, I can think of is:

val streams_def = Define
`streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;

where the function streams is of type (:num -> 'a option) ->bool -> 'a llist-> 
bool

In some cases, the function streams doesn't suffice for modeling the correct 
behavior of streams related properties..

Any suggestion or thoughts would be highly helpful...






--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info