From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.util.tactics.

(** A function to calculate the least common multiple 
    of all integers in a sequence [xs], denoted by [lcml xs]. *)
Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.

(** First we show that [x] divides [lcml (x :: xs)] for any [x] and [xs]. *)
Lemma int_divides_lcm_in_seq: 
  forall (x : nat) (xs : seq nat), x %| lcml (x :: xs).
forall (x : nat) (xs : seq nat), x %| lcml (x :: xs)
Proof.
forall (x : nat) (xs : seq nat), x %| lcml (x :: xs)
  induction xs.
x: nat
x %| lcml [:: x]
x, a: nat
xs: seq nat
IHxs: x %| lcml (x :: xs)
x %| lcml [:: x, a & xs] 
  -
x: nat
x %| lcml [:: x]
x, a: nat
xs: seq nat
IHxs: x %| lcml (x :: xs)
x %| lcml [:: x, a & xs] by apply dvdn_lcml.
x, a: nat
xs: seq nat
IHxs: x %| lcml (x :: xs)
x %| lcml [:: x, a & xs]
  -
x, a: nat
xs: seq nat
IHxs: x %| lcml (x :: xs)
x %| lcml [:: x, a & xs] rewrite /lcml -cat1s foldr_cat /foldr.
x, a: nat
xs: seq nat
IHxs: x %| lcml (x :: xs)
x
%| lcmn x
     (lcmn a
        ((fix foldr (s : seq nat) : nat :=
            match s with
            | [::] => 1
            | x :: s' => lcmn x (foldr s')
            end) xs))
    by apply dvdn_lcml.
Qed.

(** Similarly, [lcml xs] divides [lcml (x :: xs)] for any [x] and [xs]. *) 
Lemma lcm_seq_divides_lcm_super: 
  forall (x : nat) (xs : seq nat), 
  lcml xs %| lcml (x :: xs).
forall (x : nat) (xs : seq nat),
lcml xs %| lcml (x :: xs)
Proof.
forall (x : nat) (xs : seq nat),
lcml xs %| lcml (x :: xs)
  induction xs; first by auto.
x, a: nat
xs: seq nat
IHxs: lcml xs %| lcml (x :: xs)
lcml (a :: xs) %| lcml [:: x, a & xs]
  rewrite /lcml -cat1s foldr_cat /foldr.
x, a: nat
xs: seq nat
IHxs: lcml xs %| lcml (x :: xs)
lcmn a
  ((fix foldr (s : seq nat) : nat :=
      match s with
      | [::] => 1
      | x :: s' => lcmn x (foldr s')
      end) xs)
%| lcmn x
     ((fix foldr (s : seq nat) : nat :=
         match s with
         | [::] => 1
         | x :: s' => lcmn x (foldr s')
         end) ([:: a] ++ xs))
  by apply dvdn_lcmr.
Qed.

(** Given a sequence [xs], any integer [x \in xs] divides [lcml xs]. *)
Lemma lcm_seq_is_mult_of_all_ints: 
  forall (x : nat) (xs: seq nat), x \in xs -> x %| lcml xs.
forall (x : nat) (xs : seq nat),
x \in xs -> x %| lcml xs 
Proof.
forall (x : nat) (xs : seq nat),
x \in xs -> x %| lcml xs
  intros x xs IN; apply/dvdnP.
x: nat
xs: seq nat
IN: x \in xs
exists k : nat, lcml xs = k * x
  induction xs as [ | z sq IH_DIV]; first by done.
x, z: nat
sq: seq nat
IN: x \in z :: sq
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
exists k : nat, lcml (z :: sq) = k * x
  rewrite in_cons in IN.
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: (x == z) || (x \in sq)
exists k : nat, lcml (z :: sq) = k * x
  move : IN => /orP [/eqP EQ | IN].
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
EQ: x = z
exists k : nat, lcml (z :: sq) = k * x
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x
  -
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
EQ: x = z
exists k : nat, lcml (z :: sq) = k * x
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x apply /dvdnP.
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
EQ: x = z
x %| lcml (z :: sq)
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x
    rewrite EQ /lcml.
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
EQ: x = z
z %| foldr lcmn 1 (z :: sq)
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x
    by apply int_divides_lcm_in_seq.
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x
  +
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
exists k : nat, lcml (z :: sq) = k * x move : (IH_DIV IN) => [k EQ].
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
k: nat
EQ: lcml sq = k * x
exists k : nat, lcml (z :: sq) = k * x
    exists ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) * k).
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
k: nat
EQ: lcml sq = k * x
lcml (z :: sq) =
foldr lcmn 1 (z :: sq) %/ foldr lcmn 1 sq * k * x
    rewrite -mulnA -EQ divnK /lcml //.
x, z: nat
sq: seq nat
IH_DIV: x \in sq -> exists k : nat, lcml sq = k * x
IN: x \in sq
k: nat
EQ: lcml sq = k * x
foldr lcmn 1 sq %| foldr lcmn 1 (z :: sq)
    by apply lcm_seq_divides_lcm_super.
Qed.

(** The LCM of all elements in a sequence with only positive elements is positive. *)
Lemma all_pos_implies_lcml_pos:
  forall (xs : seq nat),
    (forall x, x \in xs -> x > 0) ->
    lcml xs > 0.
forall xs : seq nat,
(forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
Proof.
forall xs : seq nat,
(forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
  intros * POS.
xs: seq nat
POS: forall x : nat_eqType, x \in xs -> 0 < x
0 < lcml xs
  induction xs; first by easy.
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < lcml (a :: xs)
  rewrite /lcml -cat1s //= lcmn_gt0.
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
(0 < a) && (0 < foldr lcmn 1 xs)
  apply/andP; split => //.
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < a
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < foldr lcmn 1 xs
  -
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < a
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < foldr lcmn 1 xs by apply POS; rewrite in_cons eq_refl.
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < foldr lcmn 1 xs
  -
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
IHxs: (forall x : nat_eqType, x \in xs -> 0 < x) ->
0 < lcml xs
0 < foldr lcmn 1 xs apply: IHxs; intros b B_IN.
a: nat
xs: seq nat
POS: forall x : nat_eqType, x \in a :: xs -> 0 < x
b: nat_eqType
B_IN: b \in xs
0 < b
    by apply POS; rewrite in_cons; apply /orP; right => //.
Qed.