Library prosa.util.lcmseq
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.
A function to calculate the least common multiple
of all integers in a sequence [xs], denoted by [lcml 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 11)
============================
forall (a : nat) (xs : seq nat), a %| lcml (a :: xs)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 13)
a : nat
xs : seq nat
============================
a %| lcml (a :: xs)
----------------------------------------------------------------------------- *)
rewrite /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 14)
a : nat
xs : seq nat
============================
a %| foldr lcmn 1 (a :: xs)
----------------------------------------------------------------------------- *)
induction xs.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 18)
a : nat
============================
a %| foldr lcmn 1 [:: a]
subgoal 2 (ID 22) is:
a %| foldr lcmn 1 [:: a, a0 & xs]
----------------------------------------------------------------------------- *)
- rewrite /foldr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 27)
a : nat
============================
a %| lcmn a 1
subgoal 2 (ID 22) is:
a %| foldr lcmn 1 [:: a, a0 & xs]
----------------------------------------------------------------------------- *)
now apply dvdn_lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
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 32)
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 45)
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.
∀ (a : nat) (xs : seq nat), a %| lcml (a :: xs).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 11)
============================
forall (a : nat) (xs : seq nat), a %| lcml (a :: xs)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 13)
a : nat
xs : seq nat
============================
a %| lcml (a :: xs)
----------------------------------------------------------------------------- *)
rewrite /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 14)
a : nat
xs : seq nat
============================
a %| foldr lcmn 1 (a :: xs)
----------------------------------------------------------------------------- *)
induction xs.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 18)
a : nat
============================
a %| foldr lcmn 1 [:: a]
subgoal 2 (ID 22) is:
a %| foldr lcmn 1 [:: a, a0 & xs]
----------------------------------------------------------------------------- *)
- rewrite /foldr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 27)
a : nat
============================
a %| lcmn a 1
subgoal 2 (ID 22) is:
a %| foldr lcmn 1 [:: a, a0 & xs]
----------------------------------------------------------------------------- *)
now apply dvdn_lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
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 32)
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 45)
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 13)
============================
forall (x : nat) (xs : seq nat), lcml xs %| lcml (x :: xs)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 15)
x : nat
xs : seq nat
============================
lcml xs %| lcml (x :: xs)
----------------------------------------------------------------------------- *)
rewrite /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 16)
x : nat
xs : seq nat
============================
foldr lcmn 1 xs %| foldr lcmn 1 (x :: xs)
----------------------------------------------------------------------------- *)
induction xs; first by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 24)
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 42)
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.
∀ (x : nat) (xs : seq nat),
lcml xs %| lcml (x :: xs).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 13)
============================
forall (x : nat) (xs : seq nat), lcml xs %| lcml (x :: xs)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 15)
x : nat
xs : seq nat
============================
lcml xs %| lcml (x :: xs)
----------------------------------------------------------------------------- *)
rewrite /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 16)
x : nat
xs : seq nat
============================
foldr lcmn 1 xs %| foldr lcmn 1 (x :: xs)
----------------------------------------------------------------------------- *)
induction xs; first by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 24)
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 42)
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 22)
============================
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 25)
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 41)
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 68)
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 145)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
+ apply /dvdnP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 194)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
rewrite EQ /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 197)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
by apply int_divides_lcm_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
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 209)
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 216)
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 233)
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.
∀ (sq : seq nat) (a : nat), a \in sq → ∃ k, lcml sq = k × a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
============================
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 25)
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 41)
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 68)
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 145)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
+ apply /dvdnP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 194)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
rewrite EQ /lcml.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 197)
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 146) is:
exists k : nat, lcml (z :: sq) = k * x
----------------------------------------------------------------------------- *)
by apply int_divides_lcm_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
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 209)
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 216)
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 233)
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.