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
> 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
