The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Isn't it bad practice for the provability of a conjunct to be dependent on the order in which the conjuncts are proved?

Regards,
Jeff.

On 24 Dec 2013, at 22:40, Christopher Ernest Sally wrote:

Thanks троль and Jason.

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 that there's no easy way to do this (didn't find anything in the reference manual). I guess I'll try to write a tactic.

Best

Chris

On 25 December 2013 06:38, 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