Library additions.Euclidean_Chains

Euclidean chains

Introduction

In this module, we study a way to build efficiently efficient chains. Our approach is recursive (compositional?). Chains associated with big exponents are built by composition of smaller chains. Thus, the construction of a small computation may be parameterized by the context in which it will be used. In other terms, we shall use Continuation Passing Style
Euclidean chains are introduced by

From Coq Require Import Inverse_Image Inclusion Wf_nat
  NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia.
From additions Require Import Addition_Chains Compatibility
  More_on_positive Wf_transparent Dichotomy BinaryStrat.
From Coq Require Import Lia.

Generalizable All Variables.
Import Morphisms.
Import Monoid_def.

Ltac add_op_proper M H :=
 let h := fresh H in
   generalize (@Eop_proper _ _ _ _ M); intro h.

CPS chain construction

Type of chain continuations

Definition Fkont (A:Type) := A → @computation A.

Definition Fchain := ∀ A, Fkont A → A → @computation A.

F3 k x computes , then executes the computation associated with k z

Definition F3 : Fchain :=
 fun A k (x:A) ⇒
  y <--- x times x ;
  z <--- y times x ;
  k z.

Definition F1 : Fchain :=
 fun A k (x:A) ⇒ k x.

Definition F2 : Fchain :=
fun A k (x:A) ⇒
  y <--- x times x ;
  k y.

An Fchain f can be considered as a function that takes as argument another chain c for continueing the computation.

Definition Fapply (f : Fchain) (c: chain) : chain :=
 fun (A:Type) (x: A) ⇒ f A (c A) x.

Definition Fcompose (f1 f2: Fchain) : Fchain :=
 fun A k x ⇒ f1 A (fun y ⇒ f2 A k y) x.

Any Fchain can be transformed into a plain chain

Definition F2C (f : Fchain) : chain :=
 fun (A:Type) ⇒ f A Return .


Composition of Fchains
Fchains are used for building correct exponentiation schemes by composition of correct components. So, we have to define composition of Fchains.

Example F9 := Fcompose F3 F3.


Fchains associated with powers of 2
computes then send this value to
The neutral element for Fcompose

Lemma F1_neutral_l : ∀ f, Fcompose F1 f = f.

Lemma F1_neutral_r : ∀ f, Fcompose f F1 = f.

Fixpoint Fexp2_of_nat (n:nat) : Fchain :=
 match n with O ⇒ F1
            | S p ⇒ Fcompose F2 (Fexp2_of_nat p)
 end.

Definition Fexp2 (p:positive) : Fchain :=
  Fexp2_of_nat (Pos.to_nat p).




Remark F9_correct :chain_correct 9 (F2C F9).


A first attempt to define Fchain correctness

Module Bad.

Definition Fchain_correct (n:nat) (fc : Fchain) :=
  ∀ A `(M : @EMonoid A op E_one E_equiv) k (a:A),
    computation_execute op (fc A k a)==
    computation_execute op (k (a ^ n)).

Theorem F3_correct : Fchain_correct 3 F3. End Bad.


Equivalence on computations

Definition computation_equiv {A:Type} (op: Mult_op A)
           (equiv : Equiv A)
           (c c': @computation A) :=
   computation_execute op c == computation_execute op c'.

#[ global ] Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A):
  Equiv (@computation A) :=
  @computation_equiv A op equiv.

#[ global ] Instance comp_equiv_equivalence {A:Type} (op: Mult_op A)
           (equiv : Equiv A) : Equivalence equiv →
                               Equivalence (computation_equiv op equiv).

Fkonts that respect E_equiv

Class Fkont_proper
      `(M : @EMonoid A op E_one E_equiv) (k: Fkont A ) :=
  Fkont_proper_prf:
    Proper (equiv ==> computation_equiv op E_equiv) k.

#[ global ] Instance Return_proper `(M : @EMonoid A op E_one E_equiv) :
  Fkont_proper M (@Return A).

