Hello.
You can not choose the value of «l» because it is in the antecedent. You
must prove it for any value of “l”, as seen in the following equivalence:
> SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM]
“(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”;
<<HOL message: inventing new type variable names: 'a>>
val it =
⊢ (∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2) ⇔
∀l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2) ⇒ (m1 ⧺ m2 = l1 ⧺ l2):
thm
You can discharge the antecedent and strip the existential quantifier
leaving a fresh free variable. Use “disch_then strip_assume_tac” or more
simply, “rpt strip_tac”.
Maybe this is what you want:
prove(
“(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”,
disch_then strip_assume_tac >>
rpt BasicProvers.var_eq_tac >>
MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC);
On 19/12/17 05:21, Liu Gengyang wrote:
> 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`.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
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
