Stream: Beginner Questions

Topic: How to use the induction hypothesis

Hongjian Jiang (May 31 2023 at 13:08):

To prove some lemma, I use the induct tactic. The base is accepts (multi A m vs) w ⟹ ∃us. Ball (set us) (accepts A) ∧ w = concat us ∧ length us = m, and now I have accepts (multi A m vs) v. Could I get the conclusion of ∃us. Ball (set us) (accepts A) ∧ v = concat us ∧ length us = m

proof (prove)
using this:
accepts (multi A m vs) v
accepts (multi A m vs) w ⟹ ∃us. Ball (set us) (accepts A) ∧ w = concat us ∧ length us = m

goal (1 subgoal):

1. ∃us. Ball (set us) (accepts A) ∧ v = concat us ∧ length us = m

Wenda Li (May 31 2023 at 15:29):

A minimal working example perhaps?

Last updated: Apr 28 2024 at 08:19 UTC