Hi Thomas,
Thank you for your detailed answers, now I get it. I will try to ues another
method to solve my problem.
Regards,
Liu
-----Original Messages-----
From:"Thomas Tuerk" <[email protected]>
Sent Time:2017-12-19 23:10:56 (Tuesday)
To: [email protected]
Cc:
Subject: Re: [Hol-info] How can I instantiate the variable which constrained by
the existential quantifier in the parentheses？
Hi Liu,
you can't instantiate such a variable. The existential quantifier in your
formula is morally a universal one.
(?x. P x) ==> Q
is equivalent to
!x. (P x ==> Q)
Let's make an example and instantiate P and Q as follows:
P x := (x = 5)
Q := F
Then (?x. P x) ==> Q does not hold. "?x. P x" is true (witness x = 5) and Q is
F, so we get T ==> F, which is F.
If we were allowed to instantiate x, we could have with x := 6 the proof
obligation (6 = 5) ==> F, which can be shown. So, this shows that instantiating
such existential quantifiers is not a valid operation.
Technically speaking, the existential quantifier in your formula occurs at odd
negation level and is therefore really a universal one.
Cheers
Thomas
On 19.12.2017 12:21, Liu Gengyang wrote:
Hi，
How can I instantiate the variable which constrained by the existential
quantifier in the parentheses(i.e. (?x. _) ==> _, replacing x with a specific
value.)? For example,
(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)
Now I want to instantiate `l` using `[]` ,which tactic or lemma I could use(I
know I can use simplify tactics here, but that not I wanted.)? I have seen the
proof process of APPEND_EQ_APPEND, but it didn't instantiate `l`.
Regards,
Liu
------------------------------------------------------------------------------
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
[email protected]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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
