Hi Mario, I just want to instantiate `l`, but now I know it is impossible. I will try another method. Thank you for your answers.
Regards, Liu > -----Original Messages----- > From: "Mario Castelán Castro" <marioxcc...@yandex.com> > Sent Time: 2017-12-19 23:27:35 (Tuesday) > To: hol-info@lists.sourceforge.net > Cc: > Subject: Re: [Hol-info] How can I instantiate the variable which constrained > by the existential quantifier in the parentheses？ > > 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 ------------------------------------------------------------------------------ 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
