Bad performance

[Flavio L. C. de Moura]

Hi there,

        I am trying to implement the extended euclidean algorithm in Coq. It
receives two naturals a b and returns gcd(a,b) and the number of
operations (divisions) performed. The problem is that it is performing
very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
for instance, the machine blocks. Any help is very much appreciated. The
code is as follows:

Inductive div_t := div : nat -> nat -> div_t.

Definition div_measure (d : div_t) :=
  match d with
    div _ b => b
  end.

Program Fixpoint div_ext_aux (d : div_t) {measure div_measure d} : nat *
nat :=
match d with
| div a b => if eq_nat_dec 0 b
             then (a,0)
             else let (r, s) := div_ext_aux (div b (mod a b)) in (r, S
s)
end.
Next Obligation.
apply mod_lt. apply neq_O_lt.
assumption.
Qed.

Eval compute in (div_ext_aux (div 4 1)).
Eval compute in (div_ext_aux (div 4 2)).
Eval compute in (div_ext_aux (div 4 3)).
Eval compute in (div_ext_aux (div 4 4)).
Eval compute in (div_ext_aux (div 5 1)).
Eval compute in (div_ext_aux (div 5 2)).
Eval compute in (div_ext_aux (div 5 3)).
Eval compute in (div_ext_aux (div 6 2)).
Eval compute in (div_ext_aux (div 6 3)).
(* Stucks here *)
Eval compute in (div_ext_aux (div 6 4)).


Best regards,

Flavio.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Koprowski]

  Dear Flavio,

  Just from a quick glance, two suggestions:

• Try [vm_compute] instead of [compute], it should be more efficient,
• Please note that you are using [nat] which uses unary notation. If you are serious about performance consider binary natural numbers: http://coq.inria.fr/stdlib/Coq.NArith.BinNat.html.

  Best,

   Adam

2009/11/3 Flávio Leonardo Cavalcanti de Moura <flaviomoura@...>

Hi there,

       I am trying to implement the extended euclidean algorithm in Coq. It
receives two naturals a b and returns gcd(a,b) and the number of
operations (divisions) performed. The problem is that it is performing
very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
for instance, the machine blocks. Any help is very much appreciated. The
code is as follows:

Inductive div_t := div : nat -> nat -> div_t.

Definition div_measure (d : div_t) :=
 match d with
   div _ b => b
 end.

Program Fixpoint div_ext_aux (d : div_t) {measure div_measure d} : nat *
nat :=
match d with
| div a b => if eq_nat_dec 0 b
            then (a,0)
            else let (r, s) := div_ext_aux (div b (mod a b)) in (r, S
s)
end.
Next Obligation.
apply mod_lt. apply neq_O_lt.
assumption.
Qed.

Eval compute in (div_ext_aux (div 4 1)).
Eval compute in (div_ext_aux (div 4 2)).
Eval compute in (div_ext_aux (div 4 3)).
Eval compute in (div_ext_aux (div 4 4)).
Eval compute in (div_ext_aux (div 5 1)).
Eval compute in (div_ext_aux (div 5 2)).
Eval compute in (div_ext_aux (div 5 3)).
Eval compute in (div_ext_aux (div 6 2)).
Eval compute in (div_ext_aux (div 6 3)).
(* Stucks here *)
Eval compute in (div_ext_aux (div 6 4)).


Best regards,

Flavio.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
=====================================================
Adam.Koprowski@..., http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[Guillaume Melquiond-3]

Flávio Leonardo Cavalcanti de Moura a écrit :

> I am trying to implement the extended euclidean algorithm in Coq. It
> receives two naturals a b and returns gcd(a,b) and the number of
> operations (divisions) performed. The problem is that it is performing
> very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
> for instance, the machine blocks. Any help is very much appreciated. The
> code is as follows:

If you intend to compute in Coq, never use things that carry proof
terms. In your case, "eq_nat_dec" and "measure" are the culprits. The
first one can be replaced by beq_nat, the second one by a structural
induction.

