The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Are there any good tools (Ltac scripts, plugins, etc.) for manipulating proof trees, and, in particular, splitting them into separate definitions, some of which are made opaque by [abstract] or [Qed]?  For example, if I have a definition with many terms [pf] of type [P : Prop], I would like to abstract away these terms into other theorems, which take as arguments anything that is free in the _expression_ [pf] (but not any expressions involving such terms).  More concretely, I would like to [abstract] away the [FooC] terms in the following:

Record Foo (t : Type) :=

  {

    FooA :> Type;

    FooB : FooA -> FooA -> Type;

    FooC : forall a b (m : FooB a b), m = m /\ t = t

  }.

Record Bar (t : Type) (f g : Foo t) :=

  {

    BarA :> FooA f -> FooA g;

    BarB : forall s d (m : FooB f s d), FooB g (BarA s) (BarA d);

    BarC : forall s d m, @BarB s d m = @BarB s d m /\ f = f

  }.

Record Baz (t : Type) (C D : Foo t) (f g : Bar C D) :=

  {

    BazA : forall x, FooB D (f x) (g x);

    BazB : forall x, BazA x = BazA x /\ f = f

  }.

Definition FooBar t (C D : Foo t) : Foo t.

  exists (Bar C D) (@Baz t C D).

  abstract (intros; split; reflexivity).

Defined.

Definition foo t (C : Foo t) : Foo t.

  do 3 apply FooBar; assumption.

Defined.

Definition foo' t (C : Foo t) : Foo t.

  pose (foo C) as f.

  hnf in f.

  unfold FooBar in f.

Thanks in advance.

-Jason