Hi,Jeremy
Thank you for your reply!
I tried. But it can't work.
It responsed:
- e (RW_TAC list_ss [LENGRH_DROP]);
OK..
Exception raised at Tactical.VALID:
Invalid tactic
! Uncaught exception:
! HOL_ERR
I think the reason is that the format of "(cx l q p)" is not equal to "l",
though they are the same type "bool list".
Thank you!
------------------ Original ------------------
From: "hol-info-request";<[email protected]>;
Date: Mon, Feb 29, 2016 01:08 PM
To: "hol-info"<[email protected]>;
Subject: hol-info Digest, Vol 117, Issue 9
Send hol-info mailing list submissions to
[email protected]
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
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."
Today's Topics:
1. How to transform list format from "(cx l q p)" to "l" ( Ada )
2. Re: How to transform list format from "(cx l q p)" to "l"
(Jeremy Dawson)
3. Two postdoc positions - Reasoning about concurrency and
distribution - Imperial College London (Petar Maksimovic)
----------------------------------------------------------------------
Message: 1
Date: Sun, 28 Feb 2016 19:48:56 +0800
From: " Ada " <[email protected]>
Subject: [Hol-info] How to transform list format from "(cx l q p)" to
"l"
To: " hol-info " <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="gb18030"
Hey,guys
I am learning to use HOL4. Here are some questions about my proving:
g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) =
LENGTH p) `;
e (Induct_on `l`);
e (RW_TAC list_ss [cx_defn]);
- e (RW_TAC list_ss [cx_defn]);
OK..
1 subgoal:
> val it =
LENGTH (DROP h (cx l q p)) +
LENGTH (TAKE h (cx l p q)) =
LENGTH q
------------------------------------
0. !p q.
(LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
1. LENGTH p = LENGTH q
: proof
The definition of ?cx? is following:
|- (!q p. cx [] p q = p) /\
!v5 v4 q p.
cx (v4::v5) p q =
TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
Where, ?TAKE? is in listtheory in HOL4. It means that get firs n elements,
?DROP? is in listtheory in HOL4. It means that get after n elements,
I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==> (LENGTH
(DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named ?TAKE_DROP_LENGTH?.
But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH p =
LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the problem is
that in the goal the form is ?DROP h (cx l q p)?, but the actual form is ?DROP
h l?, where the format of ?(cx l q p)? is not equal to ?l?. But I can?t find a
good transform between them.
Could anyone give me some advices?
Thank you!
-------------- next part --------------
An HTML attachment was scrubbed...
------------------------------
Message: 2
Date: Mon, 29 Feb 2016 00:49:29 +1100
From: Jeremy Dawson <[email protected]>
Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
to "l"
To: <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="windows-1252"; format=flowed
It might be easier to avoid using TAKE_DROP_LENGTH
but instead try to simplify your subgoal using
LENGTH_TAKE_EQ and LENGTH_DROP
Then I think you'll have to instantiate your subgoal 0 once with p,q
and once with q,p
Cheers,
Jeremy
On 28/02/16 22:48, Ada wrote:
> Hey,guys
>
> I am learning to use HOL4. Here are some questions about my proving:
>
> g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p
> q) = LENGTH p) `;
>
> e (Induct_on `l`);
>
> e (RW_TAC list_ss [cx_defn]);
>
> - e (RW_TAC list_ss [cx_defn]);
>
> OK..
>
> 1 subgoal:
>
>> val it =
>
> LENGTH (DROP h (cx l q p)) +
>
> LENGTH (TAKE h (cx l p q)) =
>
> LENGTH q
>
> ------------------------------------
>
> 0.!p q.
>
> (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
>
> 1.LENGTH p = LENGTH q
>
> : proof
>
> The definition of ?cx? is following:
>
> |- (!q p. cx [] p q = p) /\
>
> !v5 v4 q p.
>
> cx (v4::v5) p q =
>
> TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
>
> DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
>
> Where,?TAKE? is in listtheory in HOL4. It means that get firs n
> elements,?DROP? is in listtheory in HOL4. It means that get after n
> elements,
>
> I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==>
> (LENGTH (DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named
> ?TAKE_DROP_LENGTH?.
>
> But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH
> p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the
> problem is that in the goal the form is ?DROP h (cx l q p)?, but the
> actual form is ?DROP h l?, where the format of ?(cx l q p)? is not equal
> to ?l?. But I can?t find a good transform between them.
>
> Could anyone give me some advices?
>
> Thank you!
>
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>
>
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------
Message: 3
Date: Sun, 28 Feb 2016 23:04:02 +0100
From: Petar Maksimovic <[email protected]>
Subject: [Hol-info] Two postdoc positions - Reasoning about
concurrency and distribution - Imperial College London
To: [email protected]
Message-ID:
<camdet4_g8lpv9qlqq4bqqttonogjo-km6x2nu+ljxgdxoo9...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
Hello everyone,
We are seeking two outstanding postdocs (one theoretical, one more
practical) with strong interests in the formal specification and
verification of concurrent and distributed systems to join the Program
Specification and Verification Group, led by Professor Philippa
Gardner, at Imperial College London.
Two three-year positions will be funded as part of "REMS: Rigorous
Engineering of Mainstream Systems", a 6-year EPSRC-funded programme
grant for ?5.6 million between Cambridge, Edinburgh and Imperial,
which finishes in 2019.
It is not easy to reason about concurrent programs. At Imperial, we
have considerable expertise in specifying concurrent libraries and
verifying concurrent programs. In particular, our recent work has
focussed on the extension of concurrent separation logic to handle
abstraction, abstract atomicity, fault-tolerance and progress. We have
applied this reasoning to, for example, concurrent indexes (B-trees
and java.util.concurrent skip lists), graph algorithms, the POSIX file
system and an ARIES database recovery algorithm.
Our immediate research goals are: to continue to provide logics for
reasoning about concurrent programs; to develop automated tools based
on our logics; to test the reasoning on key applications such as
databases, file systems and data centres; and to extend the reasoning
to distributed systems.
Please take a look at our Concurrency web page
(http://psvg.doc.ic.ac.uk/research/concurrency.html) for more details
and do not hesitate to contact Philippa at [email protected] if
you are interested in one of these postdoc positions.
Best wishes,
Petar Maksimovic
Petar Maksimovic, Ph.D.
Research Fellow
Department of Computing
Imperial College London
South Kensington Campus
London SW7 2AZ
Email: [email protected]
------------------------------
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
End of hol-info Digest, Vol 117, Issue 9
****************************************------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