For instance, the attached code (lightly tested, so possibly wrong)
answers instantly, even without using vm_compute.

Best regards,

Guillaume

Require Import Arith.

Section Mod.

Variable d : nat.

Fixpoint mod_aux a b c : nat :=
  match a, b with
  | O, O => O
  | O, S _ => c
  | S a, O => mod_aux a d (S a)
  | S a, S b => mod_aux a b c
  end.

End Mod.

Definition mod a b :=
  match b with
  | O => O
  | S b => mod_aux b a (S b) a
  end.

Fixpoint div_ext_aux a b c : nat * nat :=
  match c with
  | O => (0, 0)
  | S c =>
    if beq_nat 0 b then (a, 0)
    else let (r, s) := div_ext_aux b (mod a b) c in (r, S s)
  end.

Definition div_ext a b := div_ext_aux a b (a + b).

Eval compute in (div_ext 2143 513).

[Flavio L. C. de Moura]

Hi Guillaume,

        Thanks a lot for the information.

Flávio.


Em Ter, 2009-11-03 às 18:04 +0100, Guillaume Melquiond escreveu:

> Flávio Leonardo Cavalcanti de Moura a écrit :
>
> > I am trying to implement the extended euclidean algorithm in Coq. It
> > receives two naturals a b and returns gcd(a,b) and the number of
> > operations (divisions) performed. The problem is that it is performing
> > very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
> > for instance, the machine blocks. Any help is very much appreciated. The
> > code is as follows:
>
> If you intend to compute in Coq, never use things that carry proof
> terms. In your case, "eq_nat_dec" and "measure" are the culprits. The
> first one can be replaced by beq_nat, the second one by a structural
> induction.
>
> For instance, the attached code (lightly tested, so possibly wrong)
> answers instantly, even without using vm_compute.
>
> Best regards,
>
> Guillaume
> anexo documento somente texto (div.v)
> Require Import Arith.
>
> Section Mod.
>
> Variable d : nat.
>
> Fixpoint mod_aux a b c : nat :=
>   match a, b with
>   | O, O => O
>   | O, S _ => c
>   | S a, O => mod_aux a d (S a)
>   | S a, S b => mod_aux a b c
>   end.
>
> End Mod.
>
> Definition mod a b :=
>   match b with
>   | O => O
>   | S b => mod_aux b a (S b) a
>   end.
>
> Fixpoint div_ext_aux a b c : nat * nat :=
>   match c with
>   | O => (0, 0)
>   | S c =>
>     if beq_nat 0 b then (a, 0)
>     else let (r, s) := div_ext_aux b (mod a b) c in (r, S s)
>   end.
>
> Definition div_ext a b := div_ext_aux a b (a + b).
>
> Eval compute in (div_ext 2143 513).

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Flavio L. C. de Moura]

Hi Adam,


Thank you!


Em Ter, 2009-11-03 às 17:46 +0100, Adam Koprowski escreveu:

