The right strategy when confronted like a goal such as LENGTH (APP [] l2) = LENGTH [] + LENGTH l2
is to look at the sub-terms that contain patterns that “should” be simpler. When I look at the above, I see APP [] l2 and LENGTH [] You have equational theorems to hand that have terms matching these patterns on their left-hand sides. So, I’d simplify with those theorems. Then, you’d hope that APP [] l2 will turn into l2, and that LENGTH [] will turn into 0. That won’t quite solve the goal but it will get you very close. Michael On 28 Feb 2022, at 01:56, Kyle Darling via hol-info <hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>> wrote: Good morning, I’m currently taking a class where HOL is used but not taught via example and solution, this in turn has swayed my interest in HOL until I found the 2017 lecture on the hol-theorem-prover website. I’ve been stuck on what the TA for the class says “Is an easy question and help isn’t needed”, I joined the Slack channel though it doesn’t seem like the place to ask a homework related question. I apologize if this isn’t the correct place either but I’m at wits end attempting to solve something that’s allegedly simple. As solutions are never posted for the questions, learning HOL has been near impossible given the resources we’re handed, as such, this question is from last weeks and relates to this weeks problem and builds off of it. We’re given the following: val APP_def = Define `(APP [] (l: 'a list) = l) /\ (APP (h::(l1: 'a list)) (l2: 'a list) = h::(APP l1 l2))` Afterwards we’re asked to prove the following: ([], ``!(l1: 'a list)(l2: 'a list).LENGTH (APP l1 l2) = (LENGTH l1 + LENGTH l2)``) My first instinct is to Induct on l1 and apply, as suggested, arithmeticTheory.ADD_CLAUSES. Induct_on `l1` REWRITE_TAC [arithmeticTheory.ADD_CLAUSES] Afterwards I’m left with: ∀l2. LENGTH (APP [] l2) = LENGTH [] + LENGTH l2 My next intuition is to run REPEAT GEN_TAC and Induct on l2, though this just ends up with the current subgoal above where both l1 and l2 have been replaced with [] respectively. And that’s where I’m stumped. ———— Originally the TA had e(CONJ_TAC [arithmeticTheory.ADD_CLAUSES]) and was told to find something similar, though the first partition is what I want. Thanks for any help, HOL seems great but this class has been a huge turn away for wanting to learn a new language; I’m a Software Engineer and that says a great deal about how this course is being carried out. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
