The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You could write your own variant of the split tactic which first applies that lemma and then splits.  Or you can restructure the theorems to have the useful hypotheses available.  Or prove separate lemmas for L and R, so whichever you prove first is available to the other one.

-Jason

On Dec 24, 2013 5:38 PM, "Christopher Ernest Sally" <christopherernestsally AT gmail.com> wrote:

Yes, indeed. However that doesn't quite suit my purposes as I won't know in what order the students will want to prove the goals, and so even if I prove that family of lemmas (for different arity and order) I wouldn't know which to apply.

I just wanted to confirm 

On 25 December 2013 06:31, Jason Gross <jasongross9 AT gmail.com> wrote:

It should be easy to prove a lemma "L /\ (L -> R) -> L /\ R".  Then you can just apply this lemma before you split.  (You can prove similar lemmas for other numbers of goals.)

-Jason

On Dec 24, 2013 4:58 PM, "Christopher Ernest Sally" <christopherernestsally AT gmail.com> wrote:

Hi all

Say I have some goal of the form Hyp1 -> Hyp2 -> Hyp3 -> L /\ R and I split and then prove L. Now I have Hyp1-3 above the bar, is there any simple way to add L to the current context?

More generally, if I have several sub-goals g_1, g_2 ... g_n, how can I add a g_i to the context once I prove it?

I know this is being slightly troublesome, and normally I would not bother, only. I'm trying to write some material intended for freshmen and hence can't expose too much of Coq's inner workings to them.

Warm regards
Chris