>
>
>   Dear Flavio,
>
>
>   Just from a quick glance, two suggestions:
>       * Try [vm_compute] instead of [compute], it should be more
>         efficient,
>       * Please note that you are using [nat] which uses unary
>         notation. If you are serious about performance consider binary
>         natural
>         numbers: http://coq.inria.fr/stdlib/Coq.NArith.BinNat.html.
>   Best,
>    Adam
>
> 2009/11/3 Flávio Leonardo Cavalcanti de Moura <flaviomoura@...>
>         Hi there,
>        
>                I am trying to implement the extended euclidean
>         algorithm in Coq. It
>         receives two naturals a b and returns gcd(a,b) and the number
>         of
>         operations (divisions) performed. The problem is that it is
>         performing
>         very badly: we can hardly compute the function to 6 and 3. For
>         6 and 4,
>         for instance, the machine blocks. Any help is very much
>         appreciated. The
>         code is as follows:
>        
>         Inductive div_t := div : nat -> nat -> div_t.
>        
>         Definition div_measure (d : div_t) :=
>          match d with
>            div _ b => b
>          end.
>        
>         Program Fixpoint div_ext_aux (d : div_t) {measure div_measure
>         d} : nat *
>         nat :=
>         match d with
>         | div a b => if eq_nat_dec 0 b
>                     then (a,0)
>                     else let (r, s) := div_ext_aux (div b (mod a b))
>         in (r, S
>         s)
>         end.
>         Next Obligation.
>         apply mod_lt. apply neq_O_lt.
>         assumption.
>         Qed.
>        
>         Eval compute in (div_ext_aux (div 4 1)).
>         Eval compute in (div_ext_aux (div 4 2)).
>         Eval compute in (div_ext_aux (div 4 3)).
>         Eval compute in (div_ext_aux (div 4 4)).
>         Eval compute in (div_ext_aux (div 5 1)).
>         Eval compute in (div_ext_aux (div 5 2)).
>         Eval compute in (div_ext_aux (div 5 3)).
>         Eval compute in (div_ext_aux (div 6 2)).
>         Eval compute in (div_ext_aux (div 6 3)).
>         (* Stucks here *)
>         Eval compute in (div_ext_aux (div 6 4)).
>        
>        
>         Best regards,
>        
>         Flavio.
>        
>         --------------------------------------------------------
>         Bug reports: http://logical.saclay.inria.fr/coq-bugs
>         Archives: http://pauillac.inria.fr/pipermail/coq-club
>                  http://pauillac.inria.fr/bin/wilma/coq-club
>         Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>
>
> --
> =====================================================
> Adam.Koprowski@..., http://www.cs.ru.nl/~Adam.Koprowski
> The difference between impossible and possible
> lies in determination (Tommy Lasorda)
> =====================================================
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Matthieu Sozeau]

Hi,

Le 3 nov. 09 à 11:39, Flávio Leonardo Cavalcanti de Moura a écrit :

> Hi there,
>
> I am trying to implement the extended euclidean algorithm in Coq. It
> receives two naturals a b and returns gcd(a,b) and the number of
> operations (divisions) performed. The problem is that it is performing
> very badly: we can hardly compute the function to 6 and 3. For 6 and  
> 4,
> for instance, the machine blocks. Any help is very much appreciated.  
> The
> code is as follows:
>
> Inductive div_t := div : nat -> nat -> div_t.
>
> Definition div_measure (d : div_t) :=
>  match d with
>    div _ b => b
>  end.
>
> Program Fixpoint div_ext_aux (d : div_t) {measure div_measure d} :  
> nat *
> nat :=
> match d with
> | div a b => if eq_nat_dec 0 b
>             then (a,0)
>             else let (r, s) := div_ext_aux (div b (mod a b)) in (r, S
> s)
> end.
> Next Obligation.
> apply mod_lt. apply neq_O_lt.
> assumption.
> Qed.

This obligation should be made transparent with [Defined] instead of  
[Qed],
otherwise only the [lazy beta zeta delta iota] reduction strategy will  
be
fast enough. Apparently the way the fixpoint operator is used in v8.2  
makes
the computation very dependent on the opacity of the proof for the  
recursive
call. This combinator changed since then and in the current trunk  
[compute]
works fast even if you make the obligation opaque.

BTW, I'm not sure this definition is right.

-- Matthieu

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

(* I tested my small hack in coq to have "sexy" records on your problem,
    so if you want them, I can send it, else you will have
    to use the constructor instead.

interesting points:
*use of extraction
*use of Function instead of Program

  *)

Require Import Arith.
Require Euclid.

Record positive :=
{ val : nat;
   pos : val > 0
}.

Record result (m : nat) (n : positive) :=
{ quo : nat;
   rem : nat;
   mod_rel : m = quo * n.(val) + rem;
   sort_rel : n.(val) > rem
}.

Record result_int (n : positive) (m aq ar : nat) :=
{ quo_int : nat;
   corem : nat;
   comod_rel : m + corem + aq * n.(val) = ar + quo_int * n.(val);
   sort_rel_int : n.(val) > corem
}.

Lemma pos_pred : forall n, n.(val) > pred (n.(val)).
Proof.
   destruct n as [v p]; destruct v;
   [destruct (lt_n_O _ p)
   |apply le_n].
Qed.

Lemma Heq : forall k r aq n q,
  k + r + S aq * val n = pred (val n) + q * val n ->
S k + r + aq * val n = q * val n.
Proof.
   intros; apply plus_reg_l with (pred n.(val)); simpl;
   rewrite <- plus_n_Sm; rewrite <- plus_Sn_m;
   rewrite <- (S_pred _ _ n.(pos)); rewrite plus_assoc;
   rewrite (plus_comm (val n)); rewrite <- plus_assoc;
   assumption.
Qed.

Definition coeuclid n m aq ar : n.(val)>ar -> result_int n m aq ar.
Proof.
  intros n.
  refine (fix cm m : forall aq ar, n.(val) > ar -> result_int n m aq ar :=
          match m as m0
          return forall aq ar, n.(val) > ar -> result_int n m0 aq ar with
          | O => fun aq ar H =>
                 {|quo_int := aq;
                   corem := ar;
                   comod_rel := refl_equal _;
                   sort_rel_int := H|}
          | S k => fun aq ar =>
                   match ar as a
                   return n.(val)>a -> result_int n (S k) aq a with
                   | O =>
                     fun H =>
                     let (q, r, cmod, rel) := cm k (S aq) (pred n.(val)) _  
in
                     {|quo_int := q; corem := r;
                       comod_rel := _; sort_rel_int := rel|}
                   | S l =>
                     fun H =>
                     let (q, r, cmod, rel) := cm k aq l _ in
                     {|quo_int := q; corem := r;
                       comod_rel := _; sort_rel_int := rel|}
                   end
          end); clear cm.
(*======== previous lemmas are here to have opacity ========*)
exact (pos_pred _).
exact (Heq _ _ _ _ _ cmod).
exact (le_S_n _ _ (le_S _ _ H)).
exact (eq_S _ _ cmod).
Defined. (* but the result must be transparent *)

Lemma mod_lemma1 : forall m n r (cmod : S (m + r + 0) = 0), result m n.
Proof.
   intros; discriminate cmod.
Qed.
Lemma mod_lemma2 :
forall m n q r (cmod : S (m + r + 0) = val n + q * val n) (rel : val n >  
r),
m = q * val n + (val n - S r).
Proof.
   intros; rewrite <- (plus_n_O) in cmod; rewrite plus_n_Sm in cmod;
   apply plus_reg_l with (S r); rewrite plus_assoc; rewrite plus_comm;
   rewrite (plus_comm (S r)); rewrite <- plus_assoc;
   rewrite le_plus_minus_r.
     rewrite (plus_comm (q * n.(val))); assumption.
   exact rel.
Qed.

Definition euclid m n : result m n. (* an alternative of modulo in Arith *)
Proof.
  intros m n.
  destruct (coeuclid n (S m) 0 0 n.(pos)) as [q r cmod rel]; simpl in *.
  destruct q.
(* absurd case *)
  exact (mod_lemma1 _ _ _ cmod).
(**)
  refine ({|quo := q; rem := n.(val) - S r;
            mod_rel := _; sort_rel := _|}).
(* my opaque proofs *)
  refine (mod_lemma2 _ _ _ _ cmod rel).
  exact (lt_minus _ _ rel (lt_O_Sn _)).
Defined. (* with transparent result *)
Print euclid.

Recursive Extraction euclid.
(* extraction can also be useful outside coq *)

Record div_t := div
{ a : nat;
   b : nat
}.

