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 https://lists.sourceforge.net/lists/listinfo/hol-info
