From be45a11013ab49510d1cade972712501dfa36272 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Sat, 24 May 2025 01:36:09 -0400
Subject: [PATCH 1/3] CJMO 2024 P1

---
 Compfiles/CJMO2024P1.lean | 134 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 134 insertions(+)
 create mode 100644 Compfiles/CJMO2024P1.lean

diff --git a/Compfiles/CJMO2024P1.lean b/Compfiles/CJMO2024P1.lean
new file mode 100644
index 00000000..e876ba2d
--- /dev/null
+++ b/Compfiles/CJMO2024P1.lean
@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2025 The Compfiles Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+import Mathlib
+import ProblemExtraction
+
+problem_file { tags := [.Combinatorics] }
+
+/-!
+# Canadian Junior Math Olympiad 2024, Problem 1
+
+https://cms.math.ca/wp-content/uploads/2024/04/cjmo2024-solutions-en.pdf
+
+Centuries ago, the pirate Captain Blackboard buried a vast amount of treasure in a single
+cell of a 2 × 4 grid-structured island. You and your crew have reached the island and have
+brought special treasure detectors to find the cell with the treasure. For each detector, you can
+set it up to scan a specific subgrid [a, b]×[c, d] with 1 ≤ a ≤ b ≤ 2 and 1 ≤ c ≤ d ≤ 4. Running
+the detector will tell you whether the treasure is in the region or not, though it cannot say
+where in the region the treasure was detected. You plan on setting up Q detectors, which may
+only be run simultaneously after all Q detectors are ready. What is the minimum Q required
+to guarantee your crew can determine the location of Blackboard’s legendary treasure?
+-/
+
+open Set
+
+/-- A single cell of the `2 × 4` grid.
+    We index rows with `Fin 2` and columns with `Fin 4`. -/
+abbrev Cell : Type := Fin 2 × Fin 4
+
+/-- An *axis-aligned detector*, defined by the set of cells it scans.
+    (The usual rectangle parameters `[a,b] × [c,d]` are implicit in this set.) -/
+structure Detector where
+  cells : Finset Cell
+
+namespace Detector
+
+/-- Construct a detector from row bounds `a ≤ b` and column bounds `c ≤ d`. -/
+def ofBounds
+    (a b : Fin 2)
+    (c d : Fin 4)
+: Detector where
+  cells := { p : Cell | a ≤ p.1 ∧ p.1 ≤ b ∧ c ≤ p.2 ∧ p.2 ≤ d }
+
+end Detector
+
+/-- The outcome vector produced by *Q* detectors for a hidden treasure cell. -/
+def outcome {Q : ℕ} (D : Fin Q → Detector) (treasure : Cell) : List.Vector Bool Q :=
+  List.Vector.ofFn (fun i ↦ treasure ∈ (D i).cells)
+
+/-- A family of detectors *distinguishes* every treasure location
+    if distinct cells yield distinct outcome vectors. -/
+def Distinguishes {Q : ℕ} (D : Fin Q → Detector) : Prop :=
+  ∀ {c₁ c₂ : Cell}, c₁ ≠ c₂ → outcome D c₁ ≠ outcome D c₂
+
+/-- The minimum number of non-adaptive detectors needed to guarantee
+    the treasure cell can be identified. -/
+noncomputable def minQ : ℕ :=
+  sInf {Q : ℕ | ∃ D : Fin Q → Detector, Distinguishes D}
+
+def D (i : Fin 3): Detector :=
+  match i with
+  | 0 => Detector.ofBounds 0 0 0 3 -- first detector covers first row
+    -- ┌───┬───┬───┬───┐
+    -- │ X │ X │ X │ X │  (covers entire first row)
+    -- ├───┼───┼───┼───┤
+    -- │   │   │   │   │
+    -- └───┴───┴───┴───┘
+  | 1 => Detector.ofBounds 0 1 0 1 -- second detector covers first two colums
+    -- ┌───┬───┬───┬───┐
+    -- │ X │ X │   │   │  (covers first two columns of both rows)
+    -- ├───┼───┼───┼───┤
+    -- │ X │ X │   │   │
+    -- └───┴───┴───┴───┘
+  | 2 => Detector.ofBounds 0 1 1 2 -- third detector covers middle
+    -- ┌───┬───┬───┬───┐
+    -- │   │ X │ X │   │  (covers middle two columns of both rows)
+    -- ├───┼───┼───┼───┤
+    -- │   │ X │ X │   │
+    -- └───┴───┴───┴───┘
+
+lemma D_distinguishes : Distinguishes D := by
+  intro c₁ c₂ h
+  fin_cases c₁ <;> fin_cases c₂ <;>
+  first | decide | exfalso; simp at h
+
+noncomputable determine solution : ℕ := 3
+
+/-- Exactly three detectors are necessary and sufficient to localize the treasure. -/
+problem cjmo2024_p1 : minQ = solution := by
+  have : minQ ≤ 3 := by
+    unfold minQ
+    apply Nat.sInf_le
+    use D
+    exact D_distinguishes
+
+  have card_cell : Nat.card Cell = 8 := by simp
+  have card_vec_2 : Nat.card (List.Vector Bool 2) = 4 := by simp
+
+  have : 2 ∉ {Q : ℕ | ∃ D : Fin Q → Detector, Distinguishes D} := by
+    intro h
+    rcases h with ⟨D, hD⟩
+    unfold Distinguishes at hD
+    have : Set.InjOn (outcome D) ⊤ := by
+      intro p _ q _ h
+      cases (eq_or_ne p q)
+      case inl h => exact h
+      case inr h' =>
+        specialize hD h'
+        exact False.elim (hD h)
+
+    have outcode_inj : Function.Injective (outcome D) := by
+      intro p q h
+      cases (eq_or_ne p q)
+      case inl h => exact h
+      case inr h' =>
+        specialize hD h'
+        exact False.elim (hD h)
+
+    have prereq : (Nat.card (List.Vector Bool 2) = 0 → Nat.card Cell = 0) := by
+      intro h
+      rw [card_vec_2] at h
+      exfalso
+      norm_num at h
+
+    have test3 := Finite.card_le_of_injective' outcode_inj prereq
+
+    rw [card_cell] at test3
+    rw [show Nat.card (List.Vector Bool 2) = 4 by simp] at test3
+
+    linarith
+
+  sorry

