Revision 25d7504145c07e4345a472338a8616b023fc8243 authored by Pierre-Yves Strub on 11 July 2015, 19:03:40 UTC, committed by Pierre-Yves Strub on 12 July 2015, 12:14:23 UTC
[fix #17219]
1 parent 9b8598c
Poly.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B licence.
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Fun.
require import Pred.
require import Int.
require import NewList.
require (*--*) Ring.
(* -------------------------------------------------------------------- *)
type R.
type poly.
clone import Ring.ComRing with type t <- R.
op ofseq : R list -> poly.
op toseq : poly -> R list.
op norm_r (s : R list) =
with s = "[]" => []
with s = (::) x s' =>
if x = zeror then norm_r s' else s.
op norm (s : R list) = rev (norm_r (rev s)).
axiom ofseqK p: ofseq (toseq p) = p.
axiom toseqK s: toseq (ofseq s) = norm s.
axiom toseq_last p: last_ oner (toseq p) <> zeror.
axiom poly_eq p q:
(forall x, nth zeror (toseq p) x = nth zeror (toseq q) x) => p = q.
lemma norm_nil: norm [] = [].
proof. by rewrite /norm rev_nil. qed.
lemma norm1 x: norm [x] = if x = zeror then [] else [x].
proof. by rewrite /norm rev1 /=; case (x = zeror). qed.
lemma nth_norm n s: nth zeror (norm s) n = nth zeror s n.
proof.
case (n < 0) => [h|]; first by rewrite !nth_neg.
rewrite -lezNgt; elim/last_ind s n => [|s x IHs] n ge0_n.
by rewrite norm_nil.
rewrite /norm rev_rcons /=; case (x = zeror) => [-> |].
rewrite -/(norm _) IHs // nth_rcons; case (n < size s)=> //.
by rewrite -lezNgt => h; rewrite nth_default.
by move=> _; rewrite rev_cons revK.
qed.
(* -------------------------------------------------------------------- *)
op deg (p : poly) = size (toseq p) axiomatized by degE.
op coeff (p : poly) n = nth zeror (toseq p) n axiomatized by coeffE.
op lead_coef (p : poly) = coeff p (deg p - 1) axiomatized by lead_coefE.
(* -------------------------------------------------------------------- *)
op coefp n = fun p, coeff p n.
(* -------------------------------------------------------------------- *)
lemma poly_eqP p q: (forall x, coeff p x = coeff q x) <=> p = q.
proof.
by split=> [| ->] // h; apply/poly_eq=> x; have := h x; rewrite !coeffE.
qed.
(* -------------------------------------------------------------------- *)
op polyC (c : R) = ofseq [c].
lemma polyseqC (c : R): toseq (polyC c) = if c = zeror then [] else [c].
proof. by rewrite /polyC toseqK norm1. qed.
lemma size_polyC c : deg (polyC c) = if c = zeror then 0 else 1.
proof. by rewrite degE /= polyseqC; case (c = zeror). qed.
lemma coefC c i: coeff (polyC c) i = if i = 0 then c else zeror.
proof.
by rewrite coeffE /= polyseqC; case (c = zeror) => [-> | //]; case (i = 0).
qed.
lemma polyCK: cancel polyC (coefp 0).
proof. by move=> c; rewrite /coefp coefC. qed.
lemma polyC_inj: injective polyC.
proof.
move=> c1 c2 eqc12; cut := coefC c2 0 => /=.
by rewrite -eqc12 coefC.
qed.
lemma lead_coefC c: lead_coef (polyC c) = c.
proof.
by rewrite lead_coefE degE coeffE /= !polyseqC; case (c = zeror).
qed.
(* -------------------------------------------------------------------- *)
lemma coef_ofseq s k: coeff (ofseq s) k = nth zeror s k.
proof. by rewrite coeffE /= toseqK nth_norm. qed.
lemma coef_neg p n: n < 0 => coeff p n = zeror.
proof. by move=> h; rewrite coeffE /= nth_neg. qed.
lemma coef_overdeg p k: deg p <= k => coeff p k = zeror.
proof. by rewrite degE coeffE /= => h; rewrite nth_default. qed.
(* -------------------------------------------------------------------- *)
op poly (E : int -> R) n = ofseq (mkseq E n).
lemma coef_poly n E k:
coeff (poly E n) k = if 0 <= k < n then E k else zeror.
proof.
rewrite lezNgt; case (k < 0) => /=.
by move=> lt0_k; rewrite coef_neg.
rewrite -lezNgt => ge0_k; case (k < n) => /=.
by move=> lt_kn; rewrite /poly coef_ofseq nth_mkseq.
rewrite -lezNgt => le_nk; rewrite /poly coef_ofseq.
by rewrite nth_default // size_mkseq; smt.
qed.
lemma coefK p: poly (coeff p) (deg p) = p.
proof.
apply poly_eqP=> x; rewrite coef_poly lezNgt; case (x < 0)=> /=.
by move=> lt0_x; rewrite coef_neg.
move=> _; rewrite coeffE degE /=; case (x < size (toseq p)) => //.
by rewrite -lezNgt => _; rewrite nth_default.
qed.
(* -------------------------------------------------------------------- *)
op poly0 = polyC zeror axiomatized by poly0E.
theory ZModule.
op (+) (p q : poly) =
poly (fun i, coeff p i + coeff q i) (max (deg p) (deg q))
axiomatized by add_polyE.
op [-] (p : poly) =
poly (fun i, -(coeff p i)) (deg p)
axiomatized by opp_polyE.
lemma coef_add_poly (p q : poly) i : coeff (p + q) i = coeff p i + coeff q i.
proof.
case (i < 0) => [lt0_i|]; first by rewrite !coef_neg // addr0.
rewrite -lezNgt => ge0_i; rewrite add_polyE /= coef_poly ge0_i /=.
case (i < max (deg p) (deg q)) => //; rewrite -lezNgt => h.
rewrite !coef_overdeg ?add0r //; smt.
qed.
lemma coef_opp_poly (p : poly) i: coeff (-p) i = -(coeff p i).
proof.
case (i < 0) => [lt0_i|]; first by rewrite !coef_neg // oppr0.
rewrite -lezNgt => ge0_i; rewrite opp_polyE /= coef_poly ge0_i /=.
by case (i < deg p) => // h; rewrite coef_overdeg ?oppr0 // lezNgt.
qed.
lemma add_polyA: associative ZModule.(+).
proof.
by move=> p q r; rewrite -poly_eqP=> i; rewrite !coef_add_poly addrA.
qed.
lemma add_polyC: commutative ZModule.(+).
proof.
by move=> p q; rewrite -poly_eqP=> i; rewrite !coef_add_poly addrC.
qed.
lemma add_poly0 (p : poly): poly0 + p = p.
proof.
by rewrite -poly_eqP=> i; rewrite coef_add_poly poly0E coefC /= add0r.
qed.
lemma add_polyN (p : poly): -p + p = poly0.
proof.
rewrite -poly_eqP=> i; rewrite coef_add_poly coef_opp_poly.
by rewrite poly0E coefC /= addNr.
qed.
end ZModule.
Computing file changes ...