Library general
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrnat.
Require Import seq.
Require Import ssrfun.
Require Import eqtype.
Require Import fintype.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section Logic.
Lemma iffB: forall a b : bool, (a -> b) -> (b -> a) -> (a=b).
Proof. move=>a b; case: a=>//=. by case: b=>//[->]. by case: b=>//[_ ->]. Qed.
End Logic.
Section Exp.
Fixpoint exp(m n:nat) {struct n}: nat :=
if n is S n' then (m * (exp m n')) else 1.
Lemma exp0n: forall x, exp 0 (S x) = 0.
Proof. by elim. Qed.
Lemma expn1: forall x, exp x 1 = x.
Proof. by move=>x; rewrite /= muln1. Qed.
Lemma exp_positive: forall m n, 0 < m -> 0 < exp m n.
Proof. by move=>m n p; elim:n=>//=[n IH]; rewrite -(muln1 1) leq_mul. Qed.
Lemma exp_plus: forall m n r, exp m (n+r) = exp m n * exp m r.
Proof.
move=>m n r. elim:n=>[|n IH]/=.
by rewrite add0n mul1n. by rewrite -mulnA -IH.
Qed.
Lemma exp_mul: forall x y z, exp (x * y) z = (exp x z) * (exp y z).
Proof. move=>x y; elim=>//=[z IH].
by rewrite IH !mulnA [_*y]mulnC [_*y]mulnC !mulnA [_*(exp x z)]mulnC.
Qed.
Lemma exp_exp: forall m n r, exp (exp m n) r = exp m (n*r).
Proof.
move=>m n; elim=>//=[|r IH]; first by rewrite muln0.
by rewrite IH [_*S _]mulnC /= exp_plus [n*r]mulnC.
Qed.
Lemma leqnexp: forall m n, 1 < m -> n <= exp m n.
Proof.
move=>m n H. elim:n=>//=[n IH]. do 2 case:m H IH =>//=[m H IH].
rewrite -ltnS in IH. apply: (leq_trans IH _).
rewrite mulSn addnA; apply: (leq_trans _ (leq_addr _ _)).
case: (exp (S (S m))) (@exp_positive (S (S m)) n (ltn0Sn (S m)))=>//[e _].
by rewrite addnS ltnS addSn ltnS leq_addr.
Qed.
Lemma leq_exp2l: forall x y1 y2,
(0 < x) -> (y1 <= y2) -> (exp x y1 <= exp x y2).
Proof.
move=>x y1 y2 H K.
rewrite -(subnK K).
elim: (y2-y1)=>//=[|n IH].
by rewrite addn0; apply: leqnn.
by rewrite addnS /=; apply: leq_trans IH _;
rewrite -{1}(mul1n (exp x _)); apply: leq_mul=>//; apply: leqnn.
Qed.
Lemma leq_exp2r: forall x1 x2 y,
(x1 <= x2) -> (exp x1 y <= exp x2 y).
Proof. move=>x1 x2 y H. elim: y=>//=[y IH]. by apply: leq_mul. Qed.
Lemma leq_exp: forall x1 y1 x2 y2,
(0 < x2) ->
(x1 <= x2) -> (y1 <= y2) -> (exp x1 y1) <= (exp x2 y2).
Proof.
move=>x1 y1 x2 y2 U H K. apply: (@leq_trans (exp x2 y1)).
by apply: leq_exp2r. by apply: leq_exp2l.
Qed.
End Exp.
Section Factorial.
multiply m n = m * (m+1) * ... * (m+(n-1))
Fixpoint multiply(m n:nat) {struct n}: nat :=
match n with
| 0 => 1
| S n' => m * (multiply (S m) n')
end.
Lemma multiply_middle: forall m n r, (multiply m n) * (multiply (m+n) r) = multiply m (n+r).
Proof.
move=>m n r. move:m r.
elim:n=>//=[m r|n IH m r].
by rewrite addn0 add0n mul1n.
by rewrite -IH mulnA addSn addnS.
Qed.
Definition fact(n:nat) := multiply 1 n.
Lemma fact_positive: forall n, 0 < fact n.
Proof.
elim=>//=[n IH].
rewrite /fact -[S n]addn1 -(multiply_middle 1 n 1) /= muln1 muln_addr !muln1.
apply: (leq_trans IH _). by apply: leq_addr.
Qed.
Lemma fact_middle: forall m n, (0 < m) -> (m <= n) ->
fact n = multiply 1 (m-1) * m * multiply (m+1) (n-m).
Proof.
move=>m n H1 H2.
rewrite /fact.
move: (multiply_middle 1 (m-1) (n-(m-1))).
rewrite !subnK //.
move=>[<-].
have E: m = multiply m 1 by rewrite /= muln1.
rewrite -[_*m*_]mulnA {5}E multiply_middle.
have F: n- (m - 1) = 1 + (n - m).
rewrite -(@subn_add2r 1 n (m-1)) !subn1 !addn1 !add1n (ltn_predK H1).
by rewrite leq_subS.
by rewrite F.
by rewrite leq_sub_add; apply: leqW.
Qed.
Lemma multiply_exp: forall x y, multiply (S x) y <= exp (x+y) y.
Proof.
move=>x y.
elim: y=>//[y IH].
rewrite -{1}[S y]addn1 -multiply_middle /= mulnC muln1.
apply: leq_mul.
by rewrite addnS; apply:leqnn.
apply: leq_trans IH _.
apply: leq_exp2r.
by rewrite addnS; apply: ltnW; apply:leqnn.
Qed.
Lemma fact_exp: forall x, fact x <= (exp x x).
Proof.
move=>x. rewrite /fact.
apply: leq_trans (@multiply_exp 0 x) _.
by rewrite add0n; apply: leqnn.
Qed.
End Factorial.
Section Division.
Require Import Euclid.
Lemma div_mod_exists: forall m n, 0 < m -> exists q, exists r, (n == q*m + r) && (r < m).
Proof.
move=>m n H.
elim: (quotient m (ltP H) n)=>[q [r [K L]]].
exists q; exists r.
apply/andP; split. apply/eqnP. by rewrite K plusE multE.
by apply/ltP.
Qed.
Inductive diveuclr (a b :nat) : Set :=
divexr : forall q r, r < b -> a = q * b + r -> diveuclr a b.
Lemma eucl_devr : forall b, 0 < b -> forall a:nat, diveuclr a b.
Proof.
move=>b H a. case: (eucl_dev b (ltP H) a)=>q r. move/ltP=> K. move=>E.
rewrite plusE multE in E.
by apply (@divexr a b q r K E).
Qed.
Definition div(a b:nat) (H: (0 < b)) : nat :=
match (eucl_devr H a) with
| divexr q r _ _ => q
end.
Definition mod(a b:nat) (H: (0 < b)) : nat :=
match (eucl_devr H a) with
| divexr q r _ _ => r
end.
Lemma div_mod: forall a b (H: 0 < b), a = (div a H)*b + (mod a H).
Proof. by move=>b H a; rewrite /div /mod; case: (eucl_devr). Qed.
Lemma mod_lt: forall a b (H: 0 < b), (mod a H) < b.
Proof. by move=>b H a; rewrite /mod; case: (eucl_devr). Qed.
Lemma uniq_div: forall m a b r s, r < m -> s < m -> a*m + r = b*m + s -> a = b.
Proof.
have U0: forall m a b r s, r < m -> s < m -> a <=b -> a*m + r = b*m + s -> a = b.
move=>k a b r s Lr Ls L; rewrite -(subnK L).
elim: {1 2 3 5 6}a L => [_ |d IH leq H].
by rewrite mul0n !add0n =>V; case: (b-a) V=>//=[n V]; move: (leq_addr (n*k+s) k);
rewrite addnA -V leqNgt Lr.
by move/eqP: H; rewrite muln_addl /= -!addnA eqn_addl addnA -muln_addl; move/eqP=>H;
rewrite {1}(IH (ltnW leq) H) ?addSn //.
move=>k a b r s Lr Ls; case:(leqP a b)=>[leq|gt K]; first by apply: U0.
by symmetry; symmetry in K; move: K; apply: U0; last by apply: ltnW.
Qed.
Lemma uniq_mod: forall m a b r s, r < m -> s < m -> a*m + r = b*m + s -> r = s.
Proof. by move=>k a b r s Lr Ls E; move: (uniq_div Lr Ls E)=>K; move/eqP: E;
rewrite K eqn_addl; move/eqP. Qed.
Lemma eq_div: forall a b (H: 0 < b) q r, r < b -> a = q*b + r -> div a H = q.
Proof. by move=>a b H q r L E; rewrite (div_mod a H) in E;
apply (uniq_div (mod_lt a H) L E). Qed.
Lemma eq_mod: forall a b (H: 0 < b) q r, r < b -> a = q*b + r -> mod a H = r.
Proof. by move=>a b H q r L E; rewrite (div_mod a H) in E;
apply (uniq_mod (mod_lt a H) L E). Qed.
Lemma mod_small: forall a b (H: 0 < b) (K:a < b), mod a H = a.
Proof. move=>a b H K; move: (div_mod a H).
case: (div a H)=>//=d E; move: (leq_addr (d*b+mod a H) b).
by rewrite addnA -E leqNgt K.
Qed.
Lemma mod0: forall a b (H: 0 < b), mod (a*b) H = 0.
Proof. move=>a b H; move: (erefl (a*b)). rewrite -{2}[a*b]addn0 => E.
by apply (eq_mod H H E).
Qed.
Lemma mod_add: forall a b c (H: 0 < c), mod (a + b) H = mod (a + mod b H) H.
Proof.
move=>a b c H; move: (div_mod (a + b) H)=>K.
rewrite {1}(div_mod b H) [_* c + _]addnC addnA (div_mod (a+mod b H) H) -addnA [_+_*c]addnC addnA -!muln_addl in K.
by symmetry in K; apply: (uniq_mod (mod_lt (a + b) H) (mod_lt (a+mod b H) H) K).
Qed.
Lemma mod_cancel: forall a b c (H: 0 < c), (b < c) -> mod (a + b) H = mod a H -> b = 0.
Proof.
move=>a b c H L E.
rewrite addnC mod_add addnC in E.
move/eqP: (div_mod ((mod a H) + b) H)=>K.
rewrite E addnC eqn_addr in K.
case: (div (b+ mod a H) H) K=>//=[|n F].
by move/eqP.
move: (leq_addr (n*c) c).
rewrite -addn1 muln_addl mul1n addnC in F.
by rewrite -(eqP F) leqNgt L.
Qed.
End Division.
Section OptionData.
Variable A: eqType.
Definition option_eqd(x y: option A) :=
match (x,y) with
| (Some x', Some y') => x' == y'
| (None, None) => true
| _ => false
end.
Lemma option_eqPx: reflect_eq option_eqd.
Proof.
move=>[x|] [y|];
by (apply: (iffP eqP)=>[->|]//=; by case) || (apply introP).
Qed.
Canonical Structure optionData := EqType option_eqPx.
End OptionData.
Section OptionFin.
Variable A: finType.
Definition option_enum := Adds None (maps (fun x => Some x) (enum A)).
Lemma option_enumP: forall x:option A, count (pred1 x) option_enum = 1.
Proof.
case=>[x|]//=.
rewrite count_maps /comp /=.
have E: (fun y => (Some x) == (Some y)) =1 (pred1 x) by move=>z //=.
by rewrite (eq_count E) FinType.enumP.
rewrite count_maps /comp /=.
have E: (fun y:A => None == (Some y)) =1 (pred0) by move=>z //=.
by rewrite (eq_count E) count_pred0.
Qed.
Canonical Structure optionFin := FinType option_enumP.
Definition NoneF: optionFin := None.
Definition SomeF(x:A): optionFin := Some x.
Definition is_some (x: option A) :=
if x is Some _ then true else false.
Variable x: option A.
Lemma is_some_None: (x == None) = (negb (is_some x)).
Proof. by elim:x. Qed.
End OptionFin.
Section OptionTools.
Definition map_option (A B:Type) (f : A->B) (x: option A): option B :=
if x is Some x' then Some (f x') else None.
Lemma card_option: forall A:finType, card (optionFin A) = S (card A).
Proof.
by move=>A; rewrite /card /optionFin /= count_maps /comp /= (eq_count (a2:=A)).
Qed.
Variable A B:finType.
Variable f:A->B.
Lemma is_some_map: forall x, (is_some (map_option f x)) = (is_some x).
Proof. by case =>//=. Qed.
End OptionTools.
Section CardGeneral.
Variable d d' : finType.
Variable f:d->d'.
Lemma image_exists: forall a:pred d, forall y:d', (image f a y) -> {x:d | y = f x}.
move=>a y I.
case: (pickP (preimage f (pred1 y))) =>[x xb|be]//=.
by exists x; apply (eqP xb).
by rewrite /image (eq_disjoint be) disjoint0 in I.
Qed.
Lemma injective_card: (injective f) -> (card d) <= (card d').
Proof. by move=> I; rewrite -(card_image I) cardA /card count_size. Qed.
Lemma card_cat: forall (s1 s2 : seq d), card (cat s1 s2) <= card s1 + card s2.
Proof.
elim=>//=[s2 | hd tl IH s2].
by rewrite card0 add0n; apply: leqnn.
rewrite /card.
elim: (enum d)=>//=[Ihd Itl IIH].
rewrite addnA -[(predU1 hd tl Ihd + _) + _]addnA [_ + s2 Ihd]addnC addnA -addnA.
apply: leq_add =>//.
by rewrite /predU1 mem_cat /predU /=; case: (hd == Ihd); case: (tl Ihd); case: (s2 Ihd).
Qed.
End CardGeneral.
Section Max.
Variable d:finType.
Variable f:d->nat.
Definition max: nat :=
foldr (fun x mx => if (f x) > mx then (f x) else mx) 0 (enum d).
Lemma max_upper: forall x, f x <= max.
Proof.
move=>x.
rewrite /max.
elim: (enum d) (mem_enum x)=>//=[hd tl IH H].
move: (predU1P H)=>[->|H'].
case U: (_<_) =>/=. by apply: leqnn. by rewrite leqNgt U.
case U: (_<_) =>/=. by apply: (leq_trans (IH H') _); apply: ltnW; apply: U. by apply: (IH H').
Qed.
Lemma max_lower: forall n, (forall x, (f x) <=n) -> max <= n.
Proof. by move=>n H; rewrite /max; elim: (enum d)=>//=[hd tl IH]; by case: (_ < _). Qed.
End Max.
Section Seqs.
Variable d1 d2 : eqType.
Fixpoint zip(l1:seq d2) (l2:seq d1) {struct l1} : seq (prod_eqType d2 d1) :=
match (l1,l2) with
| (Adds x1 l1', Adds x2 l2') => Adds (x1, x2) (zip l1' l2')
| _ => seq0
end.
Lemma maps_prodE1_zip: forall l1 l2,
size l1 = size l2 -> maps (fun x=>x.1) (zip l1 l2) = l1.
Proof. by elim=>//=[h1 t1 IH l2]; case:l2=>//[h2 t2]/=; case=>E; rewrite {1}(IH t2 E). Qed.
Lemma maps_prodE2_zip: forall l1 l2,
size l1 = size l2 -> maps (fun x=>x.2) (zip l1 l2) = l2.
Proof. by elim=>[l2|h1 t1 IH l2]; case:l2=>//h2 t2/=; case=>E; rewrite {1}(IH t2 E). Qed.
Lemma eq_maps_mem : forall (f1 f2 : d1 -> d2) (l:seq d1),
(forall x, l x -> f1 x = f2 x) -> maps f1 l = maps f2 l.
Proof.
move=> f1 f2 l Ef.
elim:l Ef => [Ef|x s Hrec Ef] //=.
rewrite (Ef x) ?Hrec //.
by move=>y ymem; apply: Ef; rewrite mem_adds; apply/predU1P; right.
by rewrite mem_adds; apply/predU1P; left.
Qed.
Lemma maps_sub_index:forall (l1:seq d2) (l2:seq d1) x0,
(size l1 = size l2) ->
(forall x, count (pred1 x) l2 <= 1) ->
l1 = maps (fun x=>sub (x0 x) l1 (index x l2)) l2.
Proof.
move=>l1 l2 x0 e.
rewrite -(maps_prodE2_zip e) //; rewrite -{2 3}(maps_prodE1_zip e) //.
move=>c.
elim:(zip l1 l2) c =>//=[h l IH c].
apply/eqP; rewrite /= {1}IH .
rewrite eqseq_adds; apply/andP; split; first by rewrite eq_refl.
apply/eqP; apply: eq_maps_mem=>x x_mem//.
case U: (x == h.2)=>//.
have V: count (pred1 x) (maps (fun x=>x.2) l) == 0.
by move: (c x); rewrite U-[1]addn0 leq_add2l leqn0.
rewrite -leqn0 leqNgt -has_count in V.
by move: (hasPn V x x_mem); rewrite eq_refl.
move=>x.
by apply: (leq_trans _ (c x)); apply: leq_addl.
Qed.
Definition flatten(d:eqType): seq (seq_eqType d) -> seq d :=
foldr (fun x f => cat x f) seq0.
Lemma card_flatten: forall (f1 f2:finType) (f:f1->seq f2) (l:seq f1) b,
(forall x, card (f x) <= b) ->
card (@flatten f2 (maps f l)) <= b * (card l).
Proof.
move=>f1 f2 f l b L.
elim:l=>//=[|x s IH].
by rewrite card0; apply leq0n.
rewrite cardU1.
case H: (s x).
have K: (@flatten f2 (maps f s)) =1 cat (f x) (@flatten f2 (maps f s)).
clear IH; move=>y.
elim: s H=>//=[z t H]; move/predU1P=>[E|N].
by rewrite !mem_cat (*/predU mem_cat *) /predU E orbA orbb.
by rewrite !mem_cat /predU {1}(H N) !mem_cat /predU !orbA (orbC (f z y) (f x y)).
by rewrite /= add0n -(eq_card K).
apply: leq_trans (card_cat _ _) _.
rewrite muln_addr /= muln1.
by apply: leq_add.
Qed.
End Seqs.
Section PigeonHole.
Lemma pigeon: forall (d1 d2:finType) (f:d1->d2),
(card d2 < card d1) -> (exists x:d1, exists y:d1, negb (x == y) && (f x == f y)).
Proof.
move=>d1 d2 f I.
case: (pickP (fun xy => negb ((xy.1) == (xy.2)) && (f (xy.1) == f (xy.2))))=>[[x y] /=m|e].
by exists x; exists y.
have V: (injective f).
move=>x y E.
move: (e (x, y))=>/=; move/nandP=>[H1|H2].
by apply/eqP; apply: negbE2.
by rewrite E eq_refl in H2.
have W: (card d1) <= (card d2) by apply: (injective_card V).
have C: (card d1) < (card d1).
by rewrite -(leq_add2l 1) !add1n in W; apply: (leq_trans W I).
by rewrite ltnn in C.
Qed.
Lemma pigeon_nat: forall (d:finType) (f:nat->d) n,
(card d < n) -> (exists x:nat, exists y:nat, (x < y) && (y < n) && (f x == f y)).
Proof.
move=>d f n H.
set g: ordinal n -> d := fun i => f i.
have gc: card d < card (ordinal_finType n) by rewrite card_ordinal.
move: (pigeon g gc)=>[[x xm] [[y ym] K]]. move/andP: K=>[K1 K2].
rewrite eqE /= in K1.
rewrite /g /= in K2.
case: (leqP x y)=>[|L].
rewrite leq_eqVlt. move/orP=>[L|L]; first by rewrite L in K1.
by exists x; exists y; apply/andP; split; first by apply/andP; split.
exists y; exists x; apply/andP; split; last by rewrite eq_sym.
by apply/andP; split.
Qed.
End PigeonHole.
Prenex Implicits injective_card.