From 4609352a615541c5ee1c2713df60165ee1231b00 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Sat, 24 May 2025 14:32:29 -0400
Subject: [PATCH 2/3] files

---
 Compfiles.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Compfiles.lean b/Compfiles.lean
index 0a84efbd..d70fcd40 100644
--- a/Compfiles.lean
+++ b/Compfiles.lean
@@ -5,6 +5,7 @@ import Compfiles.Bulgaria1998P6
 import Compfiles.Bulgaria1998P8
 import Compfiles.Bulgaria1998P11
 import Compfiles.CIIM2022P6
+import Compfiles.CJMO2024P1
 import Compfiles.Canada1998P3
 import Compfiles.Canada1998P5
 import Compfiles.Hungary1998P6

From 5b8f8d8747746c07ca57d507a718c06720c7533b Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Mon, 26 May 2025 16:12:47 -0400
Subject: [PATCH 3/3] snips

---
 Compfiles/CJMO2024P1.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Compfiles/CJMO2024P1.lean b/Compfiles/CJMO2024P1.lean
index e876ba2d..60e50090 100644
--- a/Compfiles/CJMO2024P1.lean
+++ b/Compfiles/CJMO2024P1.lean
@@ -59,6 +59,8 @@ def Distinguishes {Q : ℕ} (D : Fin Q → Detector) : Prop :=
 noncomputable def minQ : ℕ :=
   sInf {Q : ℕ | ∃ D : Fin Q → Detector, Distinguishes D}
 
+snip begin
+
 def D (i : Fin 3): Detector :=
   match i with
   | 0 => Detector.ofBounds 0 0 0 3 -- first detector covers first row
@@ -85,6 +87,8 @@ lemma D_distinguishes : Distinguishes D := by
   fin_cases c₁ <;> fin_cases c₂ <;>
   first | decide | exfalso; simp at h
 
+snip end
+
 noncomputable determine solution : ℕ := 3
 
 /-- Exactly three detectors are necessary and sufficient to localize the treasure. -/