The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

See http://coq.inria.fr/distrib/8.4/refman/Reference-Manual011.html#hevea_default743 and  http://coq.inria.fr/distrib/8.4/refman/Reference-Manual011.html#hevea_default753.  Essential, the [p] is turned into a special function, which is evaluated by using the form [let p_on_argument := context p[argument] in ...]; matching on [context p [foo] ] binds [p] to the goal/type/term, with a foo-shaped hole in it.

-Jason

On Mon, Jun 17, 2013 at 11:24 PM, Math Prover <mathprover AT gmail.com> wrote:

Hi Jason,

  Thanks for your detailed response.

  There's one aspect of your code I don't understand: what does "context p" mean?

  I've looked at http://coq.inria.fr/distrib/8.4/refman/Reference-Manual012.html but it's not clear to me what adding an "p" after context does.

Thanks!

On Mon, Jun 17, 2013 at 7:05 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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"