Module Ring_polynom_AddOn

Adapter of Ring_polynom for VPL needs. - We instantiate polynomials on Z - We introduce an alternative definition of evaluation closer to our needs.

Require Coq.setoid_ring.Cring.
Require Export Coq.setoid_ring.Ring_polynom.
Require Export ZArith.
Require Import Equivalence.

Open Scope Z_scope.

Instance Zops: (@Ncring.Ring_ops Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z)).

Instance Qri : (Ncring.Ring (Ro:=Zops)).
constructor; try Morphisms.solve_proper.
- exact eq_equivalence.
- exact Zplus_comm.
- exact Zplus_assoc.
- exact Zmult_1_l.
- exact Zmult_1_r.
- exact Zmult_assoc.
- exact Zmult_plus_distr_l.
- intros; apply Zmult_plus_distr_r.
- exact Zplus_opp_r.
Defined.

Instance Zcri : (Cring.Cring (R:=Z)).
- exact Zmult_comm.
Defined.
Definition Zpower: Z -> N -> Z
:= pow_N 1 Zmult.

Definition PExpr:=PExpr Z.

Definition Pol:=Pol Z.

Definition PEeval (l:list Z) (p:PExpr): Z
:= PEeval 0 Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) Zpower l p.

Definition Pphi (l:list Z) (p:Pol): Z
:= Pphi 0 Zplus Zmult (fun x => x) l p.

Definition norm (pe:PExpr): Pol :=
  norm_aux 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe.

Definition Peq (p1 p2:Pol) : bool :=
  Peq Zeq_bool p1 p2.

Definition PExpr_eq (pe1 pe2: PExpr): bool :=
  Peq (norm pe1) (norm pe2).

Extraction Inline PExpr_eq Peq norm.

Fixpoint PEsem (pe: PExpr) (m: positive -> Z): Z :=
match pe with
  | PEc c => c
  | PEX j => m j
  | PEadd pe1 pe2 => Zplus (PEsem pe1 m) (PEsem pe2 m)
  | PEsub pe1 pe2 => Zminus (PEsem pe1 m) (PEsem pe2 m)
  | PEmul pe1 pe2 => Zmult (PEsem pe1 m) (PEsem pe2 m)
  | PEopp pe1 => Zopp (PEsem pe1 m)
  | PEpow pe1 n => Zpower (PEsem pe1 m) n
  end.

Require Import Coq.setoid_ring.BinList.

Lemma jump_iter_tl_aux {A} (n:nat): forall (l:list A),
  jump (Pos.of_nat (S n)) l = nat_iter (S n) (@tl _) l.

Proof.

  simpl; induction n; simpl; auto.
  intros; rewrite <- IHn.
  rewrite jump_succ. simpl; auto.
Qed.

Lemma jump_iter_tl {A} (p:positive) (l: list A):
jump p l = nat_iter (Pos.to_nat p) (@tl _) l.

Proof.

  rewrite <- (Pos2Nat.id p) at 1.
  generalize (Pos2Nat.is_pos p).
  generalize (Pos.to_nat p).
  intros n; case n.
  - intros H; inversion H.
  - intros n0 H; clear H.
  apply jump_iter_tl_aux.
Qed.

Lemma nth_positive_nat_iter {A} (p:positive): forall (l:list A) d,
nth d p l = hd d (nat_iter (pred (Pos.to_nat p)) (@tl _) l).

Proof.

  induction p; auto.
    - intros; simpl; rewrite IHp; simpl.
      rewrite jump_iter_tl.
      rewrite <- nat_iter_plus.
      rewrite <- nat_iter_succ_r.
      cutrewrite ((S (pred (Pos.to_nat p) + Pos.to_nat p))=(Pos.to_nat p~0)).
      simpl; auto.
      rewrite Pos2Nat.inj_xO.
      generalize (Pos2Nat.is_pos p).
      omega.
  - intros; simpl; rewrite IHp; simpl.
      rewrite jump_iter_tl.
      rewrite <- nat_iter_plus.
      cutrewrite (((pred (Pos.to_nat p)) + Pos.to_nat p)%nat=pred (Pos.to_nat p~0)).
      simpl; auto.
      rewrite Pos2Nat.inj_xO.
      generalize (Pos2Nat.is_pos p).
      omega.
