diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 8e50a77..4384779 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -102,8 +102,10 @@ name: Nix CI for bundle 8.18 'on': pull_request: paths: - - .github/workflows/** + - .github/workflows/nix-action-8.18.yml pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.18.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml new file mode 100644 index 0000000..4607e4b --- /dev/null +++ b/.github/workflows/nix-action-8.19.yml @@ -0,0 +1,115 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + hahn: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup weakmemory + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: weakmemory + - id: stepCheck + name: Checking presence of CI target hahn + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"hahn\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hahn" +name: Nix CI for bundle 8.19 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.19.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.19.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index 0e68439..faea8e0 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -30,7 +30,7 @@ # coqproject = "_CoqProject"; ## select an entry to build in the following `bundles` set - default-bundle = "8.18"; + default-bundle = "8.19"; bundles."8.17" = { coqPackages.coq.override.version = "8.17"; @@ -38,6 +38,9 @@ bundles."8.18" = { coqPackages.coq.override.version = "8.18"; }; + bundles."8.19" = { + coqPackages.coq.override.version = "8.19"; + }; ## Cachix caches to use in CI ## Below we list some standard ones diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 8fb619a..4de5be7 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"cef6668e637efb2941cbda0ac0f0a435730fa3c1" +"fca0f055eac704f1774a36518b073f20e7cf9862" diff --git a/HahnCountable.v b/HahnCountable.v index 5daee26..83d2fad 100644 --- a/HahnCountable.v +++ b/HahnCountable.v @@ -22,7 +22,7 @@ Lemma findP_spec A (cond : A -> Prop) (l : list A) forall j, j < findP cond l -> ~ cond (nth j l d). Proof. induction l; ins; desf; splits; ins; desf; try lia; intuition. - eauto using lt_S_n. + eauto using PeanoNat.lt_S_n. Qed. Lemma exists_min (cond : nat -> Prop) (H: exists n, cond n) : @@ -83,7 +83,9 @@ Lemma lt_funI f (ONE: forall x, x < f x) i j (LT: i < j) d : Proof. revert i LT; induction j; ins; try lia. destruct (eqP i j); desf; eauto. - eapply lt_trans, ONE; apply IHj; lia. + etransitivity. + { apply IHj. lia. } + apply ONE. Qed. Definition lt_size A i (s : A -> Prop) := @@ -200,17 +202,18 @@ Section countable. intros; specialize (M i); desc. specialize_full SUR; eauto; desf. destruct (le_lt_dec i0 i); [by edestruct M0; eauto|]. - revert M M0; rewrite (le_plus_minus (S i) i0); auto with arith. + revert M M0. + replace i0 with (S i + (i0 - S i)) by lia. generalize (i0 - S i) as n; intros. exists (S i + findP (fun x => s x /\ ~ In x (mk_list (S i) f)) (mk_list (S n) (fun x => (f (S i + x))))). forward eapply findP_spec with (cond := fun x => s x /\ ~ In x (mk_list (S i) f)) (d := f 0) (l := mk_list (S n) (fun x => (f (S i + x)))) as K; desc; eauto. - by apply in_mk_list_iff; eauto. - split; try done; rewrite in_mk_list_iff; intro X; desf. - by symmetry in X0; eapply M0 in X0; eauto with arith. - + { by apply in_mk_list_iff; eauto. } + { split; try easy. + rewrite in_mk_list_iff; intro X; desf. + by symmetry in X0; eapply M0 in X0; eauto with arith. } rewrite nth_mk_list in *; desf. by rewrite in_mk_list_iff in *; destruct K1; eauto with arith. @@ -219,8 +222,9 @@ Section countable. by exists j; auto with arith. specialize (K0 (j - S i)). rewrite nth_mk_list in K0; desf; [lia|]. - rewrite le_plus_minus_r, in_mk_list_iff in K0; auto with arith. - apply NNPP; intro; eapply K0; desf; lia. } + rewrite in_mk_list_iff in K0; auto with arith. + apply NNPP; intro; eapply K0; desf; try lia. + replace (S i + (j - S i)) with j by lia; auto. } apply choice in N; destruct N as [g N]. right. @@ -410,7 +414,8 @@ Section enum_ext. Lemma prefix_of_nat_prefix i j (LEQ : i <= j) : exists l, prefix_of_nat j = prefix_of_nat i ++ l. Proof. - apply le_plus_minus in LEQ; rewrite LEQ; generalize (j - i) as n. + replace j with (i + (j - i)) by lia. + generalize (j - i) as n. clear; intro n; rewrite Nat.add_comm; induction n; ins; desf; eauto using app_nil_end. by rewrite IHn; eexists; rewrite <- app_assoc. Qed. @@ -604,7 +609,7 @@ Section enum_ext. assert (Lin : i < n). { clear - SUR Li. red in Li; desc. - eapply lt_le_trans; eauto. + eapply Nat.lt_le_trans; eauto. replace n with (length (map f (List.seq 0 n))) by now (rewrite length_map, length_seq). apply NoDup_incl_length; try red; ins. diff --git a/HahnList.v b/HahnList.v index d1bb255..e960305 100644 --- a/HahnList.v +++ b/HahnList.v @@ -1136,7 +1136,9 @@ Lemma mk_listE n A (f: nat -> A) : Proof. induction n; ins; rewrite IHn. rewrite seq_split with (x:=n) (y:=S n); try lia. - by rewrite map_app, plus_0_r, <- minus_Sn_m, minus_diag. + rewrite map_app. + rewrite Nat.add_0_r. + replace (S n - n) with 1 by lia; ins. Qed. Lemma in_mk_list_iff A (x: A) n f : @@ -1160,7 +1162,9 @@ Proof. induction n; ins; desf; rewrite app_nth; desf; rewrite mk_list_length in *; desf; try lia. apply nth_overflow; ins; lia. - by assert (i = n) by lia; desf; rewrite minus_diag. + assert (i = n) by lia; desf. + replace (n - n) with 0 by lia. + ins. Qed. Definition length_mk_list := mk_list_length. @@ -1182,7 +1186,8 @@ Fixpoint max_of_list l := Lemma max_of_list_app l l' : max_of_list (l ++ l') = max (max_of_list l) (max_of_list l'). Proof. - by induction l; ins; rewrite IHl, Max.max_assoc. + induction l; ins; rewrite IHl. + lia. Qed. (** Miscellaneous *) diff --git a/HahnNatExtra.v b/HahnNatExtra.v index 4bd5001..557ac2d 100644 --- a/HahnNatExtra.v +++ b/HahnNatExtra.v @@ -1,4 +1,5 @@ -Require Import NPeano Arith micromega.Lia Setoid HahnBase. +Require Import Arith micromega.Lia Setoid HahnBase. +Require Import PeanoNat. Lemma div2_add_double n m : Nat.div2 (2 * n + m) = n + Nat.div2 m. @@ -36,15 +37,17 @@ Qed. Lemma arith_sum_le_mono n m (L : n <= m) : arith_sum n <= arith_sum m. Proof. - apply le_plus_minus in L; rewrite L; clear L; generalize (m - n) as k; ins. - rewrite Nat.add_comm; induction k; ins. + apply Nat.sub_add in L; rewrite <- L; clear L. + generalize (m - n) as k; ins. + induction k; ins. rewrite arith_sum_S; lia. Qed. Lemma arith_sum_lt n m (L : n < m) : arith_sum n + n < arith_sum m. Proof. - apply le_plus_minus in L; rewrite L; clear L; generalize (m - S n) as k; intros. - replace (S n + k) with (S (n + k)) by done. + apply Nat.sub_add in L; rewrite <- L; clear L. + generalize (m - S n) as k; intros. + replace (k + S n) with (S (n + k)) by lia. rewrite arith_sum_S. forward apply (arith_sum_le_mono n (n + k)); lia. Qed. diff --git a/HahnTrace.v b/HahnTrace.v index 79824ab..e2f3aa9 100644 --- a/HahnTrace.v +++ b/HahnTrace.v @@ -394,8 +394,8 @@ Proof. do 2 f_equal. eapply filterP_map_seq_eq; simpl; eauto. ins; forward apply (l0 (length l + i)); desf; try lia. - by rewrite minus_plus. - ins; eapply l1 in H; lia. + 2: ins; eapply l1 in H; lia. + replace (length l + i - length l) with i; ins; lia. - eapply map_trace_prepend_lt with (fl := fl) in l2; desf. rewrite l4, filterP_app, appA; clear l4. f_equal. diff --git a/HahnWf.v b/HahnWf.v index 43b5cde..c7c3a1e 100644 --- a/HahnWf.v +++ b/HahnWf.v @@ -86,12 +86,13 @@ Proof. { clear - R1; intros; desc. revert L0. - rewrite (le_plus_minus _ _ L); generalize (j - S i) as k. + rewrite <- (Nat.sub_add _ _ L). + generalize (j - S i) as k. revert R1; generalize (2 * n + 1) as m; ins. induction k; rewrite ?Nat.add_0_r; vauto. apply t_step, R1; lia. eapply t_trans, t_step; [apply IHk; lia|]. - rewrite Nat.add_succ_r; apply R1; lia. + rewrite !Nat.add_succ_r. ins. apply R1. lia. } tertium_non_datur (exists i j, i < j <= n /\ f (2 * i) = f (2 * j)) as [C|C]; desc. @@ -121,9 +122,11 @@ Proof. apply powE; exists f; splits; ins; eapply R1; lia. assert (L: r ^^ (2 * n + 1 - 2 * x) (f (2 * x)) (f (S (2 * n)))). { apply powE; exists (fun n => f (2 * x + n)); rewrite ?Nat.add_0_r. - rewrite le_plus_minus_r; splits; intros; try done; try lia. - f_equal; lia. - rewrite Nat.add_succ_r; apply R1; lia. } + splits; auto. + { ins. f_equal. lia. } + intros. + replace (2 * x + S i) with (S (2 * x + i)) by lia. + apply R1; lia. } rewrite <- Nat.add_succ_l, <- Nat.add_1_r. do 2 hahn_rewrite pow_add; unfold seq; repeat eexists; eauto. } @@ -132,8 +135,10 @@ Proof. - edestruct IRR. exists (2 * x0 - 2 * x); split; try lia. eexists; split; [apply powE|edone]. - exists (fun n => f (n + 2 * x)); splits; intros; - try (f_equal; lia); apply R1; lia. + exists (fun n => f (n + 2 * x)); splits; intros. + all: try (f_equal; lia). + ins. apply R1. + lia. Qed. Lemma ct_bounded_n_total A s (r : relation A) (ACYC: acyclic r)