(* useful stuff if you use program:
Require Import Program.

Lemma acc_wf : forall _x a_,
Acc (fun x y : div_t => b x < b y) {| a := _x; b := a_|}.
Proof.
induction a_; split; intros x_ K; destruct x_ as [_y x_].
simpl in *.
destruct (lt_n_O _ K).
destruct IHa_ as [H].
split; intros y L.
simpl in *.
exact (H _ (lt_le_trans _ _ _ L (le_S_n _ _ K))).
Qed.
*)
Require Import Recdef.

Function div_ext_aux (d : div_t) {measure b} : nat *
nat :=
  match le_lt_dec d.(b) 0 with
  | left H => (d.(a), 0)
  | right H => let eucl := euclid d.(a) {|val:=d.(b); pos:=H|} in
               let (r, s) := div_ext_aux {|a := d.(b);
                                           b := eucl.(rem _ _)|} in
               (r, S s)
end.
simpl; intros; apply sort_rel.
Defined.
  (* we have to hope the proof is small enough to be tractable *)

Recursive Extraction div_ext_aux.

Print R_div_ext_aux.
Print R_div_ext_aux_correct.
Print R_div_ext_aux_complete.
Print div_ext_aux.
Print div_ext_aux_terminate.
Print div_ext_aux_F.
Print div_ext_aux_equation.

Definition divext k :=
  iter (div_t -> nat * nat) k div_ext_aux_F (fun _ => (0, 0)).
(* in a way, what guillaume talked about *)

Eval vm_compute in (divext 3 (div 4 3)).
Eval compute in (divext 4 (div 4 4)).
Eval compute in (divext 5 (div 5 1)).
Eval compute in (divext 5 (div 5 2)).
Eval compute in (divext 5 (div 5 3)).
Eval compute in (divext 6 (div 6 2)).
Eval compute in (divext 6 (div 6 3)).
(* no Stucks here *)
Eval compute in (div_ext_aux (div 6 4)).

Eval compute in (div_ext_aux (div 4 3)).
Eval compute in (div_ext_aux (div 4 4)).
Eval compute in (div_ext_aux (div 5 1)).
Eval compute in (div_ext_aux (div 5 2)).
Eval compute in (div_ext_aux (div 5 3)).
Eval compute in (div_ext_aux (div 6 2)).
Eval compute in (div_ext_aux (div 6 3)).
(* no Stucks here *)
Eval compute in (div_ext_aux (div 6 4)).

Eval compute in (div_ext_aux (div 125 35)).

Le Tue, 03 Nov 2009 19:43:02 +0100, Matthieu Sozeau <mattam@...> a  
écrit:

> Hi,
>
> Le 3 nov. 09 à 11:39, Flávio Leonardo Cavalcanti de Moura a écrit :
>
>> Hi there,
>>
>> I am trying to implement the extended euclidean algorithm in Coq. It
>> receives two naturals a b and returns gcd(a,b) and the number of
>> operations (divisions) performed. The problem is that it is performing
>> very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
>> for instance, the machine blocks. Any help is very much appreciated. The
>> code is as follows:
>>
>> Inductive div_t := div : nat -> nat -> div_t.
>>
>> Definition div_measure (d : div_t) :=
>>  match d with
>>    div _ b => b
>>  end.
>>
>> Program Fixpoint div_ext_aux (d : div_t) {measure div_measure d} : nat *
>> nat :=
>> match d with
>> | div a b => if eq_nat_dec 0 b
>>             then (a,0)
>>             else let (r, s) := div_ext_aux (div b (mod a b)) in (r, S
>> s)
>> end.
>> Next Obligation.
>> apply mod_lt. apply neq_O_lt.
>> assumption.
>> Qed.
>
> This obligation should be made transparent with [Defined] instead of  
> [Qed],
> otherwise only the [lazy beta zeta delta iota] reduction strategy will be
> fast enough. Apparently the way the fixpoint operator is used in v8.2  
> makes
> the computation very dependent on the opacity of the proof for the  
> recursive
> call. This combinator changed since then and in the current trunk  
> [compute]
> works fast even if you make the obligation opaque.
>
> BTW, I'm not sure this definition is right.
>
> -- Matthieu
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
Utilisant le client e-mail révolutionnaire d'Opera :  
http://www.opera.com/mail/

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

