The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here is some code which, I believe, should work, taken (nd cleaned up a bit) from my development at https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/Common.v?at=default.

Ltac split_in_context ident funl funr :=
  repeat match goal with
           | [ H : context p [ident] |- _ ] =>
             let H0 := context p[funl] in let H0' := (eval cbv beta in H0) in assert H0' by apply H;
             let H1 := context p[funr] in let H1' := (eval cbv beta in H1) in assert H1' by apply H;
             clear H
         end.

Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a).

Ltac split_and' :=
  repeat match goal with
           | [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in
             assert (H0 := proj1 H); assert (H1 := proj2 H); clear H
         end.
Ltac split_and := split_and'; split_in_context and (fun a b : Prop => a) (fun a b : Prop => b).

-Jason

On Mon, Jun 17, 2013 at 5:16 AM, Math Prover <mathprover AT gmail.com> wrote:

Hi,

  I want to destruct a "scoped and". See attached tac.v

  My existing implementation is somewhat ugly -- for each length, I need to create (a) two lemmas and (b) an extra line in the tactic.

  I was wondering if there was a simpler way to do this in "one shot"