Skip to content

Commit

Permalink
Made compatible w/ Coq 8.19
Browse files Browse the repository at this point in the history
  • Loading branch information
anlun committed Apr 16, 2024
1 parent 064b5c7 commit 1025881
Show file tree
Hide file tree
Showing 9 changed files with 169 additions and 31 deletions.
4 changes: 3 additions & 1 deletion .github/workflows/nix-action-8.18.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
115 changes: 115 additions & 0 deletions .github/workflows/nix-action-8.19.yml
Original file line number Diff line number Diff line change
@@ -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
5 changes: 4 additions & 1 deletion .nix/config.nix
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,17 @@
# 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";
};
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
Expand Down
2 changes: 1 addition & 1 deletion .nix/coq-nix-toolbox.nix
Original file line number Diff line number Diff line change
@@ -1 +1 @@
"cef6668e637efb2941cbda0ac0f0a435730fa3c1"
"fca0f055eac704f1774a36518b073f20e7cf9862"
27 changes: 16 additions & 11 deletions HahnCountable.v
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down Expand Up @@ -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) :=
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
11 changes: 8 additions & 3 deletions HahnList.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand All @@ -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.
Expand All @@ -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 *)
Expand Down
13 changes: 8 additions & 5 deletions HahnNatExtra.v
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions HahnTrace.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
19 changes: 12 additions & 7 deletions HahnWf.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
}
Expand All @@ -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)
Expand Down

0 comments on commit 1025881

Please sign in to comment.