Stream: Beginner Questions

Topic: How to use the induction hypothesis


view this post on Zulip 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

view this post on Zulip Wenda Li (May 31 2023 at 15:29):

A minimal working example perhaps?


Last updated: Feb 27 2024 at 08:17 UTC