(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
pragma +implicits.
(* -------------------------------------------------------------------- *)
require import AllCore List.
require (*--*) Bigop Ring Number.
import Ring.IntID.
(* -------------------------------------------------------------------- *)
abstract theory BigZModule.
type t.
clone import Ring.ZModule as ZM with type t <- t.
clear [ZM.* ZM.AddMonoid.*].
clone include Bigop with
type t <- t,
op Support.idm <- ZM.zeror,
op Support.(+) <- ZM.(+)
proof Support.Axioms.*.
realize Support.Axioms.addmA. by apply/addrA. qed.
realize Support.Axioms.addmC. by apply/addrC. qed.
realize Support.Axioms.add0m. by apply/add0r. qed.
(* -------------------------------------------------------------------- *)
lemma sumrD P F1 F2 (r : 'a list):
(big P F1 r) + (big P F2 r) = big P (fun x => F1 x + F2 x) r.
proof. by rewrite big_split. qed.
(* -------------------------------------------------------------------- *)
lemma sumrN P F (r : 'a list):
- (big P F r) = (big P (fun x => -(F x)) r).
proof. by apply/(big_endo oppr0 opprD). qed.
(* -------------------------------------------------------------------- *)
lemma sumrB P F1 F2 (r : 'a list):
(big P F1 r) - (big P F2 r) = big P (fun x => F1 x - F2 x) r.
proof. by rewrite sumrN sumrD; apply/eq_bigr=> /= x. qed.
(* -------------------------------------------------------------------- *)
lemma nosmt sumr_const (P : 'a -> bool) x s:
big P (fun i => x) s = intmul x (count P s).
proof. by rewrite big_const intmulpE 1:count_ge0 // -ZM.AddMonoid.iteropE. qed.
(* -------------------------------------------------------------------- *)
lemma sumr_undup ['a] (P : 'a -> bool) F s :
big P F s = big P (fun a => intmul (F a) (count (pred1 a) s)) (undup s).
proof.
rewrite big_undup; apply/eq_bigr=> x _ /=.
by rewrite intmulpE ?count_ge0 ZM.AddMonoid.iteropE.
qed.
end BigZModule.
(* -------------------------------------------------------------------- *)
abstract theory BigComRing.
type t.
clone import Ring.ComRing as CR with type t <- t.
clear [CR.* CR.AddMonoid.* CR.MulMonoid.*].
(* -------------------------------------------------------------------- *)
theory BAdd.
clone include BigZModule with
type t <- t,
op ZM.zeror <- CR.zeror,
op ZM.( + ) <- CR.( + ),
op ZM.([-]) <- CR.([-]),
op ZM.intmul <- CR.intmul
proof ZM.* remove abbrev ZM.(-).
realize ZM.addrA. by apply/addrA. qed.
realize ZM.addrC. by apply/addrC. qed.
realize ZM.add0r. by apply/add0r. qed.
realize ZM.addNr. by apply/addNr. qed.
lemma nosmt sumr_1 (P : 'a -> bool) s:
big P (fun i => oner) s = CR.ofint (count P s).
proof. by apply/sumr_const. qed.
lemma mulr_suml (P : 'a -> bool) F s x :
(big P F s) * x = big P (fun i => F i * x) s.
proof. by rewrite big_distrl //; (apply/mul0r || apply/mulrDl). qed.
lemma mulr_sumr (P : 'a -> bool) F s x :
x * (big P F s) = big P (fun i => x * F i) s.
proof. by rewrite big_distrr //; (apply/mulr0 || apply/mulrDr). qed.
lemma divr_suml (P : 'a -> bool) F s x :
(big P F s) / x = big P (fun i => F i / x) s.
proof. by rewrite mulr_suml; apply/eq_bigr. qed.
end BAdd.
(* -------------------------------------------------------------------- *)
theory BMul.
clone include Bigop with
type t <- t,
op Support.idm <- CR.oner,
op Support.(+) <- CR.( * )
proof Support.*.
realize Support.Axioms.addmA. by apply/mulrA. qed.
realize Support.Axioms.addmC. by apply/mulrC. qed.
realize Support.Axioms.add0m. by apply/mul1r. qed.
end BMul.
(* -------------------------------------------------------------------- *)
lemma mulr_big (P Q : 'a -> bool) (f g : 'a -> t) r s:
BAdd.big P f r * BAdd.big Q g s
= BAdd.big P (fun x => BAdd.big Q (fun y => f x * g y) s) r.
proof.
elim: r s => [|x r ih] s; first by rewrite BAdd.big_nil mul0r.
rewrite !BAdd.big_cons; case: (P x) => Px; last by rewrite ih.
by rewrite mulrDl -ih BAdd.mulr_sumr.
qed.
end BigComRing.
(* -------------------------------------------------------------------- *)
abstract theory BigOrder.
type t.
clone import Number.RealDomain as Num with type t <- t.
clear [Num.*].
import Num.Domain.
clone include BigComRing with
type t <- t,
pred CR.unit <- Num.Domain.unit,
op CR.zeror <- Num.Domain.zeror,
op CR.oner <- Num.Domain.oner,
op CR.( + ) <- Num.Domain.( + ),
op CR.([-]) <- Num.Domain.([-]),
op CR.( * ) <- Num.Domain.( * ),
op CR.invr <- Num.Domain.invr,
op CR.intmul <- Num.Domain.intmul,
op CR.ofint <- Num.Domain.ofint,
op CR.exp <- Num.Domain.exp
proof * remove abbrev CR.(-) remove abbrev CR.(/).
realize CR.addrA . proof. by apply/Num.Domain.addrA. qed.
realize CR.addrC . proof. by apply/Num.Domain.addrC. qed.
realize CR.add0r . proof. by apply/Num.Domain.add0r. qed.
realize CR.addNr . proof. by apply/Num.Domain.addNr. qed.
realize CR.oner_neq0 . proof. by apply/Num.Domain.oner_neq0. qed.
realize CR.mulrA . proof. by apply/Num.Domain.mulrA. qed.
realize CR.mulrC . proof. by apply/Num.Domain.mulrC. qed.
realize CR.mul1r . proof. by apply/Num.Domain.mul1r. qed.
realize CR.mulrDl . proof. by apply/Num.Domain.mulrDl. qed.
realize CR.mulVr . proof. by apply/Num.Domain.mulVr. qed.
realize CR.unitP . proof. by apply/Num.Domain.unitP. qed.
realize CR.unitout . proof. by apply/Num.Domain.unitout. qed.
lemma nosmt ler_sum (P : 'a -> bool) (F1 F2 :'a -> t) s:
(forall a, P a => F1 a <= F2 a)
=> (BAdd.big P F1 s <= BAdd.big P F2 s).
proof.
apply: (@BAdd.big_ind2 (fun (x y : t) => x <= y)) => //=.
by apply/ler_add.
qed.
lemma nosmt sumr_ge0 (P : 'a -> bool) (F : 'a -> t) s:
(forall a, P a => zeror <= F a)
=> zeror <= BAdd.big P F s.
proof.
move=> h; apply: (@BAdd.big_ind (fun x => zeror <= x)) => //=.
by apply/addr_ge0.
qed.
lemma nosmt prodr_ge0 (P : 'a -> bool) F s:
(forall a, P a => zeror <= F a)
=> zeror <= BMul.big P F s.
proof.
move=> h; apply: (@BMul.big_ind (fun x => zeror <= x)) => //=.
by apply/mulr_ge0.
qed.
lemma nosmt prodr_gt0 (P : 'a -> bool) F s:
(forall a, P a => zeror < F a)
=> zeror < BMul.big P F s.
proof.
move=> h; apply: (@BMul.big_ind (fun x => zeror < x)) => //=.
by apply/mulr_gt0.
qed.
lemma nosmt ler_prod (P : 'a -> bool) (F1 F2 :'a -> t) s:
(forall a, P a => zeror <= F1 a <= F2 a)
=> (BMul.big P F1 s <= BMul.big P F2 s).
proof.
move=> h; elim: s => [|x s ih]; first by rewrite !BMul.big_nil lerr.
rewrite !BMul.big_cons; case: (P x)=> // /h [ge0F1x leF12x].
by apply/ler_pmul=> //; apply/prodr_ge0=> a /h [].
qed.
lemma nosmt ler_sum_seq (P : 'a -> bool) (F1 F2 :'a -> t) s:
(forall a, mem s a => P a => F1 a <= F2 a)
=> (BAdd.big P F1 s <= BAdd.big P F2 s).
proof.
move=> h; rewrite !(@BAdd.big_seq_cond P).
by rewrite ler_sum=> //= x []; apply/h.
qed.
lemma nosmt sumr_ge0_seq (P : 'a -> bool) (F : 'a -> t) s:
(forall a, mem s a => P a => zeror <= F a)
=> zeror <= BAdd.big P F s.
proof.
move=> h; rewrite !(@BAdd.big_seq_cond P).
by rewrite sumr_ge0=> //= x []; apply/h.
qed.
lemma nosmt prodr_ge0_seq (P : 'a -> bool) F s:
(forall a, mem s a => P a => zeror <= F a)
=> zeror <= BMul.big P F s.
proof.
move=> h; rewrite !(@BMul.big_seq_cond P).
by rewrite prodr_ge0=> //= x []; apply/h.
qed.
lemma nosmt prodr_gt0_seq (P : 'a -> bool) F s:
(forall a, mem s a => P a => zeror < F a)
=> zeror < BMul.big P F s.
proof.
move=> h; rewrite !(@BMul.big_seq_cond P).
by rewrite prodr_gt0=> //= x []; apply/h.
qed.
lemma nosmt ler_prod_seq (P : 'a -> bool) (F1 F2 :'a -> t) s:
(forall a, mem s a => P a => zeror <= F1 a <= F2 a)
=> (BMul.big P F1 s <= BMul.big P F2 s).
proof.
move=> h; rewrite !(@BMul.big_seq_cond P).
by rewrite ler_prod=> //= x []; apply/h.
qed.
end BigOrder.