The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have some tactics that make complicated definitions, which I'd like to pass through [simpl] and some other simplification mechanisms before storing.  Currently, I have the following code (which mostly comes from Adam):

Set Implicit Arguments.

Section sig.

  Definition sigT2_sigT A P Q (x : @sigT2 A P Q) := let (a, h, _) := x in existT _ a h.

  Global Coercion sigT2_sigT : sigT2 >-> sigT.

  Definition projT3 A P Q (x : @sigT2 A P Q) :=

    let (x0, _, h) as x0 return (Q (projT1 x0)) := x in h.

  Definition sig2_sig A P Q (x : @sig2 A P Q) := let (a, h, _) := x in exist _ a h.

  Global Coercion sig2_sig : sig2 >-> sig.

  Definition proj3_sig A P Q (x : @sig2 A P Q) :=

    let (x0, _, h) as x0 return (Q (proj1_sig x0)) := x in h.

End sig.

Lemma sigT_eta : forall A (P : A -> Type) (x : sigT P),

  x = existT _ (projT1 x) (projT2 x).

  destruct x; reflexivity.

Qed.

Lemma sigT2_eta : forall A (P Q : A -> Type) (x : sigT2 P Q),

  x = existT2 _ _ (projT1 x) (projT2 x) (projT3 x).

  destruct x; reflexivity.

Qed.

Lemma sig_eta : forall A (P : A -> Prop) (x : sig P),

  x = exist _ (proj1_sig x) (proj2_sig x).

  destruct x; reflexivity.

Qed.

Lemma sig2_eta : forall A (P Q : A -> Prop) (x : sig2 P Q),

  x = exist2 _ _ (proj1_sig x) (proj2_sig x) (proj3_sig x).

  destruct x; reflexivity.

Qed.

(* Silly predicate that we can use to get Ltac to help us manipulate terms *)

Definition focus A (_ : A) := True.

(* This definition does most of the work of simplification. *)

Ltac simpl_definition_by_tac_and_exact defn tac :=

  assert (Hf : focus defn) by constructor;

    try unfold defn in Hf; try tac; simpl in Hf;

      repeat match type of Hf with

               | context[match ?E with existT2 _ _ _ => _ end] => rewrite (sigT2_eta E) in Hf; simpl in Hf

               | context[match ?E with exist2 _ _ _ => _ end] => rewrite (sig2_eta E) in Hf; simpl in Hf

               | context[match ?E with existT _ _ => _ end] => rewrite (sigT_eta E) in Hf; simpl in Hf

               | context[match ?E with exist _ _ => _ end] => rewrite (sig_eta E) in Hf; simpl in Hf

             end;

      match type of Hf with

        | focus ?V => exact V

      end.

Ltac simpl_definition_by_exact defn := simpl_definition_by_tac_and_exact defn idtac.

(** To simplify something defined as [Ident'] of type [IdentT] into [Ident], do something like:

Definition Ident'' : IdentT.

  simpl_definition_by_exact Ident'.

Defined.

(* Then we clean up a bit with reduction. *)

Definition Ident := Eval cbv beta iota zeta delta [Ident''] in Ident''.

*)

I have two questions:

(1) Is there a way to automate the last two steps, either by macros or Ltac or whatever, so that I can run something like

Simpl Definition Ident := Ident'.

or

Definition Ident := Eval simpl_definition in Ident'

and have it expand this to what's commented out above?

(2) Is there a way to simplify types?  That is, say I have a type [fooT], and I've defined [foo] to be 

[Definition foo : fooT := ...]

is there a way to define [foo' := foo] so that [pose foo' as H] is the same as [pose foo as H; unfold fooT in H]?

I've tried

Definition fooT' := nat.

Definition fooT := fooT'.

Parameter bar : fooT.

Definition bar' := bar.

Definition foo := bar'.

Definition foo' := Eval compute in foo.

Definition foo'' := Eval cbv beta iota zeta delta [foo fooT] in foo.

Print foo'.

Print foo''.

but neither works when [bar] is opaque.  (Yes, I realize that I can do [Check foo], copy/paste the output to run [Eval simpl in _], and then copy/paste the output of that to [Definition foo' : _ := foo] (where I fill in the underscore by hand.)  I'm looking for a way to do this in an automated fashion.

The closest I've come is

Set Implicit Arguments.

Section typeof.

  Let typeof (A : Type) (a : A) := A.

  Let foo''T := Eval simpl in typeof foo''.

  Let foo''T' := Eval cbv beta iota delta [typeof foo''T fooT] zeta in foo''T.

  Definition foo''' : foo''T' := Eval unfold foo'' in foo''.

End typeof.

Print foo'''.

but this leaves an extra [let foo''T' := fooT' in ] that it would be nice to remove.

Thanks.

-Jason