Dear All,
Thankyou to Sir John Harrison for providing valuable help with the
Definition. Also thanks to Mr. Marks Adam for highlighting the type
difference.
I am having the following type checking issue with my goal in the Matrix
theory of HOL-Light. It seems that left hand side and right hand side dont
have similar types. I would appreciate if someone can please help me out
with the change in definition or change in writing the goal or any other
suggestion to get rid of this error.
let horz_conct1 = new_definition
`(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda
a b .
if (b<=dimindex(:N))
then (A$a$b) else (B$a$(b-(dimindex(:N))))`;;
Now if i want to prove that
g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B)
(C)= horz_conct1 (A) (horz_conct1 B C)`;;
The types for the left hand side and right hand side were:
`:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M)
`:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M)
it gives following error
Exception: Failure "typechecking error (initial type assignment)".
So the definition is accepted but the proof goal using the function gives
the problem.
Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
On Mon, Jul 4, 2016 at 5:28 AM, <hol-info-requ...@lists.sourceforge.net>
wrote:
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
>
>
> Today's Topics:
>
> 1. Re: A question about the definition of the function in HOL4
> (Ramana Kumar)
> 2. Matrix Definition Query (Abid Rauf)
> 3. Type checking issue (Abid Rauf)
> 4. Re: Matrix Definition Query (John Harrison)
> 5. Re: Type checking issue (Mark Adams)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Thu, 30 Jun 2016 23:17:10 +1000
> From: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> Subject: Re: [Hol-info] A question about the definition of the
> function in HOL4
> To: Ada <956066...@qq.com>
> Cc: hol-info <hol-info@lists.sourceforge.net>
> Message-ID:
> <CAMej=
> 26cfzgl+f9esjuxwe6sao5nttk6hrdjekco-uzfkfw...@mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Hi Ada,
>
> It still looks like you might be mixing up ML and HOL. Are you trying to
> define an ML function, or a HOL function?
>
> In ML, the conjunction of two Boolean expressions can be formed using the
> "andalso" operator.
> Now, maybe you already defined /\ like this, and gave it infix status:
>
> infix /\;
> fun op /\ (a, b) = a andalso b;
>
> Then I would expect your definition to work.
>
> But please note that this is a definition in ML. If you want to make a
> definition in HOL, use Define.
> For example:
>
> val ccdd_def = Define`ccdd a b c d = if ((a = b) /\ (c = d)) then T else
> F`;
>
> Cheers,
> Ramana
>
>
> On 30 June 2016 at 22:51, Ada <956066...@qq.com> wrote:
>
> > Hi,guys
> > I am working with HOL4.
> > I defined a function in HOL4,like following
> > - fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false;
> > It responded that:
> > ! Toplevel input:
> > ! fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false;
> > ! ^^^^^^^
> > ! Type clash: expression of type
> > ! bool
> > ! cannot have type
> > ! 'a -> 'b
> > I can't understand it.
> > Who know the reason?
> > Thanks!
> >
> >
> >
> ------------------------------------------------------------------------------
> > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> > Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> > present their vision of the future. This family event has something for
> > everyone, including kids. Get more information and register today.
> > http://sdm.link/attshape
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
> Message: 2
> Date: Fri, 1 Jul 2016 11:45:28 +0500
> From: Abid Rauf <abid.r...@seecs.edu.pk>
> Subject: [Hol-info] Matrix Definition Query
> To: hol-info@lists.sourceforge.net
> Message-ID:
> <
> camyoggwwzzss3-1wsutpmgjhsdpoadxvolmrfruyhxaw0cn...@mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear All,
>
> I have a Query about Matrices. Can i write a definition in HOL light which
> takes two matrices of dimensions real^N^M and real^Q^P and after a certain
> operation output a vector with dimension real^(N*Q)^(M*P).
> I was going through the theory and found finite_sum, which is the addition
> of dimensions, but here i need product or multiplication of dimensions. Can
> anyone help me out please.
>
> Best Regards,
> Abid Rauf
> Ph.D Scholar (CS) & RA SAVe Labs,
> School of Electrical Engineering and Computer Science (SEECS),
> National University of Science and Technology (NUST), H-12, Islamabad,
> Pakistan
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
> Message: 3
> Date: Sat, 2 Jul 2016 14:30:43 +0500
> From: Abid Rauf <abid.r...@seecs.edu.pk>
> Subject: [Hol-info] Type checking issue
> To: hol-info@lists.sourceforge.net
> Message-ID:
> <CAMYogGVCtZm0=
> i_dnt7tgcz_j7t8boyftcn381s4vue7klc...@mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear All,
>
> I am having the following type checking issue with a definition in the
> Matrix theory of HOL-Light. It seems the double application of the function
> leads to an unknown dimension of the matrix, which is causing the problem.
> I would appreciate if someone can please help me out with us.
>
> let horz_conct1 = new_definition
> `(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda
> a b .
> if (b<=dimindex(:N))
> then (A$a$b) else (B$a$(b-(dimindex(:N))))`;;
>
> Now if i want to prove that
>
> g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B)
> (C)= horz_conct1 (A) (horz_conct1 B C)`;;
>
> it gives following error
>
> Exception: Failure "typechecking error (initial type assignment)".
> So the definition is accepted but the proof goal using the function gives
> the problem.
>
>
> Best Regards,
> Abid Rauf
> Ph.D Scholar (CS) & RA SAVe Labs,
> School of Electrical Engineering and Computer Science (SEECS),
> National University of Science and Technology (NUST), H-12, Islamabad,
> Pakistan
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
> Message: 4
> Date: Sat, 02 Jul 2016 17:08:59 +0100
> From: John Harrison <john.harri...@cl.cam.ac.uk>
> Subject: Re: [Hol-info] Matrix Definition Query
> To: Abid Rauf <abid.r...@seecs.edu.pk>
> Cc: hol-info@lists.sourceforge.net
> Message-ID: <e1bjnty-0003jz...@mta0.cl.cam.ac.uk>
>
>
> Hi Abid,
>
> | I was going through the theory and found finite_sum, which is the
> addition
> | of dimensions, but here i need product or multiplication of dimensions.
> Can
> | anyone help me out please.
>
> I think the following should work --- I should probably add it to the
> system
> as it might be useful for others too.
>
> let finite_prod_tybij =
> let th = prove
> (`?x. x IN 1..(dimindex(:A) * dimindex(:B))`,
> EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL] THEN
> MESON_TAC[LE_1; DIMINDEX_GE_1; MULT_EQ_0]) in
> new_type_definition "finite_prod"
> ("mk_finite_prod","dest_finite_prod") th;;
>
> let FINITE_PROD_IMAGE = prove
> (`UNIV:(A,B)finite_prod->bool =
> IMAGE mk_finite_prod (1..(dimindex(:A)*dimindex(:B)))`,
> REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN
> MESON_TAC[finite_prod_tybij]);;
>
> let DIMINDEX_HAS_SIZE_FINITE_PROD = prove
> (`(UNIV:(M,N)finite_prod->bool) HAS_SIZE (dimindex(:M) * dimindex(:N))`,
> SIMP_TAC[FINITE_PROD_IMAGE] THEN
> MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
> ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1]
> THEN
> MESON_TAC[finite_prod_tybij]);;
>
> let DIMINDEX_FINITE_PROD = prove
> (`dimindex(:(M,N)finite_prod) = dimindex(:M) * dimindex(:N)`,
> GEN_REWRITE_TAC LAND_CONV [dimindex] THEN
> REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PROD]);;
>
> John.
>
>
>
> ------------------------------
>
> Message: 5
> Date: Mon, 04 Jul 2016 01:28:35 +0100
> From: Mark Adams <m...@proof-technologies.com>
> Subject: Re: [Hol-info] Type checking issue
> To: Abid Rauf <abid.r...@seecs.edu.pk>
> Cc: hol-info@lists.sourceforge.net
> Message-ID: <cde8a22147d81eb6fcab205d4031c...@webmail.names.co.uk>
> Content-Type: text/plain; charset="us-ascii"
>
> Hello Abid,
>
> The term quotation fails type checking simply because the types of LHS
> and RHS of the equality are different:
>
> `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M)
>
> `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M)
>
> As I understand it (I may be wrong here), there is no way of getting the
> HOL type system to let you express this associativity property about
> 'horz_conct1'. If you want to express these kinds of properties, I
> think you need to define your function in a different way, not using
> types like this.
>
> Mark.
>
> On 02/07/2016 10:30, Abid Rauf wrote:
>
> > Dear All,
> >
> > I am having the following type checking issue with a definition in the
> Matrix theory of HOL-Light. It seems the double application of the function
> leads to an unknown dimension of the matrix, which is causing the problem.
> I would appreciate if someone can please help me out with us.
> >
> > let horz_conct1 = new_definition
> > `(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda
> a b .
> > if (b<=dimindex(:N))
> > then (A$a$b) else (B$a$(b-(dimindex(:N))))`;;
> >
> > Now if i want to prove that
> >
> > g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B)
> (C)= horz_conct1 (A) (horz_conct1 B C)`;;
> >
> > it gives following error
> >
> > Exception: Failure "typechecking error (initial type assignment)".
> >
> > So the definition is accepted but the proof goal using the function
> gives the problem.
> >
> > Best Regards,
> >
> > Abid Rauf
> > Ph.D Scholar (CS) & RA SAVe Labs,
> > School of Electrical Engineering and Computer Science (SEECS),
> > National University of Science and Technology (NUST), H-12, Islamabad,
> Pakistan
> >
> ------------------------------------------------------------------------------
> > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> > Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> > present their vision of the future. This family event has something for
> > everyone, including kids. Get more information and register today.
> > http://sdm.link/attshape
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
>
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
>
> ------------------------------
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> End of hol-info Digest, Vol 122, Issue 1
> ****************************************
>
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
