I’m working on a proof in Welder and running into issues with what seems like a strong induction scenario. I need to prove that when two lists have identical contents and an operation is idempotent, associative, and commutative, then applying reduce(op, initial, list1) equals reduce(op, initial, list2). During my proof, I have a list called list1 structured as head::tail, and I want to demonstrate that reduce(op, initial, exclude(head, tail)) equals reduce(op, initial, exclude(head, list2)). The exclude function removes all instances of the specified element from a list. Since exclude(head, tail) has fewer elements than head::tail, this looks like a perfect case for strong induction based on list size. However, Welder gives me an error saying no induction hypothesis exists for exclude(head, tail). What’s the proper way to set up and use strong induction in Welder? Are there specific tactics or approaches I should use?
The issue you’re encountering is that Welder’s induction mechanism needs explicit guidance when dealing with nested recursive structures like your exclude function. Since exclude(head, tail) doesn’t directly match the structural pattern of your original induction variable, Welder can’t automatically recognize the induction hypothesis applies. You’ll need to manually establish the connection using a lemma that proves the size relationship between your original list and the result of exclude. I’ve found success by first proving a helper lemma that shows exclude always produces a list with size less than or equal to the original, then using that lemma to invoke the induction hypothesis explicitly. Try setting up your proof with lemma size_exclude_le to establish this relationship before attempting to apply the induction hypothesis to your exclude expressions.
welder struggles with non-structural induction patterns like this. try using induction_on tactic with a custom measure instead of relying on automatic induction. you’ll need somthing like induction_on (list_length list1) then manually show that list_length (exclude(head, tail)) < list_length (head::tail). this way welder knows the recursive call is on a smaller argument.
Strong induction in Welder requires you to prove termination explicitly through a well-founded ordering on your data structure. For your case, you need to establish that the recursive calls are made on strictly smaller arguments according to some measure. The key is defining a measure function that captures the “size” or “complexity” of your input and then proving this measure decreases with each recursive step. In your situation, define a measure based on list length and prove that exclude operations preserve the required ordering. Use the decreases clause in your function definition to specify this measure, then Welder will automatically generate the necessary induction hypotheses. Without this explicit measure, Welder cannot determine which induction principle to apply, which explains why you’re getting the “no induction hypothesis” error.