Thanks,
yes I've just understood that point: that MP won't work because t and t'
are free and so they are different and can't be unified.
The problem was in the parenthesis in my initial goal: changing the
parenthesis the goal was solved by METIS_TAC from the beginning.
Thanks,
Domenico
2013/10/20 Ramana Kumar <ram...@member.fsf.org>
> OK, to specialise assumption 0 with `u`, you can use the following:
> FIRST_X_ASSUM(Q.SPEC_THEN`u`ASSUME_TAC)
>
> In general, to apply some inference rule to an assumption, you can use
> something like
> selector (fn th => ASSUME_TAC (rule th))
> where selector is something to pick the right assumption, like
> FIRST_X_ASSUM, or Q.PAT_ASSUM.
> A lot of those functions to pass to the selector are predefined (like the
> SPEC_THEN I used above).
>
> Your step 2) however, won't prove your goal, because t is different from
> t'.
> If your goal only contain t and not t', you could use RES_TAC at that
> point (or METIS_TAC[]) to prove it.
>
>
> On Sun, Oct 20, 2013 at 10:57 AM, Domenico D. D. Masini <
> domenico.mas...@gmail.com> wrote:
>
>> Sorry, I want to use SPEC not GEN in the step 1).
>>
>> Kind Regards,
>> Domenico
>>
>>
>> 2013/10/20 Domenico D. D. Masini <domenico.mas...@gmail.com>
>>
>> Hello,
>>>
>>> thanks for the reply but the goal to me seems trivial from the current
>>> assumptions in the goalstack.
>>>
>>> I want to generalize 'u' (not 't')
>>>
>>> 1) from the assumption 0: '!u. (R (t,u) ==> ?v. R (t,v) /\ R (u,v))' to
>>> obtain R (t,u) ==> ?v. R (t,v) /\ R (u,v), then
>>> 2) with MP from the new 0: R (t,u) ==> ?v. R (t,v) /\ R (u,v) and the
>>> assumption 1: R (t',u), obtain ?v. R (t',v) /\ R (u,v) which is just the
>>> goal.
>>>
>>> The problem is that I want to generalize on the assumption and not the
>>> goal.
>>>
>>> Kind Regards,
>>> Domenico
>>>
>>>
>>>
>>>
>>>
>>> 2013/10/19 Ramana Kumar <ram...@member.fsf.org>
>>>
>>>> The variable `t` in your goal cannot be generalised, for the same
>>>> reason that you can't generalise variables that appear free in the
>>>> assumptions of a theorem.
>>>>
>>>> I think the goalstack you showed is unproveable. But it looks like you
>>>> probably did an induction without using a general enough induction
>>>> hypothesis.
>>>> Perhaps show us your initial goal. The answer to "How can I apply GEN
>>>> to the assumption 0?" might be "generalise your induction hypothesis".
>>>>
>>>> On Sat, Oct 19, 2013 at 11:53 AM, Domenico D. D. Masini <
>>>> domenico.mas...@gmail.com> wrote:
>>>>
>>>>> Hello,
>>>>>
>>>>> I'm trying to learn hol, and one thing is not clear to me is how to
>>>>> mix forward proof in a goal directed proof while being in an active goal
>>>>> package session.
>>>>>
>>>>> One thing I was trying is to complete a proof with this current
>>>>> goalstack:
>>>>>
>>>>> ?v. R (t',v) /\ R (u,v)
>>>>> ------------------------------------
>>>>> 0. !u. R (t,u) ==> ?v. R (t,v) /\ R (u,v)
>>>>> 1. R (t',u)
>>>>>
>>>>> How can I apply GEN to the assumption 0 and then MP on the new 0 and 1?
>>>>>
>>>>> Thanks for any suggestion.
>>>>>
>>>>> Kind Regards,
>>>>> Domenico
>>>>>
>>>>>
>>>>> ------------------------------------------------------------------------------
>>>>> October Webinars: Code for Performance
>>>>> Free Intel webinars can help you accelerate application performance.
>>>>> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the
>>>>> most from
>>>>> the latest Intel processors and coprocessors. See abstracts and
>>>>> register >
>>>>>
>>>>> http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
>>>>> _______________________________________________
>>>>> hol-info mailing list
>>>>> hol-info@lists.sourceforge.net
>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>
>>>>>
>>>>
>>>
>>
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
