On 14.02.2014 01:42, Michael Norrish wrote:
On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste...
I
know it is the standard to leave the goal unchanged. But I personally met
many
buggy situations that I hardly detected
On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste... I
know it is the standard to leave the goal unchanged. But I personally met many
buggy situations that I hardly detected because HOL {4,Light} was just
allowing
a
OK, my original example now works.
But I get exception Unchanged raised when I try IMP_REWRITE_TAC[] on the
goal ``p \/ q == q \/ p``.
I still would expect the tactic to be able to solve this goal, no?
And if it can't then would it not be better to leave the goal unchanged
rather than to raise an
Hi Ramana,
this is intended: what makes the tactic solve p /\ q == q /\ p is
that it uses the context p /\ q when doing the rewriting. Therefore
the theorems used for the rewrite are p = T and q = T, which indeed
turns p /\ q into T /\ T.
However with p \/ q the context only brings (p \/
Hi Vincent,
I have just now started trying to use your new tactic, and I am having some
trouble. When I call IMP_REWRITE_TAC[] on some simple goal like ``p /\ q
== q /\ p``, it raises an exception (Unchanged). Is this the intended
behaviour? That seems pretty annoying.
Also, I have not yet found
Hi Ramana,
- regarding your example: no, it is not the intended behavior. I'll have
a look asap.
- regarding the infinite loop: do you mean that it goes most of the time
into an infinite loop? This is not normal either... Could you provide me
with such examples?
The examples provided in
So indeed, the goal is solved immediatly in HOL Light... Gonna work on
it :-/
Le 10/02/2014 18:39, Vincent Aravantinos a écrit :
Hi Ramana,
- regarding your example: no, it is not the intended behavior. I'll
have a look asap.
- regarding the infinite loop: do you mean that it goes most of
Solved. The new version is uploaded:
https://github.com/aravantv/HOL4-impconv
Thanks for the report! Was indeed a mistake in the translation from
HOL-Light/Ocaml to HOL4/SML...
V.
Le 10/02/2014 21:00, Vincent Aravantinos a écrit :
So indeed, the goal is solved immediatly in HOL Light...
This looks great, Vincent.
Are you interested in working on a version for HOL4?
On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com wrote:
Hi list,
I developed a new tactic that takes a theorem of the form P == l = r and
replaces l by r in a goal adding
Hi Ramana,
I will make a few performance improvements on the HOL Light version in the
coming weeks hopefully, and then I plan indeed to translate it to HOL4.
V.
2013/7/30 Ramana Kumar ramana.ku...@cl.cam.ac.uk
This looks great, Vincent.
Are you interested in working on a version for HOL4?
Hi list,
I developed a new tactic that takes a theorem of the form P == l = r and
replaces l by r in a goal adding whatever it needs to make it work properly
(typically conjunction with P; but can also be an implication or even
existentials).
This is a follow-up of the discussion I started a few
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to reduce the user's burden of subgoal splits *)
(* when creating tactics to prove theorems. If a separate subgoal*)
(* is desired, simply use CONJ_TAC after
Forgot: in the examples below, both tactics are used with the theorem |-
!x. x 0 == x / x = 1
2013/7/11 Vincent Aravantinos vincent.aravanti...@gmail.com
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to
13 matches
Mail list logo
