Test coqbot responses #217
Comments
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y
opam pin add coq 'https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
1 similar comment
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 27KiB file on GitHub Actions Artifacts under
|
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 27KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y
opam pin add coq 'https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y -k git
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 27KiB file on GitHub Actions Artifacts under
|
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 27KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y -k git
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 27KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon:coq-core.opam' --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon:coq-stdlib.opam' --no-action
opam install coq coq-core coq-stdlib --reinstall
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 28KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon'
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 25KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 29KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --confirm-level=unsafe-yes
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/bug.v (full log on GitHub Actions - verbose log) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 77KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq coq-core coq-stdlib coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --confirm-level=unsafe-yes
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam install coq coq-core coq-stdlib coqide-server --reinstall -y --confirm-level=unsafe-yes
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 25KiB file on GitHub Actions Artifacts under
|
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 29KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/bug.v (full log on GitHub Actions - verbose log) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 13KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross) build logminimizer logIf you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging |
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/bug.v (full log on GitHub Actions - verbose log) 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 87 lines to 50 lines, then from 55 lines to 52 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.13.1
coqtop version 58611a5f03d0:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (b999f458037563317ddbb8ab6e3ecf9e1986077d)
Expected coqc runtime on this file: 0.220 sec *)
Require Stdlib.ZArith.ZArith.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
-
apply length_chunk_app; assumption.
-
intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+
pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+
rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 14KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/bug.v (full log on GitHub Actions - verbose log) 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 87 lines to 50 lines, then from 55 lines to 52 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.13.1
coqtop version 5e78f6d93a6e:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (b999f458037563317ddbb8ab6e3ecf9e1986077d)
Expected coqc runtime on this file: 0.218 sec *)
Require Stdlib.ZArith.ZArith.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
-
apply length_chunk_app; assumption.
-
intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+
pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+
rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 14KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > bug.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q bug.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Minimized File (full log on GitHub Actions) 🌟 Minimized Coq File (consider adding this file to the test-suite)Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 30KiB file on GitHub Actions Artifacts under
|
|
@coqbot minimize coq.dev #!/usr/bin/env bash
true | coqtop
coqc --version
opam pin remove coq -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-core 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coq-stdlib 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam pin add coqide-server 'git+https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y --no-action
opam reinstall coq coq-core coq-stdlib coqide-server -y --confirm-level=unsafe-yes || exit 1
true | coqtop
coqc --version
cat <<EOF > test.v
Require Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Arith.PeanoNat.
Import Coq.Lists.List.
Import ListNotations.
Module Import Nat.
Definition div_up a b := Nat.div (a + (b-1)) b.
Lemma div_up_range a b (H : b <> 0) : a <= div_up a b * b < a + b.
Admitted.
Lemma div_up_add_mod a b n:
(a mod n = 0)%nat ->
Nat.div_up (a + b) n =
(Nat.div_up a n + Nat.div_up b n)%nat.
Admitted.
Lemma div_up_exact_mod a b:
(b <> 0)%nat ->
(a mod b = 0)%nat ->
((Nat.div_up a b) * b = a)%nat.
Admitted.
Section Chunk.
Context [A : Type] (k : nat).
Implicit Types (bs ck xs ys : list A).
Fixpoint chunk' bs ck {struct bs} : list (list A).
Admitted.
Definition chunk bs := chunk' bs [].
Context (Hk : k <> 0).
Lemma nth_error_chunk bs i (Hi : i < div_up (length bs) k)
: nth_error (chunk bs) i = Some (firstn k (skipn (i*k) bs)).
Admitted.
Lemma length_chunk bs : length (chunk bs) = div_up (length bs) k.
Admitted.
Lemma length_chunk_app (l l' : list A) :
(length l mod k)%nat = 0%nat ->
length (chunk (l ++ l')) = length (chunk l ++ chunk l').
Admitted.
Lemma chunk_app : forall (l l': list A),
(length l mod k = 0)%nat ->
chunk (l ++ l') = chunk l ++ chunk l'.
Proof.
intros * Hmod.
eapply nth_ext with (d := []) (d' := []); [ | intros idx ].
- apply length_chunk_app; assumption.
- intros Hidx; eassert (Some _ = Some _) as HS; [ | injection HS; intros Hs; apply Hs ].
rewrite <- !nth_error_nth' by assumption.
rewrite <- !nth_error_nth' by (rewrite length_chunk_app in Hidx; eassumption).
assert (idx < length (chunk l) \/ length (chunk l) <= idx)%nat as [Hlt | Hge] by lia;
[ rewrite nth_error_app1 | rewrite nth_error_app2 ]; try eassumption.
all: rewrite !nth_error_chunk.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hlt by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hidx by assumption.
all: repeat rewrite ?length_chunk, ?app_length, ?div_up_add_mod in Hge by assumption.
all: rewrite ?length_chunk, ?app_length, ?div_up_add_mod by assumption.
all: try lia.
all: pose proof Nat.div_up_range (length l) k ltac:(lia).
+ pose proof div_up_exact_mod (length l) k ltac:(lia) ltac:(lia).
rewrite !firstn_skipn_comm, !firstn_app.
replace (idx * k + k - length l)%nat with 0%nat by nia.
simpl; rewrite app_nil_r; reflexivity.
+ rewrite Nat.mul_sub_distr_r.
erewrite div_up_exact_mod by lia.
rewrite skipn_app, skipn_all2; [ reflexivity | nia ].
Qed.
EOF
coqc -q test.v |
|
Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 30KiB file on GitHub Actions Artifacts under
|
|
Testing MetaRocq/metarocq#1072 (comment) opam install -y coq-wasm
cat > test_bug.v <<EOF
From Coq Require Import List.
From Coq.Strings Require Import Byte.
From CertiCoq.Plugin Require Import CertiCoq.
From Wasm Require Import binary_format_parser datatypes instantiation_func.
Definition test_bytes : list Byte.byte := x00 :: x61 :: x73 :: x6d :: x01 :: x00 :: x00 :: x00 :: nil.
Definition test_module : option module := run_parse_module test_bytes.
CertiCoq Compile test_module.
EOF
coqc -q test_bug.v |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
No description provided.
The text was updated successfully, but these errors were encountered: