Library additions.AM
Abstract machine for following an Euclidean addition chain adapted from the old contrib coq-additions
Work in progress
From Coq Require Import List PArith Relations Lia.
Import Morphisms.
From additions Require Import Monoid_def Monoid_instances Strategies.
Import Monoid_def.
From Coq Require Import Recdef Wf_nat.
From additions Require Import More_on_positive Pow Euclidean_Chains
Dichotomy BinaryStrat.
Generalizable All Variables.
Import Morphisms.
From additions Require Import Monoid_def Monoid_instances Strategies.
Import Monoid_def.
From Coq Require Import Recdef Wf_nat.
From additions Require Import More_on_positive Pow Euclidean_Chains
Dichotomy BinaryStrat.
Generalizable All Variables.
basic instructions
Inductive instr : Set :=
| MUL : instr
| SQR : instr
| PUSH : instr
| SWAP : instr.
Definition code := list instr.
Definition mults_squares c :=
let fix count (c: code) mults squares :=
match c with
nil ⇒ (mults, squares)
| PUSH :: c' | SWAP :: c' ⇒ count c' mults squares
| SQR :: c' ⇒ count c' mults (S squares)
| MUL :: c' ⇒ count c' (S mults) squares
end in count c 0%nat 0%nat.
Section Semantics.
Variable A : Type.
Variable mul : A → A → A.
Variable one : A.
Definition stack := list A.
Definition config := (A × list A)%type.
Fixpoint exec (c : code) (x:A) (s: stack) : option config :=
match c, s with
nil, _ ⇒ Some (x,s)
| MUL::c, y::s ⇒ exec c (mul x y) s
| SQR::c, s ⇒ exec c (mul x x) s
| PUSH::c, s ⇒ exec c x (x::s)
| SWAP::c, y::z::s ⇒ exec c x (z::y::s)
| _,_ ⇒ None
end.
Lemma exec_app :
∀ (c c' : code) x s ,
exec (c ++ c') x s =
match exec c x s with
| None ⇒ None
| Some (y,s') ⇒ exec c' y s'
end.
| MUL : instr
| SQR : instr
| PUSH : instr
| SWAP : instr.
Definition code := list instr.
Definition mults_squares c :=
let fix count (c: code) mults squares :=
match c with
nil ⇒ (mults, squares)
| PUSH :: c' | SWAP :: c' ⇒ count c' mults squares
| SQR :: c' ⇒ count c' mults (S squares)
| MUL :: c' ⇒ count c' (S mults) squares
end in count c 0%nat 0%nat.
Section Semantics.
Variable A : Type.
Variable mul : A → A → A.
Variable one : A.
Definition stack := list A.
Definition config := (A × list A)%type.
Fixpoint exec (c : code) (x:A) (s: stack) : option config :=
match c, s with
nil, _ ⇒ Some (x,s)
| MUL::c, y::s ⇒ exec c (mul x y) s
| SQR::c, s ⇒ exec c (mul x x) s
| PUSH::c, s ⇒ exec c x (x::s)
| SWAP::c, y::z::s ⇒ exec c x (z::y::s)
| _,_ ⇒ None
end.
Lemma exec_app :
∀ (c c' : code) x s ,
exec (c ++ c') x s =
match exec c x s with
| None ⇒ None
| Some (y,s') ⇒ exec c' y s'
end.
Main well-formed chains
raises x to its cube
chain for raising x to its (2 ^ q)th power
Fixpoint F2q_of_nat q := match q with
| 0%nat ⇒ nil
| S p ⇒ SQR:: F2q_of_nat p
end.
Definition F2q (p:positive) :=
F2q_of_nat (Pos.to_nat p).
for computing x^(pq+r) passing by x^p
for computing x^p and x^(pq)
for computing x^p then x^(pq + r)
Definition KFK (kpr mq: code) :=
kpr ++ PUSH::SWAP :: (mq ++ MUL :: nil).
Definition FK (fn: code) := PUSH::fn.
End Semantics.
Definition chain_apply c {A:Type}
{op:A→A→A}{one:A}{equ: Equiv A}
(M: EMonoid op one equ) x
:= exec _ op c x nil.
Example code for 7 via 3
Example code for 31 via 7
24, 3
For 99 and 24
Specification and generation of correct chains
We have to build equivalences between configurations
Inductive stack_equiv {A}`{M : @EMonoid A op one equ}:
list A → list A → Prop
:=
stack_equiv0 : stack_equiv nil nil
| stack_equivn: ∀ x y s s', x == y → stack_equiv s s' →
stack_equiv (x::s) (y:: s').
Definition config_equiv {A}`{M : @EMonoid A op one equ}
(c c' : config A): Prop :=
fst c == fst c' ∧ stack_equiv (snd c) (snd c').
Inductive result_equiv`{M : @EMonoid A op one equ}: relation (option (config A)):=
result_equiv_fail : result_equiv None None
| result_equiv_success : ∀ x s y s',
config_equiv (x,s) (y, s') →
result_equiv (Some (x,s)) (Some (y,s')).
Definition Fchain_correct (p: positive) (c: code) :=
(∀ A op one equ (M: @EMonoid A op one equ) (x:A) s,
result_equiv (M:=M) (exec A op c x s)
(Some (Pow.Pos_bpow x p, s))) .
Definition Kchain_correct n p c :=
(∀ A op one equ (M: @EMonoid A op one equ) (x:A) s,
result_equiv (exec A op c x s)
(Some (Pow.Pos_bpow x n, Pow.Pos_bpow x p ::s))).
Definition correctness_statement (s: signature) : code → Prop :=
match s with
| gen_F p ⇒ fun c ⇒ Fchain_correct p c
| gen_K p d ⇒ fun c ⇒ Kchain_correct (p + d) p c
end.
#[ global ] Instance Stack_equiv_refl {A}`{M : @EMonoid A op one equ} :
Reflexive stack_equiv.
#[ global ] Instance Stack_equiv_equiv {A}`{M : @EMonoid A op one equ}:
Equivalence stack_equiv.
#[ global ] Instance result_equiv_equiv `{M : @EMonoid A op one equ}:
Equivalence result_equiv.
Lemma exec_equiv `{M : @EMonoid A op one equ} :
∀ c x s y s' , config_equiv (x, s) (y, s') →
result_equiv (exec A op c x s) (exec A op c y s').
#[ global ] Instance exec_Proper `{M : @EMonoid A op one equ} :
Proper (Logic.eq ==> equiv ==> stack_equiv ==> result_equiv) (@exec A op) .
Lemma F1_correct : Fchain_correct 1 F1.
F3 is correct
Lemma F3_correct : Fchain_correct 3 F3.
Import Pow.
Lemma F2q_correct_0: ∀ `{M : @EMonoid A op one equ} (n:nat) x s,
result_equiv (exec A op (F2q_of_nat n) x s)
(Some(Pow.power x (2 ^ n), s)).
Lemma F2q_correct_1 (n:nat) : Fchain_correct (Pos.of_nat (2 ^ n))
(F2q_of_nat n).
Remark Pos_to_nat_diff_0 n : Pos.to_nat n ≠ 0%nat.
Lemma F2q_correct (n:positive) : Fchain_correct (2 ^ n) (F2q n).
Section CompositionProofs.
Section FK.
Variable n : positive.
Variable cn : code.
Hypothesis Hn : Fchain_correct n cn.
Lemma FK_correct : Kchain_correct n 1 (FK cn).
End FK.
Section App.
Variables n p: positive.
Variables cn cp: code.
Hypothesis Hn : Fchain_correct n cn .
Hypothesis Hp : Fchain_correct p cp.
Lemma correct_app : Fchain_correct (n × p) (cn ++ cp).
End App.
Section FFK.
Variables p q: positive.
Variables cp cq: code.
Hypothesis Hp : Fchain_correct p cp.
Hypothesis Hq : Fchain_correct q cq.
Lemma FFK_correct : Kchain_correct (p × q) p (FFK cp cq).
End FFK.
Section KFK.
Variables p q r : positive.
Variables kpr mq : code.
Hypothesis Hpr : Kchain_correct p r kpr.
Hypothesis Hq : Fchain_correct q mq.
Lemma KFK_correct : Kchain_correct (p × q + r) p (KFK kpr mq).
Lemma KFF_correct: Fchain_correct (p × q + r) (KFF kpr mq).
End KFK.
End CompositionProofs.
Definition OK (s: signature)
:= fun c: code ⇒ correctness_statement s c.
Section Gamma.
Variable gamma: positive → positive.
Context (Hgamma : Strategy gamma).
Function chain_gen (s:signature) {measure signature_measure}
: code :=
match 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 ⇒ F2q p
| _ ⇒
match N.pos_div_eucl i (Npos (gamma i))
with
| (q, 0%N) ⇒
(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.
Defined.
Definition make_chain (n:positive) : code :=
(chain_gen (gen_F n)).
Proof of correctness
Lemma chain_gen_OK : ∀ s:signature, OK s (chain_gen s).
Section All_OK.
Variables (n:positive).
Let c := chain_gen (gen_F n).
Lemma L0: Fchain_correct n c.
End All_OK.
Definition AM_power {A : Type}
`(M: @EMonoid A E_op E_one E_eq) (x:A) (n:positive) :=
exec A E_op (chain_gen (gen_F n)) x nil.
Lemma AM_power_Ok {A : Type}
`(M: @EMonoid A E_op E_one E_eq) (x:A) (n:positive):
result_equiv (AM_power M x n) (Some (Pos_bpow x n, nil)).
End Gamma.
Arguments chain_gen gamma {Hgamma} _.
Definition F197887 := chain_gen dicho (gen_F 197887).