Library prosa.util.lcmseq


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
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.

Any integer [a] that is contained in the sequence [xs] divides [lcml xs].
Lemma int_divides_lcm_in_seq:
  ∀ (a : nat) (xs : seq nat), a %| lcml (a :: xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 9)
  
  ============================
  forall (a : nat) (xs : seq nat), a %| lcml (a :: xs)

----------------------------------------------------------------------------- *)

Proof.
  intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 11)
  
  a : nat
  xs : seq nat
  ============================
  a %| lcml (a :: xs)

----------------------------------------------------------------------------- *)

  rewrite /lcml.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 12)
  
  a : nat
  xs : seq nat
  ============================
  a %| foldr lcmn 1 (a :: xs)

----------------------------------------------------------------------------- *)

  induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 16)
  
  a : nat
  ============================
  a %| foldr lcmn 1 [:: a]

subgoal 2 (ID 20) is:
 a %| foldr lcmn 1 [:: a, a0 & xs]

----------------------------------------------------------------------------- *)

  - rewrite /foldr.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 25)
  
  a : nat
  ============================
  a %| lcmn a 1

subgoal 2 (ID 20) is:
 a %| foldr lcmn 1 [:: a, a0 & xs]

----------------------------------------------------------------------------- *)

    now apply dvdn_lcml.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 20)
  
  a, a0 : nat
  xs : seq nat
  IHxs : a %| foldr lcmn 1 (a :: xs)
  ============================
  a %| foldr lcmn 1 [:: a, a0 & xs]

----------------------------------------------------------------------------- *)

  - rewrite -cat1s.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  a, a0 : nat
  xs : seq nat
  IHxs : a %| foldr lcmn 1 (a :: xs)
  ============================
  a %| foldr lcmn 1 ([:: a] ++ a0 :: xs)

----------------------------------------------------------------------------- *)

    rewrite foldr_cat /foldr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  a, a0 : nat
  xs : seq nat
  IHxs : a %| foldr lcmn 1 (a :: xs)
  ============================
  a
  %| lcmn a
       (lcmn a0
          ((fix foldr (s : seq nat) : nat :=
              match s with
              | [::] => 1
              | x :: s' => lcmn x (foldr s')
              end) xs))

----------------------------------------------------------------------------- *)

    by apply dvdn_lcml.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

Also, [lcml xs1] divides [lcml xs2] if [xs2] contains one extra element as compared to [xs1].
Lemma lcm_seq_divides_lcm_super:
  ∀ (x : nat) (xs : seq nat),
  lcml xs %| lcml (x :: xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 11)
  
  ============================
  forall (x : nat) (xs : seq nat), lcml xs %| lcml (x :: xs)

----------------------------------------------------------------------------- *)

Proof.
  intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 13)
  
  x : nat
  xs : seq nat
  ============================
  lcml xs %| lcml (x :: xs)

----------------------------------------------------------------------------- *)

  rewrite /lcml.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 14)
  
  x : nat
  xs : seq nat
  ============================
  foldr lcmn 1 xs %| foldr lcmn 1 (x :: xs)

----------------------------------------------------------------------------- *)

  induction xs; first by auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 22)
  
  x, a : nat
  xs : seq nat
  IHxs : foldr lcmn 1 xs %| foldr lcmn 1 (x :: xs)
  ============================
  foldr lcmn 1 (a :: xs) %| foldr lcmn 1 [:: x, a & xs]

----------------------------------------------------------------------------- *)

  rewrite -cat1s foldr_cat /foldr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  x, a : nat
  xs : seq nat
  IHxs : foldr lcmn 1 xs %| foldr lcmn 1 (x :: xs)
  ============================
  lcmn a
    ((fix foldr (s : seq nat) : nat :=
        match s with
        | [::] => 1
        | x0 :: s' => lcmn x0 (foldr s')
        end) xs)
  %| lcmn x
       ((fix foldr (s : seq nat) : nat :=
           match s with
           | [::] => 1
           | x0 :: s' => lcmn x0 (foldr s')
           end) ([:: a] ++ xs))

----------------------------------------------------------------------------- *)

  by apply dvdn_lcmr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

All integers in a sequence [xs] divide [lcml xs].
Lemma lcm_seq_is_mult_of_all_ints:
  ∀ (sq : seq nat) (a : nat), a \in sq → ∃ k, lcml sq = k × a.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 19)
  
  ============================
  forall (sq : seq nat) (a : nat),
  a \in sq -> exists k : nat, lcml sq = k * a

----------------------------------------------------------------------------- *)

Proof.
  intros xs x IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 22)
  
  xs : seq nat
  x : nat
  IN : x \in xs
  ============================
  exists k : nat, lcml xs = k * x

----------------------------------------------------------------------------- *)

  induction xs as [ | z sq IH_DIVIDES]; first by easy.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  z : nat
  sq : seq nat
  x : nat
  IN : x \in z :: sq
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  ============================
  exists k : nat, lcml (z :: sq) = k * x

----------------------------------------------------------------------------- *)

  rewrite in_cons in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 65)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : 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].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 140)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  EQ : x = z
  ============================
  exists k : nat, lcml (z :: sq) = k * x

subgoal 2 (ID 141) is:
 exists k : nat, lcml (z :: sq) = k * x

----------------------------------------------------------------------------- *)

  + apply /dvdnP.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 189)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  EQ : x = z
  ============================
  x %| lcml (z :: sq)

subgoal 2 (ID 141) is:
 exists k : nat, lcml (z :: sq) = k * x

----------------------------------------------------------------------------- *)

    rewrite EQ /lcml.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 192)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  EQ : x = z
  ============================
  z %| foldr lcmn 1 (z :: sq)

subgoal 2 (ID 141) is:
 exists k : nat, lcml (z :: sq) = k * x

----------------------------------------------------------------------------- *)

    by apply int_divides_lcm_in_seq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 141)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  IN : x \in sq
  ============================
  exists k : nat, lcml (z :: sq) = k * x

----------------------------------------------------------------------------- *)

  + move : (IH_DIVIDES IN) ⇒ [k EQ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 204)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : x \in sq -> exists k : nat, lcml sq = k * x
  IN : x \in sq
  k : nat
  EQ : lcml sq = k * x
  ============================
  exists k0 : nat, lcml (z :: sq) = k0 * x

----------------------------------------------------------------------------- *)

    ∃ ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) × k).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 211)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : 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 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 228)
  
  z : nat
  sq : seq nat
  x : nat
  IH_DIVIDES : 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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

The LCM of all elements in a sequence with only positive elements is positive.
Lemma all_pos_implies_lcml_pos:
  ∀ (xs : seq nat),
    (∀ b, b \in xs → b > 0) →
    lcml xs > 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 26)
  
  ============================
  forall xs : seq nat,
  (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs

----------------------------------------------------------------------------- *)

Proof.
  intros × POS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 28)
  
  xs : seq nat
  POS : forall b : nat_eqType, b \in xs -> 0 < b
  ============================
  0 < lcml xs

----------------------------------------------------------------------------- *)

  induction xs; first by easy.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  0 < lcml (a :: xs)

----------------------------------------------------------------------------- *)

  rewrite /lcml -cat1s ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  0 < foldr lcmn 1 ([:: a] ++ xs)

----------------------------------------------------------------------------- *)

  simpl; rewrite lcmn_gt0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 78)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  (0 < a) && (0 < foldr lcmn 1 xs)

----------------------------------------------------------------------------- *)

  apply /andP; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 104)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  0 < a

subgoal 2 (ID 105) is:
 0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

  + apply POS; rewrite in_cons; apply /orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 180)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  a == a

subgoal 2 (ID 105) is:
 0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

    now apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 105)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

  + feed_n 1 IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 209)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  ============================
  forall b : nat_eqType, b \in xs -> 0 < b

subgoal 2 (ID 214) is:
 0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

    - intros b B_IN.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 216)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : (forall b : nat_eqType, b \in xs -> 0 < b) -> 0 < lcml xs
  b : nat_eqType
  B_IN : b \in xs
  ============================
  0 < b

subgoal 2 (ID 214) is:
 0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

      now apply POS; rewrite in_cons; apply /orP; right ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 214)
  
  a : nat
  xs : seq nat
  POS : forall b : nat_eqType, b \in a :: xs -> 0 < b
  IHxs : 0 < lcml xs
  ============================
  0 < foldr lcmn 1 xs

----------------------------------------------------------------------------- *)

    - now rewrite /lcml in IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.