I’m working on a proof in Welder and I need to use strong induction but I’m not sure if it’s supported or how to do it.
My goal: Prove that if elements(list1) == elements(list2) and g is idempotent, associative and commutative, then reduce(g, initial, list1) = reduce(g, initial, list2)
The problem: During my proof, I have a list list1 in the form y::ys and I want to show:
Here filter_out(y, .) removes all instances of y from the list. Since filter_out(y, ys) has smaller size than y::ys, I should be able to apply strong induction (the contents are still equal).
Current issue: Welder says there’s no induction hypothesis available for filter_out(y, ys).
Does Welder support strong induction? If yes, what’s the correct syntax or approach to use it in this case?
Been there with complex theorem proving workflows. Skip wrestling with Welder’s induction limitations - just automate the proof generation.
I built a system that breaks strong induction proofs into smaller chunks regular provers can actually handle. It auto-generates well-founded relation proofs, termination conditions, and all those auxiliary lemmas you’d otherwise write by hand.
For your case, it’d:
Generate length comparison lemmas between original and filtered lists
Create intermediate theorems for your algebraic properties
Build proof structure Welder accepts
Handle repetitive lemma chaining automatically
Saves weeks of manual proof engineering. You handle the math insights, automation deals with tedious mechanics.
Best part? Once you automate this pattern, similar strong induction problems become trivial.
I’ve had success proving a decreasing measure function explicitly. Define measure(list) = length(list) and prove measure(filter_out(y, ys)) < measure(y::ys). Then use Welder’s built-in well-founded induction on this measure instead of trying direct strong induction on the list structure. You’ll need to establish well-foundedness first, but once that’s done, Welder accepts the induction hypothesis for any term with smaller measure. This worked for similar proofs with filtered sublists where structural induction wasn’t enough.
welder lacks direct support for strong induction, but you can prove lemmas with the filtered list then apply reg induction to the original. just make sure your proof fits the ::ys structure, not directly on the filtered list.
I’ve dealt with similar proofs before. Try structural induction on a different parameter instead of inducting directly on the filtered list. Prove a more general theorem first about list permutations and your reduction operation. Since g has idempotent, associative, and commutative properties, element order and multiplicity won’t affect the final result. I’d prove an auxiliary lemma showing your reduction stays invariant under element reordering, then use regular structural induction on the original lists. The key insight: with those algebraic properties, you can treat the reduction as a multiset operation rather than a list operation. Makes the proof much more straightforward in Welder’s framework.
Honestly, you might need to restructure your whole approach. Don’t try to force strong induction. Instead, prove your reduction function commutes with element removal because of the idempotent property. Once you do that, the proof’s trivial - removing y from both lists keeps them equal.
Hit this same wall before. Welder doesn’t do strong induction out of the box, but here’s what works: define a well-founded relation on list lengths and prove termination yourself. Make a helper lemma showing the length relationship between your original list and filtered result. Use that to justify the recursive call. Prove length(filter_out(y, ys)) < length(y::ys) as a separate lemma first, then reference it in your main proof to show valid induction. More verbose than direct strong induction but gets you there.