Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions
Thank you! > On Aug 28, 2018, at 8:29 PM, > wrote: > > Make the assumption the left-hand-side of an implication (moving it out of > the assumptions), rewrite with the identity that says that > > ((P /\ Q) ==> R) ó (P ==> (Q ==> R)) > > and then move all the implications’ left-hand-sides back into the assumptions. > > In HOL4 you could use something like > > th |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL > > The use of the _ALL functions makes this a bit fragile, but it will work in > your case. > > You might also find that the discharged theorem works directly as a > conditional rewrite (I don’t know what the HOL Light tools is for this). > > My HOL4-informed advice would be to avoid working with theorems that have > assumptions like this: the machinery copes better with theorems that are just > implications. (Of course, goals can have assumptions and the machinery copes > very well with those, but that is a different matter.) > > Michael > > From: Dylan Melville > Date: Tuesday, 28 August 2018 at 22:48 > To: "Norrish, Michael (Data61, Acton)" , > "hol-info@lists.sourceforge.net" > Subject: Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions > > That's what I figured. How can I separate the assumptions of > second_b13_complete? > > On Mon, Aug 27, 2018, 10:32 PM <mailto:michael.norr...@data61.csiro.au>> wrote: > The assumption of the rewrite theorem is not present in the assumptions of > the goal and so you get an invalid tactic. > > Strictly speaking this is not REWRITE_TAC failing but e. Indeed, you should > find that REWRITE_TAC [second_b13_complete] applied to the goal works just > fine. > > Michael > > From: Dylan Melville <mailto:dylanmelvi...@gmail.com>> > Date: Tuesday, 28 August 2018 at 11:45 > To: "hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>" > mailto:hol-info@lists.sourceforge.net>> > Subject: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions > > VERSION: HOL Light QE (augmentation of HOL Light, very similar) > > Hello all. Today I’ve been having 2 issues with HOL. The first is that > although the documentation for REWRITE_TAC says that the tactic has no > failure conditions, when I use the following command: > > # e (REWRITE_TAC[second_b13_complete]);; > > Where second_b13_complete is: > > # second_b13_complete;; > val it : thm = > isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\ > ~isFreeIn (QuoVar "n" (TyBase "num")) f > |- (\n. (\P. P n) (eval (f) to (num->bool))) = > (\P n. P n) (eval (f) to (num->bool)) > > When used with the following goal already declared: > > # p();; > val it : goalstack = 1 subgoal (1 total) > > 0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`] > 1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`] > 2 [`isPeano f`] > > `(eval (f) to (num->bool)) 0 /\ > (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool))) > ==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))` > > > Results in the following error: > > # e (REWRITE_TAC[first_b13_complete]);; > Exception: Failure "VALID: Invalid tactic”. > > > Which is confusing, since not only is the tactic supposed to have no failure > conditions, but the bolded sections of the theorem and the goal are matched > properly, and the two conjuncted antecedents of the theorem are assumptions 0 > and 1 of the goal. So, is the reason that the tactic application fails that > antecedents of the theorem are conjuncted? If so, is there a command I’m > missing that can transform the theorem to the proper form? > > Thanks in advance. > > Dylan Melville | McMaster University, Math and Computer Science -- 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] Failure with REWRITE_TAC and UNDISCH on conjunctions
That's what I figured. How can I separate the assumptions of second_b13_complete? On Mon, Aug 27, 2018, 10:32 PM wrote: > The assumption of the rewrite theorem is not present in the assumptions of > the goal and so you get an invalid tactic. > > > > Strictly speaking this is not REWRITE_TAC failing but e. Indeed, you > should find that REWRITE_TAC [second_b13_complete] applied to the goal > works just fine. > > > > Michael > > > > *From: *Dylan Melville > *Date: *Tuesday, 28 August 2018 at 11:45 > *To: *"hol-info@lists.sourceforge.net" > *Subject: *[Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions > > > > VERSION: HOL Light QE (augmentation of HOL Light, very similar) > > > > Hello all. Today I’ve been having 2 issues with HOL. The first is that > although the documentation for REWRITE_TAC says that the tactic has no > failure conditions, when I use the following command: > > > > # e (REWRITE_TAC[second_b13_complete]);; > > > > Where second_b13_complete is: > > > > # second_b13_complete;; > > val it : thm = > > isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\ > > ~isFreeIn (QuoVar "n" (TyBase "num")) f > > |- *(\n. (\P. P n) (eval (f) to (num->bool)))* = > > (\P n. P n) (eval (f) to (num->bool)) > > > > When used with the following goal already declared: > > > > # p();; > > val it : goalstack = 1 subgoal (1 total) > > > > 0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`] > > 1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`] > > 2 [`isPeano f`] > > > > `(eval (f) to (num->bool)) 0 /\ > > (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool))) > > ==> (\P. P = (\x. T)) *(\n. (\P. P n) (eval (f) to (num->bool)))*` > > > > Results in the following error: > > > > # e (REWRITE_TAC[first_b13_complete]);; > > Exception: Failure "VALID: Invalid tactic”. > > > > Which is confusing, since not only is the tactic supposed to have no > failure conditions, but the bolded sections of the theorem and the goal are > matched properly, and the two conjuncted antecedents of the theorem are > assumptions 0 and 1 of the goal. So, is the reason that the tactic > application fails that antecedents of the theorem are conjuncted? If so, is > there a command I’m missing that can transform the theorem to the proper > form? > > > > Thanks in advance. > > > > Dylan Melville | McMaster University, Math and Computer Science > -- 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
[Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions
VERSION: HOL Light QE (augmentation of HOL Light, very similar) Hello all. Today I’ve been having 2 issues with HOL. The first is that although the documentation for REWRITE_TAC says that the tactic has no failure conditions, when I use the following command: # e (REWRITE_TAC[second_b13_complete]);; Where second_b13_complete is: # second_b13_complete;; val it : thm = isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\ ~isFreeIn (QuoVar "n" (TyBase "num")) f |- (\n. (\P. P n) (eval (f) to (num->bool))) = (\P n. P n) (eval (f) to (num->bool)) When used with the following goal already declared: # p();; val it : goalstack = 1 subgoal (1 total) 0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`] 1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`] 2 [`isPeano f`] `(eval (f) to (num->bool)) 0 /\ (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool))) ==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))` Results in the following error: # e (REWRITE_TAC[first_b13_complete]);; Exception: Failure "VALID: Invalid tactic”. Which is confusing, since not only is the tactic supposed to have no failure conditions, but the bolded sections of the theorem and the goal are matched properly, and the two conjuncted antecedents of the theorem are assumptions 0 and 1 of the goal. So, is the reason that the tactic application fails that antecedents of the theorem are conjuncted? If so, is there a command I’m missing that can transform the theorem to the proper form? Thanks in advance. Dylan Melville | McMaster University, Math and Computer Science-- 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] Assumptions of goal usage
As a more concise question: can you use assumptions of the hypothesis to eliminate the assumptions of a theorem? On Mon, Aug 20, 2018, 4:51 PM Dylan Melville wrote: > Let's say I have a goal, > > a /\ b /\ c ==> d > > and 2 theorems > > a /\ b ==> e > > e ==> f > > All I need to do to solve the goal is rewrite using a theorem that states > `f`, however I need to first prove e, which is only probable because the > goal assumes `a`. > > The basis of my question, is whether or not I can use an assumption of the > goal outside of a tactical. My proof would be a lot more readable if I > could use `a` and `b` to "prove" `e` outside of a tactical application like > ASSUM_LIST and similar tactics require. > -- 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
[Hol-info] Assumptions of goal usage
Let's say I have a goal, a /\ b /\ c ==> d and 2 theorems a /\ b ==> e e ==> f All I need to do to solve the goal is rewrite using a theorem that states `f`, however I need to first prove e, which is only probable because the goal assumes `a`. The basis of my question, is whether or not I can use an assumption of the goal outside of a tactical. My proof would be a lot more readable if I could use `a` and `b` to "prove" `e` outside of a tactical application like ASSUM_LIST and similar tactics require. -- 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
[Hol-info] Using Assumptions
Is there anyway to reference a specific assumption of the current goal as a theorem? -- 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] Applying a theorem to a specific subgoal
Thank you, this was perfect! > On Aug 8, 2018, at 2:31 AM, Heiko Becker wrote: > > Hello Dylan, > > There are two ways (I know of) to easily work on subgoals: > > 1) You use the >- symbol and not \\ or THEN as it only applies to the first > subgoal > > 2) You use THENL an give it a list of tactics, where the i-th element the > list is applied to subgoal i. > > Personally, I would recommend using ">-". > > Best regards, > > Heiko > > > On 08/08/2018 07:24 AM, Dylan Melville wrote: >> When a goal is separated into multiple subgoals during a proof of the form >> >> # prove(thm,tactic);; >> >> >> Where the last tactic is something like >> >> REPEAT CONJ_TAC >> >> Is there a way to specify that the next tactic should be applied to a >> specific subgoal? In the proof I’m working on, it was applied to all >> subgoals. >> >> >> -- >> 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 > > > -- > 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 -- 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
[Hol-info] Applying a theorem to a specific subgoal
When a goal is separated into multiple subgoals during a proof of the form # prove(thm,tactic);; Where the last tactic is something like REPEAT CONJ_TAC Is there a way to specify that the next tactic should be applied to a specific subgoal? In the proof I’m working on, it was applied to all subgoals. -- 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
[Hol-info] Term Concatenation
How do you concatenate terms in HOL? -- 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] INST on a theorem
Is there a way to print theorems with types displayed? > On Jul 23, 2018, at 12:20 PM, Thomas Tuerk wrote: > > Hi, > > hard to say, why it does not work without further details. However, one guess > is that types do not match. I would recommend showing the types when printing > the theorem. I expect that P might be of type `'a -> bool`. In this case you > need to instantiate 'a to string first. > > Best > > Thomas > > On 23.07.2018 18:10, Dylan Melville wrote: >> I have a theorem called EX which returns true when a value is an element of >> a list. It is defined as: >> >> thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t) >> >> I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t` being >> a long list of strings which contains “T”. Unfortunately my attempts to use >> INST on this theorem haven’t worked. Why doesn’t the following work? >> >> INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;; >> >> Thank you. >> >> -Dylan Melville (McMaster University) >> >> >> -- >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> <http://sdm.link/slashdot> >> >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> <https://lists.sourceforge.net/lists/listinfo/hol-info> > > -- > 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 -- 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
[Hol-info] INST on a theorem
I have a theorem called EX which returns true when a value is an element of a list. It is defined as: thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t) I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t` being a long list of strings which contains “T”. Unfortunately my attempts to use INST on this theorem haven’t worked. Why doesn’t the following work? INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;; Thank you. -Dylan Melville (McMaster University)-- 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
[Hol-info] MESON
I have a set of theorems, which state: let thm1 = A;; let thm2 = A <=> B;; And I want a theorem that states B. I tried making B my goal, and using MESON_TAC[thm1,thm2] but MESON timed out. What’s the proper way to prove B? -- 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] Adding abstraction to terms
Thank you! > On Jul 6, 2018, at 1:04 PM, Mario Xerxes Castelán Castro > wrote: > > This is eta conversion. It is handled in HOL4 by the simplifier and both > HOL4 and HOL Light have conversions called “ETA_CONV” that are more low > level. > > On 06/07/18 12:01, Dylan Melville wrote: >> Is there a tactical that shows that a term is equal to the same term with an >> added abstraction, for example: >> >> |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n >> >> Or even more simply >> >> |- f:(num->bool) <=> (\x:num. f:(num->bool) ) >> -- >> 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 >> > > -- > 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 -- 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
[Hol-info] Adding abstraction to terms
Is there a tactical that shows that a term is equal to the same term with an added abstraction, for example: |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n Or even more simply |- f:(num->bool) <=> (\x:num. f:(num->bool) ) -- 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] Taking universal quantification off an assumption
Okay, I imagine HOL-Light does the same. Thank you > On Jul 3, 2018, at 3:36 PM, Mario Xerxes Castelán Castro > wrote: > > Please include the mailing list in your replies. I do not know what you > are doing. Anyway, this does not look like HOL4. Are you using HOL > Light? I only know about HOL4. Removing the quantifier will usually be > done internally by the subsequent tactic that requires using the > proposition with a specific specialization of “n” and there is no need > to specialize the assumption manually. > > On 03/07/18 14:31, Dylan Melville wrote: >> I’m trying to prove a statement about Induction Schemas, after. Breaking >> assumptions into hypotheses I’m left with >> >> val it : goalstack = 1 subgoal (1 total) >> >> 0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`] >> 1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`] >> 2 [`isPeano f`] >> 3 [`(eval (f) to (num->bool)) 0`] >> 4 [`!n. (eval (f) to (num->bool)) n ==> (eval (f) to (num->bool)) (SUC >> n)`] >> >> `(eval (f) to (num->bool)) n` >> >> What I need help with only pertains to assumption 4 and the goal. >> >> f was originally universally quantified across the entire original term >> and so was n in all statements where it is free. I assumed that it would >> be easier to manipulate the expressions in the way I want without the >> quantifications, but I am fairly new, so if as you say most theorems / >> tactical handle the universal quantification seamlessly maybe I’m wrong. >> Otherwise, I’d like to strip the forall from the 4th assumption. >> >>> On Jul 3, 2018, at 3:23 PM, Mario Xerxes Castelán Castro >>> mailto:marioxcc...@yandex.com>> wrote: >>> >>> An hypothesis of the form “∀x. P” where “x” occurs free in P is stronger >>> than just “P” (that is, the former entails the later). Many tactics have >>> built-in specialization, so it depends on what you want to do. Can you >>> provide more details? >>> >>> On 03/07/18 14:18, Dylan Melville wrote: >>>> Is there any tactical that can take universal quantification off of a >>>> hypothesis like how GEN_TAC does with the goal? >>>> >>>> -Dylan >>>> -- >>>> Check out the vibrant tech community on one of the world's most >>>> engaging tech sites, Slashdot.org <http://Slashdot.org>! >>>> http://sdm.link/slashdot >>>> ___ >>>> hol-info mailing list >>>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>>> >>> >>> -- >>> Check out the vibrant tech community on one of the world's most >>> engaging tech sites, Slashdot.org <http://Slashdot.org>! >>> http://sdm.link/slashdot___ >>> hol-info mailing list >>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >>> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > -- > 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 -- 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
[Hol-info] Taking universal quantification off an assumption
Is there any tactical that can take universal quantification off of a hypothesis like how GEN_TAC does with the goal? -Dylan -- 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] Tactic
Also, the version Im using is HOL - Light > On Jun 28, 2018, at 5:38 PM, Dylan Melville wrote: > > Is there a tactic for splitting conjoined assumptions into separate > assumptions? -- 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
[Hol-info] Tactic
Is there a tactic for splitting conjoined assumptions into separate assumptions? -- 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] Formalizing logical puzzles
Correcting a mistake: the goldInsc definition was supposed to be # let goldInsc = new_definition `goldInsc gc <=> ~ gc`;; > On Jun 26, 2018, at 10:35 AM, Dylan Melville wrote: > > I’m working on learning the basics of using HOL to solve logic puzzles, such > as the ‘Portia’s Suitor’ problem: > > Portia has a gold casket and a silver casket and has placed a picture of > herself in one of them. On the caskets, she has written the following > inscriptions: > > • Gold: The portrait is not in here > • Silver: Exactly one of these inscriptions is true. > > Portia explains to her suitor that each inscription may be true or false, but > that she has placed her portrait in one of the caskets in a manner that is > consistent with the truth or falsity of the inscriptions. > If the suitor can choose the casket with her portrait, she will marry him. > > Obviously this is a very simple problem, but when inputting the proof into > HOL Light, I had an issue. The first axiom, the gold inscription I formalized > as > > # let goldInsc = new_definition `goldInsc gc = not gc`;; > > Then attempted the silver inscription as > > # let silvInsc = new_definition `silvInsc gc <=> silvInsc gc <=> ~ (goldInsc > gc)`;; > > Which doesn’t work as intended, obviously since goldInsc is a theorem, not an > actual function. What is the proper way to express the silver inscription? -- 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
[Hol-info] Formalizing logical puzzles
I’m working on learning the basics of using HOL to solve logic puzzles, such as the ‘Portia’s Suitor’ problem: Portia has a gold casket and a silver casket and has placed a picture of herself in one of them. On the caskets, she has written the following inscriptions: • Gold: The portrait is not in here • Silver: Exactly one of these inscriptions is true. Portia explains to her suitor that each inscription may be true or false, but that she has placed her portrait in one of the caskets in a manner that is consistent with the truth or falsity of the inscriptions. If the suitor can choose the casket with her portrait, she will marry him. Obviously this is a very simple problem, but when inputting the proof into HOL Light, I had an issue. The first axiom, the gold inscription I formalized as # let goldInsc = new_definition `goldInsc gc = not gc`;; Then attempted the silver inscription as # let silvInsc = new_definition `silvInsc gc <=> silvInsc gc <=> ~ (goldInsc gc)`;; Which doesn’t work as intended, obviously since goldInsc is a theorem, not an actual function. What is the proper way to express the silver inscription?-- 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
