Hanno Becker (Jun 04 2023 at 19:15): Hanno Becker (Jun 04 2023 at 19:15):Hi! I got a conditional rewrite rule X which I can successfully via subst X; simp in the sense that (a) the rewrite conditions can be solved, (b) the original subgoal is solved after the rewrite. However, simp add: X does not work. Also (perhaps unrelated?) subst X, simp did fail, which puzzled me because I thought of the action of subst X; simp as being a superset of subst X, simp: The former applying simp to _all_ subgoals generated by subst X, the latter only to the first. But I must have misunderstood something here...
Hanno Becker (Jun 05 2023 at 05:24):I think I figured it out...: when there are multiple conditions to the rewrite, _and_ some of them introduce schematics, the order in which you tackle the subgoals matters. Now, subst X; simp tackles them in reverse order, while subst X, simp tries the first emerging subgoal first. In my case, the order of conditions was so that simp would solve later conditions and instantiate the involved schematic, and then simp would be able to handle the first condition as well -- but simp wouldn't be able to handle the first condition directly. A similar reason seems to apply to subst X; simp vs. simp add: X: My suspicion is that the default subgoaler would tackle the rewrite conditions in simp add: X in their order of definition, while subst X; simp, as mentioned, uses the reversed order. Indeed, swapping the two rewrite conditions in question, subst X; simp suddenly starts to fail while simp add: X succeeds.
Last updated: Apr 28 2024 at 08:19 UTC