The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 18 May 2013 18:10:57 -0400,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> 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

I am not sure of what you want to do. When I mix proofs and fixpoints,
I use refine tactic to give the computational structure of the proofs
and put wildcards in the term where there should be proofs.
Then for each wildcard Coq asks me to fill in, I first assert all
required calls to the fixpoint "assert (Hx := <my fixpoint>
args).", then clear all non needed hypothesis (including the fixpoint),
and then do a one shot proof inside an abstract (well in fact, I first
do the proof, then add all the control using ";" for sequence of
scripts, "[, |, ]" for parallel scripts, and "(, )" to group scripts.
Once I have all the proof in one tactic, I use the "abstract" tactic
on it).

With abstract, you will have all proof related stuff in your fixpoint
set as opaque, so coq will have little to deal with the proof terms.

Note that you need to correctly clear your hypothesis (forgetting to
remove the fixpoint will lead to unguarded form, and you also have to
keep in mind that all hypothesis, even the uneeded one will be passed
to the abstracted proof).
==============================
Some other interesting stuff for you may be to use the Extraction
command. It extracts to Ocaml, but the syntax is a lot like Coq's one,
so you could copy-paste it.