From 79011cc68f105687b13af403fc3a65553e757ed0 Mon Sep 17 00:00:00 2001 From: Constantin Seebach Date: Sun, 1 Mar 2026 21:34:18 +0100 Subject: [PATCH 1/2] Imo1979P6 --- Compfiles.lean | 1 + Compfiles/Imo1979P2.lean | 312 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 313 insertions(+) create mode 100644 Compfiles/Imo1979P2.lean diff --git a/Compfiles.lean b/Compfiles.lean index f1431c76..c49089f7 100644 --- a/Compfiles.lean +++ b/Compfiles.lean @@ -72,6 +72,7 @@ import Compfiles.Imo1978P5 import Compfiles.Imo1978P6 import Compfiles.Imo1979P1 import Compfiles.Imo1979P5 +import Compfiles.Imo1979P6 import Compfiles.Imo1981P3 import Compfiles.Imo1981P6 import Compfiles.Imo1982P1 diff --git a/Compfiles/Imo1979P2.lean b/Compfiles/Imo1979P2.lean new file mode 100644 index 00000000..126b57f4 --- /dev/null +++ b/Compfiles/Imo1979P2.lean @@ -0,0 +1,312 @@ +/- +Copyright (c) 2026 The Compfiles Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Constantin Seebach +-/ + +import Mathlib + +import ProblemExtraction + +problem_file { tags := [.Combinatorics] } + +/-! +# International Mathematical Olympiad 1979, Problem 6 + +Let $A$ and $E$ be opposite vertices of an octagon. +A frog starts at vertex $A.$ From any vertex except $E$ it jumps to one of the two adjacent vertices. +When it reaches $E$ it stops. Let $a_n$ be the number of distinct paths of exactly $n$ jumps ending at $E$. +Prove that: \[a_{2n-1}=0, \quad a_{2n}={(2+\sqrt2)^{n-1} - (2-\sqrt2)^{n-1} \over\sqrt2}.\] +-/ + +namespace Imo1979P6 + +open SimpleGraph + +abbrev Octagon := cycleGraph 8 +abbrev A : Fin 8 := 0 +abbrev E : Fin 8 := 4 + +def isTerminalWalk {V : Type} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) := v ∉ w.support.dropLast + +noncomputable def a (n : ℕ) := Set.ncard {w : Octagon.Walk A E | isTerminalWalk w ∧ w.length = n} + +snip begin + +instance instFintypeAnd {α : Type} [DecidableEq α] (p q : α → Prop) [inst : Fintype (Subtype p)] [DecidablePred q] : Fintype (Subtype (fun x => q x ∧ p x)) := { + elems := (inst.elems.filter (fun x => q x.val)).attach.image (fun x => ⟨x.val.val, by grind⟩) + complete := by + simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, Finset.mem_filter, + Subtype.forall, Subtype.mk.injEq, exists_prop, exists_and_right, exists_eq_right, and_imp] + intro a h1 h2 + and_intros + · use h2 + apply Fintype.complete + · exact h1 +} + +instance Set.instFintypeElemOfSubtype {α : Type} (p: α → Prop) [inst : Fintype {x // p x}] : Fintype ({x | p x}) := { + elems := inst.elems + complete := by + simp only [Set.coe_setOf, Subtype.forall] + intro a h + apply Fintype.complete +} + + +@[simp] +theorem Walk.append_getVert {V : Type} {G : SimpleGraph V} {u v w : V} + (w1 : G.Walk u v) (w2 : G.Walk v w) : (w1.append w2).getVert w1.length = v + := by simp [Walk.getVert_append] + +@[simp] +theorem Walk.take_append {V : Type} {G : SimpleGraph V} {u v w : V} + (w1 : G.Walk u v) (w2 : G.Walk v w) : + (w1.append w2).take w1.length = w1.copy rfl (by simp) := by + apply Walk.ext_support + rw [Walk.take_support_eq_support_take_succ, Walk.support_append] + simp + +@[simp] +theorem Walk.drop_append_of_length_eq {V : Type} {G : SimpleGraph V} {u v w : V} + (w1 : G.Walk u v) (w2 : G.Walk v w) : + (w1.append w2).drop w1.length = w2.copy (by simp) rfl := by + apply Walk.ext_support + rw [Walk.drop_support_eq_support_drop_min, Walk.support_append_eq_support_dropLast_append] + simp + + +theorem isTerminalWalk_copy {V : Type} {G : SimpleGraph V} {u v u' v' : V} (h1 : u = u') (h2 : v = v') (w : G.Walk u v) : isTerminalWalk w → isTerminalWalk (w.copy h1 h2) := by + unfold isTerminalWalk + intro h + simp [<-h2, h] + +theorem isTerminalWalk_map {V V' : Type} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (w : G.Walk u v) : + isTerminalWalk w → isTerminalWalk (w.map f.toHom) := by + unfold isTerminalWalk + intro h + simp + contrapose! h + rw [List.dropLast_eq_take, List.mem_take_iff_getElem] at h ⊢ + simp only [List.getElem_map, EmbeddingLike.apply_eq_iff_eq] at h + grind only [= List.length_map] + +theorem isTerminalWalk_of_isSubwalk {V : Type} {G : SimpleGraph V} {u u' t : V} {w : G.Walk u t} {w' : G.Walk u' t} (htw : isTerminalWalk w) (hsub : w'.IsSubwalk w) + : isTerminalWalk w' := by + unfold isTerminalWalk at htw ⊢ + rw [Walk.isSubwalk_iff_support_isInfix, List.IsInfix] at hsub + let ⟨ru, rv, h⟩ := hsub + rw [<-h, List.append_assoc, List.dropLast_append_of_ne_nil (by simp), List.dropLast_append] at htw + contrapose! htw + split_ifs with h + · exact List.mem_append_right ru htw + · apply List.mem_append_right + apply List.mem_append_left + exact Walk.end_mem_support w' + + +instance instDecidableIsTerminalWalk {V : Type} [DecidableEq V] {G : SimpleGraph V} {u v : V} : DecidablePred (fun (w : G.Walk u v) => isTerminalWalk w) := fun w => by + unfold isTerminalWalk + use inferInstance + + +abbrev C : Fin 8 := 2 +abbrev G : Fin 8 := 6 + +noncomputable def b (n : ℕ) := Set.ncard {w : Octagon.Walk C E | isTerminalWalk w ∧ w.length = n} + +def Octagon.mirror : Octagon ≃g Octagon := { + toFun x := -x + invFun x := -x + map_rel_iff' := by + intro a b + rw [Equiv.coe_fn_mk, Octagon, cycleGraph_adj', cycleGraph_adj'] + grind only [= Fin.val_sub] + left_inv := by simp [Function.LeftInverse.eq_1] + right_inv := by simp [Function.RightInverse.eq_1, Function.LeftInverse.eq_1] +} + +def C_G_symm (n : ℕ) : {w : Octagon.Walk C E // isTerminalWalk w ∧ w.length = n} ≃ {w : Octagon.Walk G E // isTerminalWalk w ∧ w.length = n} := { + toFun := fun ⟨w, h⟩ => ⟨(w.map Octagon.mirror.toHom).copy (by decide) (by decide), by { + and_intros + · apply isTerminalWalk_copy + apply isTerminalWalk_map + exact h.left + · simp [h.right] + }⟩ + invFun := fun ⟨w, h⟩ => ⟨(w.map Octagon.mirror.toHom).copy (by decide) (by decide), by { + and_intros + · apply isTerminalWalk_copy + apply isTerminalWalk_map + exact h.left + · simp [h.right] + }⟩ + left_inv := fun ⟨w, h⟩ => by + simp only [RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding, Walk.copy_rfl_rfl, + Walk.map_map, Subtype.mk.injEq] + apply Walk.ext_support + unfold Octagon.mirror + simp + right_inv := fun ⟨w, h⟩ => by + simp only [RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding, Walk.copy_rfl_rfl, + Walk.map_map, Subtype.mk.injEq] + apply Walk.ext_support + unfold Octagon.mirror + simp +} + +def isTerminalWalk_length_cons_equiv {V : Type} {G : SimpleGraph V} {u t : V} (m n : ℕ) (npos : 0 < n) : + {w : G.Walk u t // isTerminalWalk w ∧ w.length = m+n} ≃ Σ (v:V), {w : G.Walk u v // t ∉ w.support ∧ w.length = m} × {w : G.Walk v t // isTerminalWalk w ∧ w.length = n} + := { + toFun := fun ⟨w, h⟩ => ⟨w.getVert m, ⟨w.take m, by { + and_intros + · unfold isTerminalWalk at h + rw [Walk.take_support_eq_support_take_succ] + rw [List.dropLast_eq_take] at h + have : m+1 ≤ w.support.length - 1 := by + rw [Walk.length_support] + lia + have := List.take_subset_take_left w.support this + grind only [= List.subset_def] + · simp [h.right] + }⟩, ⟨w.drop m, by { + and_intros + · apply isTerminalWalk_of_isSubwalk h.left + exact Walk.isSubwalk_drop w m + · simp [h.right] + }⟩⟩ + invFun := fun ⟨v, ⟨⟨w1, h1⟩, ⟨w2, h2⟩⟩⟩ => ⟨w1.append w2, by { + and_intros + · unfold isTerminalWalk at h2 ⊢ + rw [Walk.support_append_eq_support_dropLast_append, List.dropLast_append_of_ne_nil (by simp), List.mem_append, not_or] + and_intros + · grind only [List.mem_of_mem_dropLast] + · exact h2.left + · simp [h1.right, h2.right] + }⟩ + left_inv := fun ⟨w, h⟩ => by + simp + right_inv := fun ⟨v, ⟨⟨w1, h1, h1'⟩, ⟨w2, h2, h2'⟩⟩⟩ => by + subst m n + simp only [Walk.take_append, Walk.drop_append_of_length_eq, Sigma.mk.injEq, + Walk.append_getVert, true_and] + congr! 1 + · rw [Walk.append_getVert] + · rw [Walk.append_getVert] + · congr! 1 + · simp + · rw [Walk.append_getVert] + · simp [Walk.copy] + · congr! 1 + · simp + · rw [Walk.append_getVert] + · simp [Walk.copy] + } + +theorem a_b_recurrence_1 (n : ℕ) (npos : 0 < n) : a (n+2) = 2 * a n + 2 * b n := by + have walks_from_A (v) : Fintype.card { w : Octagon.Walk A v // E ∉ w.support ∧ w.length = 2 } = + match v with + | 0 => 2 + | 2 => 1 + | 6 => 1 + | _ => 0 + := by + decide +revert + unfold a b + calc + _ = Fintype.card {w : Octagon.Walk A E // isTerminalWalk w ∧ w.length = 2 + n} := by + rw [Set.ncard_eq_toFinset_card', add_comm] + simp + _ = ∑ v ∈ {A,C,G}, Fintype.card {w : Octagon.Walk A v // E ∉ w.support ∧ w.length = 2} * Fintype.card {w : Octagon.Walk v E // isTerminalWalk w ∧ w.length = n} := by + rw [Fintype.card_eq.mpr (Nonempty.intro (isTerminalWalk_length_cons_equiv _ _ npos))] + rw [Fintype.card_sigma] + simp_rw [Fintype.card_prod] + rw [eq_comm, Finset.sum_subset] + · simp + · intro _ _ _ + apply mul_eq_zero_of_left + decide +revert + _ = _ := by + repeat rw [Finset.sum_insert (by decide)] + rw [Finset.sum_singleton] + repeat rw [walks_from_A] + simp only [Set.ncard_eq_toFinset_card', Set.toFinset_card, Set.coe_setOf] + rw [<-Fintype.card_eq.mpr (Nonempty.intro (C_G_symm _))] + lia + +theorem a_b_recurrence_2 (n : ℕ) (npos : 0 < n) : b (n+2) = a n + 2 * b n := by + have walks_from_C (v) : Fintype.card { w : Octagon.Walk C v // E ∉ w.support ∧ w.length = 2 } = + match v with + | 0 => 1 + | 2 => 2 + | _ => 0 + := by + decide +revert + unfold a b + calc + _ = Fintype.card {w : Octagon.Walk C E // isTerminalWalk w ∧ w.length = 2 + n} := by + rw [Set.ncard_eq_toFinset_card', add_comm] + simp + _ = ∑ v ∈ {A,C}, Fintype.card {w : Octagon.Walk C v // E ∉ w.support ∧ w.length = 2} * Fintype.card {w : Octagon.Walk v E // isTerminalWalk w ∧ w.length = n} := by + rw [Fintype.card_eq.mpr (Nonempty.intro (isTerminalWalk_length_cons_equiv _ _ npos))] + rw [Fintype.card_sigma] + simp_rw [Fintype.card_prod] + rw [eq_comm, Finset.sum_subset] + · simp + · intro _ _ _ + apply mul_eq_zero_of_left + decide +revert + _ = _ := by + repeat rw [Finset.sum_insert (by decide)] + rw [Finset.sum_singleton] + repeat rw [walks_from_C] + simp only [Set.ncard_eq_toFinset_card', Set.toFinset_card, Set.coe_setOf] + lia + + +theorem a_even (n : ℕ) (npos : 0 < n) : a (2*n) = ((2+√2)^(n-1) - (2-√2)^(n-1)) / √2 := by + suffices a (2*n) = ((2+√2)^(n-1) - (2-√2)^(n-1)) / √2 ∧ b (2*n) = ((2+√2)^(n-1) + (2-√2)^(n-1)) / 2 by exact this.left + revert n + apply Nat.le_induction + · unfold a b + simp [Set.ncard_eq_toFinset_card'] + decide + · intro n npos ih + rw [mul_add, mul_one] + rw [show n + 1 - 1 = (n - 1 + 1) by lia] + repeat rw [pow_succ] + and_intros + · rw [a_b_recurrence_1 _ (by lia)] + rw [Nat.cast_add, Nat.cast_mul, Nat.cast_mul, ih.left, ih.right] + field + · rw [a_b_recurrence_2 _ (by lia)] + rw [Nat.cast_add, Nat.cast_mul, ih.left, ih.right] + generalize (2+√2)^(n-1) = α, (2-√2)^(n-1) = β + simp only [Nat.cast_ofNat] + field_simp + rw [show 2 * (α - β + √2 * (α + β)) = √2 * (2+√2) * α + √2 * (2-√2) * β by grind] + field + + +theorem walk_even (w : Octagon.Walk A E) : Even w.length := by + let coloring := cycleGraph.bicoloring_of_even 8 (by simp [Nat.even_iff]) + rw [coloring.even_length_iff_congr] + decide + +theorem a_odd (n : ℕ) (npos : 0 < n) : a (2*n-1) = 0 := by + unfold a + rw [Set.ncard_eq_toFinset_card', Finset.card_eq_zero] + apply Finset.eq_empty_of_forall_notMem + intro w + have := walk_even w + grind only [= Nat.even_iff, = Set.mem_toFinset, usr Set.mem_setOf_eq] + +snip end + + +problem imo1979_p6 (n : ℕ) (npos : 0 < n) : a (2*n-1) = 0 ∧ a (2*n) = ((2+√2)^(n-1) - (2-√2)^(n-1)) / √2 := by + and_intros + · exact a_odd n npos + · exact a_even n npos + +end Imo1979P6 From 55cb723996aa215ebf652228875f3b871fd634ea Mon Sep 17 00:00:00 2001 From: urinstinkt <83813265+urinstinkt@users.noreply.github.com> Date: Sun, 1 Mar 2026 21:39:06 +0100 Subject: [PATCH 2/2] Rename Imo1979P2.lean to Imo1979P6.lean --- Compfiles/{Imo1979P2.lean => Imo1979P6.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename Compfiles/{Imo1979P2.lean => Imo1979P6.lean} (100%) diff --git a/Compfiles/Imo1979P2.lean b/Compfiles/Imo1979P6.lean similarity index 100% rename from Compfiles/Imo1979P2.lean rename to Compfiles/Imo1979P6.lean