The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Hello,
  Seeing the messages about proof layouts, here is a somewhat tangentially
related suggestion. When doing a rewrite, say we have a rewrite
rule of the form
lemma1 : forall x y z, A -> B -> (C=D)

then say we have a goal H1 ... Hn |- G and we want to do
Rewrite lemma1. This gives a new goal
H1, ..., Hn |- G'  (with C replaced by D in G', variables x y z unified...)
plus sub-goals A and B (depending on the x y z).

Mathematically, it suffices to prove
H1, ..., Hn, A, B |- G' 
and the subgoals A and B.

Could we get a tactic to do this? 

That might be useful as an automatic way of 
avoiding multiple branches where one keeps on
proving the same thing.  

Somewhat similarly, when doing Apply lemma2
with
lemma2: forall ..., A -> B -> C -> D

to a goal H1, ..., Hn |- G
it could solve G by unifying D, then give back subgoals

H1, ..., Hn |- A
H1, ..., Hn, A |- B
H1, ..., Hn, A, B |- C.

---Carlos Simpson