Le Wed, 04 Nov 2009 09:48:16 +0100, Roman Beslik <beroal@...> a écrit:

> It's inconceivable that nobody suggested to export the code into some  
> other language with optimized compiler.

Maybe was my previous mail a bit too long... (or not enough verbose),
but this is not as handy as using the coq toplevel.

>
> Flávio Leonardo Cavalcanti de Moura wrote:
>> Hi there, I am trying to implement the extended euclidean algorithm in  
>> Coq. It
>> receives two naturals a b and returns gcd(a,b) and the number of
>> operations (divisions) performed. The problem is that it is performing
>> very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
>> for instance, the machine blocks.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Roman Beslik-2]

It's inconceivable that nobody suggested to export the code into some
other language with optimized compiler.

Flávio Leonardo Cavalcanti de Moura wrote:
> Hi there,
>
> I am trying to implement the extended euclidean algorithm in Coq. It
> receives two naturals a b and returns gcd(a,b) and the number of
> operations (divisions) performed. The problem is that it is performing
> very badly: we can hardly compute the function to 6 and 3. For 6 and 4,
> for instance, the machine blocks.
--
Best regards,
  Roman Beslik.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

Hi, all

Would it be a good idea to have a coq version-independant compiler?

That is just the output of a "Print All.", so that we could have a  
/theories directory in which only type checking has to be done and a  
directory /theories_src which is the actual directory, so recompiling  
proof will only type-check without constructing proofs and without having  
the problems of the versions of the .vo files?

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Chlipala-3]

Roman Beslik wrote:
> It's inconceivable that nobody suggested to export the code into some
> other language with optimized compiler.

At least for larger inputs, this might not help appreciably; the
algorithm will still run approximately "forever," because it will use
unary natural numbers.  You need some extensions to extraction to assure
that this doesn't happen; in particular, you need to compile
pattern-matches over [nat]s in a way that is compatible with using a
more efficient representation of [nat].  Maybe this example doesn't need
pattern-matching, so it would be fine, but simply extracting isn't
always a guarantee of improved asymptotic performance.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Mathieu Boespflug-2]

Hi,

2009/11/4 Roman Beslik <beroal@...>:
> It's inconceivable that nobody suggested to export the code into some other
> language with optimized compiler.

That's exactly the idea behind Dedukti [1], where proofs are compiled
to native code. A translation for Coq proofs to Dedukti isn't
finalized yet, but stay tuned. That being said, Coq already has
facilities to improve the speed of computation, such as compiling to
byte-code using vm_compute, as pointed out elsewhere in this thread.

[1] http://www.lix.polytechnique.fr/dedutki

-- Mathieu

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[greenrd]

Not Found
The requested URL /dedutki was not found on this server.

--
Robin

At Wed, 4 Nov 2009 21:31:25 +0100,
Mathieu Boespflug wrote:

>
> Hi,
>
> 2009/11/4 Roman Beslik <beroal@...>:
> > It's inconceivable that nobody suggested to export the code into some other
> > language with optimized compiler.
>
> That's exactly the idea behind Dedukti [1], where proofs are compiled
> to native code. A translation for Coq proofs to Dedukti isn't
> finalized yet, but stay tuned. That being said, Coq already has
> facilities to improve the speed of computation, such as compiling to
> byte-code using vm_compute, as pointed out elsewhere in this thread.
>
> [1] http://www.lix.polytechnique.fr/dedutki
>
> -- Mathieu
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[André Hirschowitz]