Fchain correctness (for exponent of type nat

Definition Fchain_correct_nat (n:nat) (f : Fchain) :=
 ∀ A `(M : @EMonoid A op E_one E_equiv) k
        (Hk :Fkont_proper M k)
        (a : A) ,
 computation_execute op (f A k a) ==
 computation_execute op (k (a ^ n)).

Definition Fchain_correct (p:positive) (f : Fchain) :=
 Fchain_correct_nat (Pos.to_nat p) f.

Lemma F1_correct : Fchain_correct 1 F1.

Lemma F3_correct : Fchain_correct 3 F3.
Lemma F2_correct : Fchain_correct 2 F2.

F2C preserves correctness

Lemma F2C_correct (p:positive) (fc : Fchain) :
  Fchain_correct p fc → chain_correct p (F2C fc).

Module Bad2.

Lemma Fcompose_correct :
  ∀ f1 f2 n1 n2,
    Fchain_correct n1 f1 →
    Fchain_correct n2 f2 →
    Fchain_correct (n1 × n2) (Fcompose f1 f2).

End Bad2.

Fisrt attempt to define Fchain_proper

Module Bad3.

Class Fchain_proper (fc : Fchain) := Fchain_proper_bad_prf :
 ∀ `(M : @EMonoid A op E_one E_equiv) k ,
    Fkont_proper M k →
    ∀ x y, x == y →
               @computation_equiv _ op E_equiv
                                  (fc A k x)
                                  (fc A k y).


#[ global ] Instance Fcompose_proper (f1 f2 : Fchain)
         (_ : Fchain_proper f1)
         (_ : Fchain_proper f2) :
  Fchain_proper (Fcompose f1 f2).

End Bad3.

Correct definition

Definition Fkont_equiv `(M : @EMonoid A op E_one E_equiv)
 (k k': Fkont A ) :=
 ∀ x y : A, x == y →
                 computation_equiv op E_equiv (k x) (k' y).

Class Fchain_proper (fc : Fchain) := Fchain_proper_prf :
 ∀ `(M : @EMonoid A op E_one E_equiv) k k' ,
    Fkont_proper M k → Fkont_proper M k' →
    Fkont_equiv M k k' →
   ∀ x y, x == y →
               @computation_equiv _ op E_equiv
                                  (fc A k x)
                                  (fc A k' y).

#[ global ] Instance F1_proper : Fchain_proper F1.

#[ global ] Instance F3_proper : Fchain_proper F3.

#[ global ] Instance F2_proper : Fchain_proper F2.

Fcompose respects correctness and properness

Lemma Fcompose_correct_nat : ∀ fc1 fc2 n1 n2,
                           Fchain_correct_nat n1 fc1 →
                           Fchain_correct_nat n2 fc2 →
                           Fchain_proper fc2 →
                           Fchain_correct_nat (n1 × n2)%nat
                                              (Fcompose fc1 fc2).

Lemma Fcompose_correct :
  ∀ fc1 fc2 n1 n2,
    Fchain_correct n1 fc1 →
    Fchain_correct n2 fc2 →
    Fchain_proper fc2 →
    Fchain_correct (n1 × n2) (Fcompose fc1 fc2).

#[ global ] Instance Fcompose_proper (fc1 fc2: Fchain)
                         (_ : Fchain_proper fc1)
                         (_ : Fchain_proper fc2) :
  Fchain_proper (Fcompose fc1 fc2).

#[ global ] Instance Fexp2_nat_proper (n:nat) :
                           Fchain_proper (Fexp2_of_nat n).

Lemma Fexp2_nat_correct (n:nat) :
                           Fchain_correct_nat (2 ^ n)
                                              (Fexp2_of_nat n).

Lemma Fexp2_correct (p:positive) :
  Fchain_correct (2 ^ p) (Fexp2 p).

#[ global ] Instance Fexp2_proper (p:positive) : Fchain_proper (Fexp2 p).

Remark

We are now able to build chains for any exponent of the form , using Fcompose and previous lemmas.
Let us look at a simple example

#[global] Hint Resolve F1_correct F1_proper
     F3_correct F3_proper Fcompose_correct Fcompose_proper
     Fexp2_correct Fexp2_proper : chains.

Example F144: {f : Fchain | Fchain_correct 144 f ∧
                             Fchain_proper f}.


Bad solution

Module Bad4.

Definition Fplus (f1 f2 : Fchain) : Fchain :=
  fun A k x ⇒ f1 A
                  (fun y ⇒
                     f2 A
                        (fun z ⇒ t <--- z times y; k t) x) x.

Example F23 := Fplus F3 (Fplus (Fexp2 4) (Fexp2 2)).

Lemma F23_ok : chain_correct 23 (F2C F23).



End Bad4.

Continuations with two arguments

Definition Kkont A:= A → A → @computation A.

CPS chain builders for two exponents

Definition Kchain := ∀ A, Kkont A → A → @computation A.


Kchain for and

Example k3_1 : Kchain := fun A (k:Kkont A) (x:A) ⇒
  x2 <--- x times x ;
  x3 <--- x2 times x ;
  k x3 x.


Kchain for and

Example k7_3 : Kchain := fun A (k:Kkont A) (x:A) ⇒
  x2 <--- x times x;
  x3 <--- x2 times x ;
  x6 <--- x3 times x3 ;
  x7 <--- x6 times x ;
  k x7 x3.

The Definition of correct chains and proper chains and continuations are adapted to Kchains

Definition Kkont_proper `(M : @EMonoid A op E_one E_equiv)
           (k : Kkont A) :=
 Proper (equiv ==> equiv ==> computation_equiv op E_equiv) k .

Definition Kkont_equiv `(M : @EMonoid A op E_one E_equiv)
           (k k': Kkont A ) :=
 ∀ x y : A, x == y → ∀ z t, z == t →
         computation_equiv op E_equiv (k x z) (k' y t).

A Kchain is correct with respect to two exponents and if it computes and for every

About EMonoid.

Definition Kchain_correct_nat (n p : nat) (kc : Kchain) :=
  ∀ (A : Type) (op : Mult_op A) (E_one : A) (E_equiv : Equiv A)
          (M : EMonoid op E_one E_equiv)
          (k : Kkont A),
    Kkont_proper M k →
    ∀ (a : A) ,
      computation_execute op (kc A k a) ==
      computation_execute op (k (a ^ n) (a ^ p)).

Definition Kchain_correct (n p : positive) (kc : Kchain) :=
  Kchain_correct_nat (Pos.to_nat n) (Pos.to_nat p) kc.

Class Kchain_proper (kc : Kchain) :=
Kchain_proper_prf :
 ∀ `(M : @EMonoid A op E_one E_equiv) k k' x y ,
   Kkont_proper M k →
   Kkont_proper M k' →
   Kkont_equiv M k k' →
   E_equiv x y →
   computation_equiv op E_equiv (kc A k x) (kc A k' y).

#[ global ] Instance k7_3_proper : Kchain_proper k7_3.

Lemma k7_3_correct : Kchain_correct 7 3 k7_3.

conversion between several definitions of correctness

Lemma Kchain_correct_conv (kc : Kchain) (n p : nat) :
  0%nat ≠ n → 0%nat ≠ p →
  Kchain_correct_nat n p kc →
  Kchain_correct (Pos.of_nat n) (Pos.of_nat p) kc.

More chain combinators

Since we are working with two types of functional chains, we have to define several ways of composing them. Each of these operators is certified to preserve correctnes and properness
Conversion of Kchains into Fchains

Definition K2F (knp : Kchain) : Fchain :=
  fun A (k:Fkont A) ⇒ knp A (fun y _ ⇒ k y).

Lemma K2F_correct_nat :
  ∀ knp n p, Kchain_correct_nat n p knp →
                 Fchain_correct_nat n (K2F knp).

Lemma K2F_correct :
  ∀ kc n p, Kchain_correct n p kc →
                 Fchain_correct n (K2F kc).

#[ global ] Instance K2F_proper (kc : Kchain)(_ : Kchain_proper kc) :
  Fchain_proper (K2F kc).

Using kbr for computing and , then using Cq for computing , then sending and to the continuation

Definition KFK (kbr : Kchain) (fq : Fchain) : Kchain :=
  fun A k a ⇒
    kbr A (fun xb xr ⇒
              fq A (fun y ⇒
                      z <--- y times xr; k z xb) xb) a.

Definition KFF (kbr : Kchain) (fq : Fchain) : Fchain :=
  K2F (KFK kbr fq).

Definition FFK (fp fq : Fchain) : Kchain :=
  fun A k a ⇒ fp A (fun xb ⇒ fq A (fun y ⇒ k y xb) xb) a.

Definition FK (f : Fchain) : Kchain :=
  fun (A : Type) (k : Kkont A) (a : A) ⇒
    f A (fun y ⇒ k y a) a.

Example k17_7 := KFK k7_3 (Fexp2 1).

In the following section, we prove that the constructions KFK and KFF respect properness and correctness

Section KFK_proof.
 Variables b q r: nat.
 Variable kbr : Kchain.
 Variable fq : Fchain.
 Hypothesis Hbr : Kchain_correct_nat b r kbr.
 Hypothesis Hq : Fchain_correct_nat q fq.
 Hypothesis Hbr_prop : Kchain_proper kbr.
 Hypothesis Hq_prop : Fchain_proper fq.

 Lemma KFK_correct_nat : Kchain_correct_nat (b × q + r)%nat b (KFK kbr fq).
simplifying the hypotheses

 Lemma KFF_correct_nat : Fchain_correct_nat (b × q + r)%nat (KFF kbr fq).

Lemma KFK_proper : Kchain_proper (KFK kbr fq).

#[global] Instance KFF_proper : Fchain_proper (KFF kbr fq).

End KFK_proof.
Lemma KFK_correct :
  ∀ (b q r : positive) (kbr : Kchain) (fq : Fchain),
    Kchain_correct b r kbr →
    Fchain_correct q fq →
    Kchain_proper kbr →
    Fchain_proper fq →
    Kchain_correct (b × q + r) b (KFK kbr fq).

Check KFK_proper.

Check KFK_proper.

Lemma KFF_correct :
  ∀ (b q r : positive) (kbr : Kchain) (fq : Fchain),
    Kchain_correct b r kbr →
    Fchain_correct q fq →
    Kchain_proper kbr →
    Fchain_proper fq →
    Fchain_correct (b × q + r) (KFF kbr fq).

Lemma FFK_correct_nat :
  ∀ (p q : nat) (fp fq : Fchain),
    Fchain_correct_nat p fp →
    Fchain_correct_nat q fq →
    Fchain_proper fp →
    Fchain_proper fq → Kchain_correct_nat (p × q) p (FFK fp fq).
simplifying the hypotheses

Lemma FFK_correct (p q : positive) (fp fq : Fchain):
    Fchain_correct p fp →
    Fchain_correct q fq →
    Fchain_proper fp →
    Fchain_proper fq →
    Kchain_correct (p × q ) p (FFK fp fq).

#[ global ] Instance FFK_proper
         (fp fq : Fchain)
         (_ : Fchain_proper fp)
         (_ : Fchain_proper fq)
  : Kchain_proper (FFK fp fq).

Lemma FK_correct : ∀ (p: positive) (Fp : Fchain),
                     Fchain_correct p Fp →
                     Fchain_proper Fp →
                     Kchain_correct p 1 (FK Fp).

#[ global ] Instance FK_proper (Fp : Fchain) (_ : Fchain_proper Fp):
  Kchain_proper (FK Fp).

#[global] Hint Resolve KFF_correct KFF_proper KFK_correct KFK_proper : chains.

Lemma k3_1_correct : Kchain_correct 3 1 k3_1.

Lemma k3_1_proper : Kchain_proper k3_1.

#[global] Hint Resolve k3_1_correct k3_1_proper : chains.

an example of correct chain construction


Definition F87 :=
 let k7_3 := KFK k3_1 (Fexp2 1) in
 let k10_7 := KFK k7_3 F1 in
 KFF k10_7 (Fexp2 3).



Lemma OK87 : Fchain_correct 87 F87.

Ltac compute_chain ch :=
   let X := fresh "x" in
   let Y := fresh "y" in
   let X := constr:(ch) in
   let Y := (eval vm_compute in X)
   in exact Y.

Definition C87' := ltac:( compute_chain C87 ).

Print C87'.

Lemma PF87: parametric C87'.

Automatic generation of correct euclidean chains

We want to define a function that builds a correct chain for any positive exponent, using the previously defined and certified composition operators : Fcompose, KFK, etc.
Obviously, we have to define total mutually recursive functions:
  • A function that builds an Fchain for any positive exponent p
  • A function that builds a Kchain for any pair of exponents (n,p) where
In Coq, various ways of building functions are available:
  • Structural mutual recursion with Fixpoint
  • Using Program Fixpoint
  • Using Function
For simplicity's sake, we chosed to avoid dependent elimination and used Function with a decreasing measure. For this purpose, we define a single data-type for associated with the generation of F- and K-chains.
For specifying the computation of a Kchain for and where , we use the pair of positive numbers , thus avoiding to propagate the constraint in our definitions.


Inductive signature : Type :=
| gen_F (n:positive)
Fchain for the exponent n
| gen_K (p d: positive)
Kchain for the exponents p+d and p
.

Unifying statements about chain generation


Definition signature_exponent (s:signature) : positive :=
 match s with
| gen_F n ⇒ n
| gen_K p d ⇒ p + d
end.

Definition kont_type (s: signature)(A:Type) : Type :=
match s with
| gen_F _ ⇒ Fkont A
| gen_K _ _ ⇒ Kkont A
end.

Definition chain_type (s: signature) : Type :=
 match s with
| gen_F _ ⇒ Fchain
| gen_K _ _ ⇒ Kchain
end.

Definition correctness_statement (s: signature) :
chain_type s → Prop :=
match s with
  | gen_F p ⇒ fun ch ⇒ Fchain_correct p ch
  | gen_K p d ⇒ fun ch ⇒ Kchain_correct (p + d) p ch
end.

Definition proper_statement (s: signature) :
chain_type s → Prop :=
match s with
  | gen_F _ ⇒ fun ch ⇒ Fchain_proper ch
  | gen_K _ _ ⇒ fun ch ⇒ Kchain_proper ch
end.

Full correctness


Definition OK (s: signature)
  := fun c: chain_type s ⇒ correctness_statement s c ∧
                            proper_statement s c.


#[global] Hint Resolve pos_gt_3 : chains.

Section Gamma.
Variable gamma: positive → positive.
Context (Hgamma : Strategy gamma).

Definition signature_measure (s : signature) : nat :=
match s with
  | gen_F n ⇒ 2 × Pos.to_nat n
  | gen_K p d ⇒ 2 × Pos.to_nat (p + d) +1
end.


 Lemma PO1 :∀ (s : signature) (i : positive),
  s = gen_F i →
  ∀ anonymous : i ≠ 1,
  pos_eq_dec i 1 = right anonymous →
  ∀ anonymous0 : i ≠ 3,
  pos_eq_dec i 3 = right anonymous0 →
  exact_log2 i = None →
  ∀ q r : N,
  r = 0%N →
  N.pos_div_eucl i (N.pos (gamma i)) = (q, 0%N) →
  (signature_measure (gen_F (N2pos q)) < signature_measure (gen_F i))%nat.

 Lemma PO2 : ∀ (s : signature) (i : positive),
     s = gen_F i →
     ∀ anonymous : i ≠ 1,
       pos_eq_dec i 1 = right anonymous →
       ∀ anonymous0 : i ≠ 3,
         pos_eq_dec i 3 = right anonymous0 →
         exact_log2 i = None →
         ∀ q r : N,
           r = 0%N →
           N.pos_div_eucl i (N.pos (gamma i)) = (q, 0%N) →
           (signature_measure (gen_F (gamma i)) < signature_measure (gen_F i))%nat.

 Lemma PO3 : ∀ (s : signature) (i : positive),
  s = gen_F i →
  ∀ anonymous : i ≠ 1,
  pos_eq_dec i 1 = right anonymous →
  ∀ anonymous0 : i ≠ 3,
  pos_eq_dec i 3 = right anonymous0 →
  exact_log2 i = None →
  ∀ (q r : N) (p : positive),
  r = N.pos p →
  N.pos_div_eucl i (N.pos (gamma i)) = (q, N.pos p) →
  (signature_measure (gen_F (N2pos q)) < signature_measure (gen_F i))%nat.

 Lemma PO4 : ∀ (s : signature) (i : positive),
  s = gen_F i →
  ∀ anonymous : i ≠ 1,
  pos_eq_dec i 1 = right anonymous →
  ∀ anonymous0 : i ≠ 3,
  pos_eq_dec i 3 = right anonymous0 →
  exact_log2 i = None →
  ∀ (q r : N) (p : positive),
  r = N.pos p →
  N.pos_div_eucl i (N.pos (gamma i)) = (q, N.pos p) →
  (signature_measure (gen_K (N2pos (N.pos p)) (gamma i - N2pos (N.pos p))) <
   signature_measure (gen_F i))%nat.

 Lemma PO6: ∀ (s : signature) (p d : positive),
  s = gen_K p d →
  ∀ anonymous : p ≠ 1,
  pos_eq_dec p 1 = right anonymous →
  ∀ q r : N,
  r = 0%N →
  N.pos_div_eucl (p + d) (N.pos p) = (q, 0%N) →
  (signature_measure (gen_F (N2pos q)) < signature_measure (gen_K p d))%nat.

Lemma PO8 :∀ (s : signature) (p d : positive),
  s = gen_K p d →
  ∀ anonymous : p ≠ 1,
  pos_eq_dec p 1 = right anonymous →
  ∀ (q r : N) (p0 : positive),
  r = N.pos p0 →
  N.pos_div_eucl (p + d) (N.pos p) = (q, N.pos p0) →
  (signature_measure (gen_F (N2pos q)) < signature_measure (gen_K p d))%nat.

 Lemma PO9 :∀ (s : signature) (p d : positive),
  s = gen_K p d →
  ∀ anonymous : p ≠ 1,
  pos_eq_dec p 1 = right anonymous →
  ∀ (q r : N) (p0 : positive),
  r = N.pos p0 →
  N.pos_div_eucl (p + d) (N.pos p) = (q, N.pos p0) →
  (signature_measure (gen_K (N2pos (N.pos p0)) (p - N2pos (N.pos p0))) <
   signature_measure (gen_K p d))%nat.
Function chain_gen (s:signature) {measure signature_measure}
: chain_type s :=
  match s return chain_type s with
    | gen_F i ⇒
      if pos_eq_dec i 1 then F1 else
        if pos_eq_dec i 3
        then F3
        else
          match exact_log2 i with
              Some p ⇒ Fexp2 p
            | _ ⇒
              match N.pos_div_eucl i (Npos (gamma i))
              with
                | (q, 0%N) ⇒
                  Fcompose (chain_gen (gen_F (gamma i)))
                            (chain_gen (gen_F (N2pos q)))
                | (q,_r) ⇒ KFF (chain_gen
                                   (gen_K (N2pos _r)
                                          (gamma i - N2pos _r)))
                                (chain_gen (gen_F (N2pos q)))
              end end
    | gen_K p d ⇒
      if pos_eq_dec p 1 then FK (chain_gen (gen_F (1 + d)))
      else
        match N.pos_div_eucl (p + d) (Npos p) with
          | (q, 0%N) ⇒ FFK (chain_gen (gen_F p))
                              (chain_gen (gen_F (N2pos q)))
          | (q, _r) ⇒ KFK (chain_gen (gen_K (N2pos _r)
                                            (p - N2pos _r)))
                          (chain_gen (gen_F (N2pos q)))
        end
  end.

Definition make_chain (n:positive) : chain :=
 F2C (chain_gen (gen_F n)).

Lemma chain_gen_OK : ∀ s:signature,
    OK s (chain_gen s).

Theorem make_chain_correct : ∀ p, chain_correct p (make_chain p).

End Gamma.
Arguments make_chain gamma {_} _ _ _ .


Require Import Int63.Uint63.
Require Import Monoid_instances.

Check cpower (make_chain dicho) 10.
Module Examples.
Search (int → Z).
Search (positive → int).

Definition fast_int63_power (x :positive)(n:N) : Z :=
  to_Z (cpower (make_chain dicho) n (of_pos x)).

Definition slow_int31_power (x :positive)(n:N) : Z :=
  to_Z (power (of_pos x) (N.to_nat n) ).

Definition binary_int31_power (x :positive)(n:N) : Z :=
  to_Z (N_bpow (of_pos x) n).

long computations ...

Definition big_chain := ltac:(compute_chain (make_chain dicho 45319)).

Print big_chain.

Arguments big_chain _%type_scope.

Remark RM : (1 < 56789)%N.

Definition M := Nmod_Monoid 56789%N RM.

Definition exp56789 x := chain_apply big_chain (M:=M) x.


Eval cbv iota match delta [big_chain chain_apply computation_eval ] zeta beta in fun x ⇒ chain_apply big_chain (M:=M) x.

Definition C87' := ltac:( compute_chain C87 ).


Goal parametric (make_chain dicho 45319).

Remark big_correct :chain_correct 45319 (make_chain dicho 45319).

Remark big_correct' : chain_correct 453 (make_chain dicho 453).


Remark big_correct''' : chain_correct 453 (make_chain dicho 453).








End Examples.

Require Import Extraction.
Locate exp56789.
Extraction Language OCaml.
Extraction "bigmod" Examples.exp56789.

Recursive Extraction cpower.
Recursive Extraction make_chain.