Qed.

Lemma List_nth_hd_iter_tl {A} (n:nat): forall (l:list A) (d:A),
List.nth n l d = hd d (nat_iter n (@tl _) l).

Proof.

  induction n.
    - destruct l; simpl; auto.
    - intros; rewrite nat_iter_succ_r.
      rewrite <- IHn.
      destruct l; simpl; auto. destruct n; simpl; auto.
Qed.

Lemma nth_positive_nat {A} (p:positive) (l:list A) d:
nth d p l = List.nth (pred (Pos.to_nat p)) l d.

Proof.

intros; rewrite List_nth_hd_iter_tl, nth_positive_nat_iter.
auto.
Qed.

Definition mkMemoryList {A} (bound: positive) (mem: positive -> A)
:= List.map (fun n => mem (Pos.of_nat n)) (List.seq (S O) (Pos.to_nat bound)).

Lemma nth_mkMemoryList {A} p bnd (mem: positive -> A) d:
(p <= bnd)%positive -> nth d p (mkMemoryList bnd mem) = mem p.

Proof.

  unfold mkMemoryList.
  intros; assert (Y:(pred (Pos.to_nat p) < Pos.to_nat bnd)%nat).
    assert (X:forall (n m:nat), (0 < n)%nat -> (n <= m)%nat -> (pred n < m)%nat).
    intros; omega.
    apply X.
    apply Pos2Nat.is_pos.
    rewrite <- Pos2Nat.inj_le. auto.
  clear H; rewrite nth_positive_nat; erewrite nth_indep.
  - rewrite List.map_nth, seq_nth.
    apply f_equal.
    assert (X:forall (n:nat), (0 < n)%nat -> (1 + pred n)%nat = n).
    + intros; omega.
    + rewrite X. apply Pos2Nat.id.
      apply Pos2Nat.is_pos.
    + auto.
  - intros; autorewrite with list; auto.
  Grab Existential Variables. apply O.
Qed.

Fixpoint bound (pe:PExpr): positive :=
  match pe with
  | PEX x => x
  | PEadd pe1 pe2 => Pmax (bound pe1) (bound pe2)
  | PEsub pe1 pe2 => Pmax (bound pe1) (bound pe2)
  | PEmul pe1 pe2 => Pmax (bound pe1) (bound pe2)
  | PEopp pe => bound pe
  | PEpow pe _ => bound pe
  | _ => xH
  end.
Local Hint Resolve Pos.max_lub_l Pos.max_lub_r Pos.le_max_l Pos.le_max_r.

Theorem PEsem_Eval (pe: PExpr) (m: positive -> Z) bnd:
((bound pe) <= bnd)%positive -> PEsem pe m = PEeval (mkMemoryList bnd m) pe.

Proof.

induction pe; simpl; auto; try (intros; rewrite IHpe || rewrite IHpe1, IHpe2; eauto).
intros; rewrite nth_mkMemoryList; auto.
Qed.

Local Hint Resolve Zeq_bool_eq.

Theorem PEnorm_correct (pe: PExpr) (m: positive -> Z) bnd:
((bound pe) <= bnd)%positive ->
PEsem pe m = Pphi (mkMemoryList bnd m) (norm pe).

Proof.

  intros; erewrite PEsem_Eval; eauto.
  unfold PEeval, Pphi, norm; eapply norm_aux_spec.
  - apply Eqsth.
  - eapply Cring.cring_eq_ext; eauto.
  - eapply Cring.cring_almost_ring_theory; eauto.
  - eapply mkmorph; eauto.
  - apply Cring.cring_power_theory; eauto.
Qed.

Theorem PExpr_eq_correct (pe1 pe2: PExpr) (m: positive -> Z):
PExpr_eq pe1 pe2 = true -> PEsem pe1 m = PEsem pe2 m.

Proof.

  unfold PExpr_eq, Peq. intro H; rewrite! PEnorm_correct with (bnd:=Pmax (bound pe1) (bound pe2)); auto.
  unfold Pphi. refine (Peq_ok _ _ _ _ _ H _).
  - eapply Cring.cring_eq_ext; eauto.
  - eapply mkmorph; eauto.
  Grab Existential Variables.
    apply Zplus.
    apply 0.
Qed.