Robin Green a écrit :
> Not Found
> The requested URL /dedutki was not found on this server.
>
>  
I deduce that it should be dedukti

ah

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

I am not expert on coercions, so what I ask may be stupid, else I'll send  
a feature request.

Why must coercions be identifier?
>>>

Record bijection {A B} := Bij
{ proj : A -> B;
   lift : B -> A;
   idA : forall a, lift (proj a) = a;
   idB : forall b, proj (lift b) = b
}.

Module Type ProgramStructure.
   Parameter bit : Type.
   Parameter quart : Type.
   Parameter byte : Type.
   Parameter word : Type.
   Parameter longword : Type.

   Record merge2 A :=
   { strong : A;
     weak   : A
   }.

   Definition bitbit := merge2 bit.
   Definition quartquart := merge2 quart.
   Definition bytebyte := merge2 byte.
   Definition wordword := merge2 word.

   Parameter bitbit_bij : @bijection quart bitbit.
   Parameter quartquart_bij : @bijection byte quartquart.
   Parameter bytebyte_bij : @bijection word bytebyte.
   Parameter wordword_bij : @bijection longword wordword.

   Definition bitbit2quart := bitbit_bij.(lift).
   Definition quart2bitbit := bitbit_bij.(proj).
   Coercion bitbit2quart : bitbit >-> quart.
   Coercion quart2bitbit : quart >-> bitbit.
  ....
>>>
A lot more convenient would be to do:
>>>


Record bijection {A B} := Bij
{ proj : A -> B;
   lift : B -> A;
   idA : forall a, lift (proj a) = a;
   idB : forall b, proj (lift b) = b
}.

Module Type ProgramStructure.
   Parameter bit : Type.
   Parameter quart : Type.
   Parameter byte : Type.
   Parameter word : Type.
   Parameter longword : Type.

   Record merge2 A :=
   { strong : A;
     weak   : A
   }.

   Parameter bitbit_bij : @bijection quart bitbit.
   Parameter quartquart_bij : @bijection byte quartquart.
   Parameter bytebyte_bij : @bijection word bytebyte.
   Parameter wordword_bij : @bijection longword wordword.

   Coercion bitbit_bij.(lift) : merge2 bit >-> quart.
   Coercion bitbit_bij.(proj) : quart >-> merge2 bit.
...

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Vladimir Voevodsky]

Is there an easy way to get a fully expanded proof term for one of the  
standard library lemmas? (e.g. for mult_comm?)

I need it as an illustration for a talk.

Thanks!
V.





--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Chlipala-3]

Vladimir Voevodsky wrote:
> Is there an easy way to get a fully expanded proof term for one of the
> standard library lemmas? (e.g. for mult_comm?)

Yes; just run:

Set Printing All.
Print mult_comm.

(The first line may be omittable, depending on your definition of "fully
expanded.")

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Vladimir Voevodsky]

This I tried. I want to show how it looks like when all the  
definitions are expanded all the way down to the CIC.
V.

On Nov 13, 2009, at 11:20 AM, Yves Bertot wrote:

