Subgoal

Tools: Rocq (formerly Coq)

• (Formal system, Proof/Reason technique, Logic) A subsidiary goal generated when a proof splits into multiple cases, each requiring independent proof before the original Goal is resolved.
• (Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) In Rocq, a derived goal created when a Tactic splits the proof into multiple obligations (e.g., one per constructor or conjunct), all of which must be discharged.