The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have a fixpoint [f] which returns an element of [{ n : T | P n }].  Assuming that [f] does not use anything in [Prop] to construct the element of [T], I want to construct a fixpoint that returns a [T], which is provably equal to [f] on all elements, but which does not involve [P] anywhere.  I would like to do this without copy-paste.  Ideally, I'd like a tactic which manipulates the fixpoint and spits out an appropriate alternative definition.

For example, I'd like to be able to do something like

Fixpoint silly (n : nat) : { n' : nat | n = n' }

    := match n as n0 return {n' : nat | n0 = n'} with

         | 0 => exist _ 0 eq_refl

         | S n0 => let (n', H) := silly n0 in

                   match n' as n' return _ -> _ with

                     | 0 => fun _ => exist _ (S n0) eq_refl

                     | S n'' => fun H' =>  exist _ (S (S n'')) (f_equal S H')

                   end H

       end.

Definition silly_helper (n : nat) : nat.

  deconstruct_fix_point_tactic (silly n).

Defined.

Arguments silly_helper / .

Definition less_silly := Eval simpl in silly_helper.

Print less_silly. (* less_silly = 

fix silly_helper (n : nat) : nat :=

  match n with

  | 0 => 0

  | S n0 =>

      match silly_helper n0 with

      | 0 => S n0

      | S n'' => S (S n'')

      end

  end

     : nat -> nat *)

Or, alternatively, (* less_silly = 

fix silly_helper (n : nat) : nat :=

  match n with

  | 0 => 0

  | S n0 =>

      match silly_helper return True -> _ with

      | 0 => S n0

      | S n'' => S (S n'')

      end I

  end

     : nat -> nat *)

The reason I want to do this is because my actual fixpoint has fairly large proof terms (and types of proof terms), and I would like to speed up simplifying through this fixpoint, so that Coq doesn't have to deal with the proof terms.

Thanks,

Jason