> Vladimir Voevodsky wrote:
>> Is there an easy way to get a fully expanded proof term for one of  
>> the standard library lemmas? (e.g. for mult_comm?)
>>
>> I need it as an illustration for a talk.
>>
>> Thanks!
>> V.
>>
>>
>>
>>
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>        http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> Print mult_comm.
>
> mult_comm =
> fun n m : nat =>
> nat_ind (fun n0 : nat => n0 * m = m * n0) (mult_n_O m)
> (fun (n0 : nat) (IHn : n0 * m = m * n0) =>
> eq_ind (m * n0 + m) (fun n1 : nat => m + n0 * m = n1)
>   (eq_ind_r (fun n1 : nat => m + n1 = m * n0 + m)
>      (plus_comm m (m * n0)) IHn) (m * S n0) (mult_n_Sm m n0)) n
>   : forall n m : nat, n * m = m * n
>
> should be good enough.
>
> If not, add
>
> Set Printing all.
>
> mult_comm =
> fun n m : nat =>
> nat_ind (fun n0 : nat => @eq nat (mult n0 m) (mult m n0))
> (mult_n_O m)
> (fun (n0 : nat) (IHn : @eq nat (mult n0 m) (mult m n0)) =>
> @eq_ind nat (plus (mult m n0) m)
>   (fun n1 : nat => @eq nat (plus m (mult n0 m)) n1)
>   (@eq_ind_r nat (mult m n0)
>      (fun n1 : nat => @eq nat (plus m n1) (plus (mult m n0) m))
>      (plus_comm m (mult m n0)) (mult n0 m) IHn)
>   (mult m (S n0)) (mult_n_Sm m n0)) n
>   : forall n m : nat, @eq nat (mult n m) (mult m n)
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[greenrd]

Have you tried

Eval compute in ...

--
Robin

At Fri, 13 Nov 2009 14:06:31 +0100,
Vladimir Voevodsky wrote:

>
> This I tried. I want to show how it looks like when all the  
> definitions are expanded all the way down to the CIC.
> V.
>
> On Nov 13, 2009, at 11:20 AM, Yves Bertot wrote:
>
> > Vladimir Voevodsky wrote:
> >> Is there an easy way to get a fully expanded proof term for one of  
> >> the standard library lemmas? (e.g. for mult_comm?)
> >>
> >> I need it as an illustration for a talk.
> >>
> >> Thanks!
> >> V.
> >>
> >>
> >>
> >>
> >>
> >> --------------------------------------------------------
> >> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> >> Archives: http://pauillac.inria.fr/pipermail/coq-club
> >>        http://pauillac.inria.fr/bin/wilma/coq-club
> >> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> > Print mult_comm.
> >
> > mult_comm =
> > fun n m : nat =>
> > nat_ind (fun n0 : nat => n0 * m = m * n0) (mult_n_O m)
> > (fun (n0 : nat) (IHn : n0 * m = m * n0) =>
> > eq_ind (m * n0 + m) (fun n1 : nat => m + n0 * m = n1)
> >   (eq_ind_r (fun n1 : nat => m + n1 = m * n0 + m)
> >      (plus_comm m (m * n0)) IHn) (m * S n0) (mult_n_Sm m n0)) n
> >   : forall n m : nat, n * m = m * n
> >
> > should be good enough.
> >
> > If not, add
> >
> > Set Printing all.
> >
> > mult_comm =
> > fun n m : nat =>
> > nat_ind (fun n0 : nat => @eq nat (mult n0 m) (mult m n0))
> > (mult_n_O m)
> > (fun (n0 : nat) (IHn : @eq nat (mult n0 m) (mult m n0)) =>
> > @eq_ind nat (plus (mult m n0) m)
> >   (fun n1 : nat => @eq nat (plus m (mult n0 m)) n1)
> >   (@eq_ind_r nat (mult m n0)
> >      (fun n1 : nat => @eq nat (plus m n1) (plus (mult m n0) m))
> >      (plus_comm m (mult m n0)) (mult n0 m) IHn)
> >   (mult m (S n0)) (mult_n_Sm m n0)) n
> >   : forall n m : nat, @eq nat (mult n m) (mult m n)
> >
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

Le Fri, 13 Nov 2009 14:59:46 +0100, Robin Green <greenrd@...> a  
écrit:

> Have you tried
>
> Eval compute in ...
>
I don't recommend the use of this unless you want some computation.
For displaying, just use Print as many said.

For controlled computation, cbv can be very handful:

Eval cbv beta delta [list_ind list_rec list_rect] in ...
will show your function with beta reduction and expanding list induction  
predicates (it is often useful, since keeping them can be too verbose or  
not enough). See the documentation for that, there are more reduction  
rules available (eta and iota, I believe).

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club