The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi Jason,

In Mtac [1] you can do that, with dependent types and everything. Here
is an even sillier example illustrating the point:

---
Require Import mtac.

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
                   exist _ (S n') (f_equal S H)
       end.

Definition NotFixException : Exception.
  exact exception.
Qed.

Definition deconstruct P (f : forall n : nat, {n' : nat | P n n'}) : M
(nat -> nat) :=
  mmatch f with
  | [(zp : P 0 0) (sp : forall n n', P n n' -> P (S n) (S n'))]
    fix silly (n : nat) : {n' : nat | P n n'} :=
    match n as n0 return {n' : nat | P n0 n'} with
      | 0 => exist (fun n'=>P 0 n') 0 zp
      | S n0 =>
        let (n', H) := silly n0 in
          exist _ (S n') (sp n0 n' H)
    end
   =>
      ret (fix silly (n : nat) :=
       match n  with
         | 0 => 0
         | S n0 => let n' := silly n0 in
                   S n'
       end)
   | _ => raise NotFixException
   end.

Definition silly_helper := run (deconstruct _ silly).

Print silly_helper.

(*

silly_helper =
fix silly (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n0 => let n' := silly n0 in S n'
  end
     : nat -> nat

*)
---

Notice that the proofs for the base and the inductive case are
abstracted in the pattern.

Let me know if you have any questions.

Best,

Beta

[1] www.mpi-sws.org/~beta/mtac




On Sun, May 19, 2013 at 11:16 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> I think my message may not have made it to coq-club, because I pasted too
> much code into it.  Sorry for any duplication.  Here is my reply:
>
> I have not yet timed the performance, so my worries may not be valid.  What
> I am worried about is as much, if not more, the size of the type of the
> proof terms as it is the size of the proof terms themselves.  I already use
> the abstract command, but thanks.
>
> The problem with the Extraction command is that Ocaml is not dependently
> typed.  I gave up on writing the computational parts of my fixpoint by hand
> because of problems with dependently-typed matches.
>
> -Jason
>
>
> On Sat, May 18, 2013 at 7:00 PM, AUGER Cédric 
> <sedrikov AT gmail.com>
>  wrote:
>>
>> 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.
>
>