I think a good start to tracking it down would be to remove tactics from the
end of 't' (starting with 't2') until it doesn't fail. Then check that the
resulting goal states are alpha-equivalent. If they are then the culprit
should be the next tactic, otherwise carry on going back until the goal
states are alpha-equivalent.
Mark.
on 17/6/13 2:11 PM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> Yes, I was not claiming that b() is the problem. I am just curious as to
> why the tactic fails when I apply it a second time, since I can't find any
> explicit use of references, and I think I'm only using tactics from
bossLib
> (and lcsymtacs).
>
> On Mon, Jun 17, 2013 at 1:58 PM, Konrad Slind
<konrad.sl...@gmail.com>wrote:
>
>> If that top_goal was the "original", then the tactic simply fails,
>> and it has nothing to do with the use of b().
>>
>> Konrad.
>>
>>
>>
>> On Mon, Jun 17, 2013 at 6:38 AM, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk>wrote:
>>
>>> t (top_goal());
>>> val it = ([], fn): goal list * validation
>>> t (top_goal());
>>> Exception- HOL_ERR {message = "first subgoal not solved by second
>>> tactic", origin_function = "THEN1", origin_structure = "Tactical"}
raised
>>>
>>> I didn't think there were any refs touched by t, but I'll have a look
>>> more closely...
>>>
>>>
>>> On Sun, Jun 16, 2013 at 10:21 PM, Konrad Slind
> <konrad.sl...@gmail.com>wrote:
>>>
>>>> > Could you perhaps tell me what could possibly be behind the behaviour
>>>> above?
>>>>
>>>> Superficial answer: refs
>>>>
>>>> Do you get the same behaviour if you invoke t away from the goalstack?
>>>>
>>>> t (top_goal()) = t (top_goal())
>>>>
>>>>
>>>> Konrad.
>>>>
>>>>
>>>> On Sun, Jun 16, 2013 at 3:03 PM, Ramana Kumar
<ramana.ku...@cl.cam.ac.uk
>>>> > wrote:
>>>>
>>>>> I have run into strange problem:
>>>>> e(t); (* succeeds and proves the goal *)
>>>>> b(); (* return to original goal *)
>>>>> e(t); (* fails *)
>>>>>
>>>>> I'll copy the code for t below, but there's a lot of required context,
>>>>> which I won't go into in this first message... Could you perhaps tell
> me
>>>>> what could possibly be behind the behaviour above?
>>>>>
>>>>> My t is (tac >> t2), where
>>>>> val t2 = metis_tac[RTC_TRANSITIVE,transitive_def]
>>>>> val tac =
>>>>> rpt gen_tac >>
>>>>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >>
>>>>>
>>>>>
>
qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`](Q.X_CHOOSE_THEN`cb`
> strip_assume_tac)(CONJUNCT1
>>>>> (CONJUNCT2 compile_append_out)) >>
>>>>> simp[Abbr`cs1`] >>
>>>>> REWRITE_TAC[Once SWAP_REVERSE] >>
>>>>> simp[] >> strip_tac >>
>>>>> qpat_assum`(A.out = cb ++ B)`mp_tac >>
>>>>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >> strip_tac >>
>>>>> qabbrev_tac`tt = case t of TCNonTail => t | TCTail j k =>
>>>>> TCTail j (k + 1)` >>
>>>>>
>>>>>
>
qspecl_then[`cmnv`,`CTLet(sz+1)::cenv`,`tt`,`sz+1`,`cs1`,`exp'`](Q.X_CHOOSE_
> THEN`cd`strip_assume_tac)(CONJUNCT1
>>>>> compile_append_out) >>
>>>>> first_x_assum(qspecl_then[`rd'`,`cmnv`,`cs1`,`CTLet
>>>>> (sz+1)::cenv`,`sz+1`,`csz`,`bs2`,`bce`,`bcr`
>>>>> ,`bc0 ++ REVERSE cc`
>>>>> ,`REVERSE cd`,`(DROP (LENGTH cd)
>>>>> (REVERSE cb))++bc1`]mp_tac) >>
>>>>> discharge_hyps >- (
>>>>> simp[TAKE_APPEND1,TAKE_APPEND2,Abbr`bs2`] >>
>>>>> conj_asm1_tac >- (
>>>>>
>>>>>
> qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`,`cb`,`cd`]mp_tac
>>>>> compile_bindings_thm >>
>>>>> simp[DROP_APPEND1,DROP_LENGTH_NIL_rwt] ) >>
>>>>> conj_tac >- PROVE_TAC[] >>
>>>>>
>>>>>
>
fs[Cenv_bs_def,s_refs_def,SUM_APPEND,FILTER_APPEND,ALL_DISTINCT_APPEND,FILTE
> R_REVERSE,EVERY_REVERSE]
>>>>> >>
>>>>>
>>>>>
>
fsrw_tac[DNF_ss][MEM_FILTER,EVERY_MEM,is_Label_rwt,ALL_DISTINCT_REVERSE,MEM_
> MAP,between_def]
>>>>> >>
>>>>> fsrw_tac[ARITH_ss][Abbr`cs1`] >>
>>>>> rw[] >> spose_not_then strip_assume_tac >> res_tac >>
>>>>> fsrw_tac[ARITH_ss][] ) >>
>>>>> simp[] >>
>>>>> disch_then(qspec_then`tt`mp_tac) >>
>>>>> TRY(disch_then(qspecl_then[`bv::ig`,`sp`,`hdl`,`st`]mp_tac))
>>
>>>>> discharge_hyps >- (
>>>>> simp[Abbr`bs2`] >>
>>>>> simp[Abbr`tt`] >>
>>>>> Cases_on`t`>>fs[] >>
>>>>> qexists_tac`bv::blvs`>>simp[]>>
>>>>> qexists_tac`args`>>simp[])
>>>>>
>>>>>
>>>>>
>>>>>
>
----------------------------------------------------------------------------
> --
>>>>> This SF.net email is sponsored by Windows:
>>>>>
>>>>> Build for Windows Store.
>>>>>
>>>>> http://p.sf.net/sfu/windows-dev2dev
>>>>> _______________________________________________
>>>>> hol-info mailing list
>>>>> hol-info@lists.sourceforge.net
>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>
>>>>>
>>>>
>>>
>>
>
>
>
> ----------------------------------------
>
>
----------------------------------------------------------------------------
> --
> This SF.net email is sponsored by Windows:
>
> Build for Windows Store.
>
> http://p.sf.net/sfu/windows-dev2dev
>
>
> ----------------------------------------
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:
Build for Windows Store.
http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
