Merge branch 'master' into vi.incomp

.github/workflows/PR_summary.yml

@@ -14,6 +14,27 @@ jobs:
       with:
         fetch-depth: 0
 
+    - name: Update the merge-conflict label
+      run: |
+        printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
+        if git merge origin/master --no-ff --no-commit
+        then
+          git merge --abort || true
+          echo "This PR does not have merge conflicts with master."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        else
+          echo "This PR has merge conflicts with main."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request POST \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        fi
+
     - name: Set up Python
       uses: actions/setup-python@v5
       with:

.github/workflows/zulip_emoji_closed_pr.yaml

@@ -0,0 +1,61 @@
+name: Add "closed-pr" emoji in Zulip
+# adds a reaction to Zulip messages that refer to a PR that was closed, but not merged
+
+# triggers the action when
+on:
+  pull_request:
+    # the pull request is closed or reopened, to add or remove the emoji
+    types: [closed, reopened]
+
+jobs:
+  add_closed_pr_emoji:
+    # we set the `TITLE` of the PR as a variable, this shields from possible code injection
+    env:
+      TITLE: ${{ github.event.pull_request.title }}
+
+    name: Add closed-pr emoji in Zulip
+    runs-on: ubuntu-latest
+    steps:
+      - name: Debugging information
+        run: |
+          # may be superfluous: GitHub may print the values of the environment variables by default
+          printf '%s' "${TITLE}" | hexdump -cC
+          printf 'PR title:"%s"\n' "${TITLE}"
+          printf 'issue number: "%s"\npull request number: "%s"\n' "${{ github.event.issue.number }}" "${{ github.event.pull_request.number }}"
+
+      - name: Set up Python
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+
+      - name: Install dependencies
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        run: |
+          python -m pip install --upgrade pip
+          pip install zulip
+
+      - name: checkout zulip_emoji_merge_delegate script
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        uses: actions/checkout@v4
+        with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+      - name: Run Zulip Emoji Merge Delegate Script
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        env:
+          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+          ZULIP_EMAIL: [email protected]
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          # ${{ github.event.action }} is either "closed" or "reopened"
+          # however, it only matters that it is either "closed" or
+          # something different from "closed"
+          # the effect is to add the "closed-pr" emoji to the message, if it is "closed"
+          # and to remove it otherwise
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ github.event.action }}" "${{ github.event.pull_request.number }}"

Archive.lean

@@ -46,6 +46,7 @@ import Archive.Imo.Imo2020Q2
 import Archive.Imo.Imo2021Q1
 import Archive.Imo.Imo2024Q1
 import Archive.Imo.Imo2024Q2
+import Archive.Imo.Imo2024Q3
 import Archive.Imo.Imo2024Q5
 import Archive.Imo.Imo2024Q6
 import Archive.MiuLanguage.Basic

Archive/Imo/Imo1998Q2.lean

@@ -39,9 +39,6 @@ the lower bound: `a(b-1)^2/2 ≤ |A|`.
 Rearranging gives the result.
 -/
 
-
-open scoped Classical
-
 variable {C J : Type*} (r : C → J → Prop)
 
 namespace Imo1998Q2
@@ -86,21 +83,25 @@ theorem JudgePair.agree_iff_same_rating (p : JudgePair J) (c : C) :
     p.Agree r c ↔ (r c p.judge₁ ↔ r c p.judge₂) :=
   Iff.rfl
 
+open scoped Classical in
 /-- The set of contestants on which two judges agree. -/
 def agreedContestants [Fintype C] (p : JudgePair J) : Finset C :=
   Finset.univ.filter fun c => p.Agree r c
 section
 
 variable [Fintype J] [Fintype C]
 
+open scoped Classical in
 /-- All incidences of agreement. -/
 def A : Finset (AgreedTriple C J) :=
   Finset.univ.filter @fun (a : AgreedTriple C J) =>
     (a.judgePair.Agree r a.contestant ∧ a.judgePair.Distinct)
 
+open scoped Classical in
 theorem A_maps_to_offDiag_judgePair (a : AgreedTriple C J) :
     a ∈ A r → a.judgePair ∈ Finset.offDiag (@Finset.univ J _) := by simp [A, Finset.mem_offDiag]
 
+open scoped Classical in
 theorem A_fibre_over_contestant (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct) =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).image Prod.snd := by
@@ -110,6 +111,7 @@ theorem A_fibre_over_contestant (c : C) :
   · rintro ⟨_, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
   · intro h; aesop
 
+open scoped Classical in
 theorem A_fibre_over_contestant_card (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
@@ -119,13 +121,15 @@ theorem A_fibre_over_contestant_card (c : C) :
   rintro ⟨a, p⟩ h ⟨a', p'⟩ h' rfl
   aesop (add simp AgreedTriple.contestant)
 
+open scoped Classical in
 theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
     agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image
     AgreedTriple.contestant := by
   dsimp only [A, agreedContestants]; ext c; constructor <;> intro h
   · rw [Finset.mem_image]; refine ⟨⟨c, p⟩, ?_⟩; aesop
   · aesop
 
+open scoped Classical in
 theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
     (agreedContestants r p).card =
       ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).card := by
@@ -138,6 +142,7 @@ theorem A_card_upper_bound {k : ℕ}
     (hk : ∀ p : JudgePair J, p.Distinct → (agreedContestants r p).card ≤ k) :
     (A r).card ≤ k * (Fintype.card J * Fintype.card J - Fintype.card J) := by
   change _ ≤ k * (Finset.card _ * Finset.card _ - Finset.card _)
+  classical
   rw [← Finset.offDiag_card]
   apply Finset.card_le_mul_card_image_of_maps_to (A_maps_to_offDiag_judgePair r)
   intro p hp
@@ -162,6 +167,7 @@ section
 
 variable [Fintype J]
 
+open scoped Classical in
 theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z + 2 * z + 1 ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c).card := by
   let x := (Finset.univ.filter fun j => r c j).card
@@ -173,6 +179,7 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   suffices x + y = 2 * z + 1 by simp [← Int.ofNat_add, this]
   rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ]; rfl
 
+open scoped Classical in
 theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card := by
   let s := Finset.univ.filter fun p : JudgePair J => p.Agree r c
@@ -192,6 +199,7 @@ theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2
 
 theorem A_card_lower_bound [Fintype C] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) :
     2 * z * z * Fintype.card C ≤ (A r).card := by
+  classical
   have h : ∀ a, a ∈ A r → Prod.fst a ∈ @Finset.univ C _ := by intros; apply Finset.mem_univ
   apply Finset.mul_card_image_le_card_of_maps_to h
   intro c _