-- Homework 5
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Due: Oct 22, 2026
--
-- Group members (up to 3):
-- _______________________
-- _______________________
-- _______________________
--
-- ============================================================
-- The tasks are labelled [Foundations], [Proficiency], and
-- [Mastery]. See Homework 1 for the instructions.
--
-- Use proof terms, not tactics.
--
-- ============================================================

set_option autoImplicit false
set_option linter.unusedVariables false
set_option inductive.autoPromoteIndices false

namespace Homework5

-- ============================================================
-- 1. [Foundations] Recall that the Lean kernel doesn't know any
--    logic, and even the most basic concepts like "and" and "or" must
--    have their inductive types taught to the kernel. Some of these
--    are redefined below.

namespace Logic

inductive And (p q : Prop) : Prop where
  | intro : p → q → And p q

inductive Or (p q : Prop) : Prop where
  | inl : p → Or p q
  | inr : q → Or p q

inductive False : Prop where

inductive Exists {A : Type} (P : A → Prop) : Prop where
  | intro : (w : A) → P w → Exists P

local infixr:35 (priority := high) " ∧ " => And
local infixr:30 (priority := high) " ∨ " => Or

-- Now prove the following assertions. Feel free to use the infixes
-- above.

-- 1.1
theorem And.left {p q : Prop} : p ∧ q → p :=
  sorry

-- 1.2
theorem And.right {p q : Prop} : p ∧ q → q :=
  sorry

-- 1.3 (This was left as an exercise in Lecture 10.)
theorem Or.elim {p q r : Prop} : p ∨ q → (p → r) → (q → r) → r :=
  sorry

-- 1.4
theorem False.elim {p : Prop} : False → p :=
  sorry

-- In the standard library, `∃ x, P x` is notation for
-- `Exists (fun x => P x)`. To avoid clashing with that notation, we
-- write `Exists` explicitly below.

-- 1.5
example : Exists (fun n : Nat => n + n = 4) :=
  sorry

-- 1.6 This is the elimination rule for `Exists`. (This was left as
-- an exercise in Lecture 11.)
theorem Exists.elim {A : Type} {P : A → Prop} {q : Prop} :
    Exists P → ((x : A) → P x → q) → q :=
  sorry

-- 1.7 [Proficiency]
theorem exists_and {A : Type} {P Q : A → Prop} :
    Exists (fun x => P x ∧ Q x) → Exists P ∧ Exists Q :=
  sorry

-- 1.8 [Proficiency] The converse of 1.7 is false. To show this,
-- prove the following two statements.
theorem exists_and_exists :
    Exists (fun x : Bool => x = true) ∧ Exists (fun x : Bool => x = false) :=
  sorry

theorem not_exists_and : ¬ Exists (fun x : Bool => x = true ∧ x = false) :=
  sorry

end Logic

-- ============================================================
-- 2. [Foundations] Define an inductive type `Odd` that detects odd
--    numbers, analogous to the type `Even` that we saw in class.

inductive Odd : (n : Nat) → Prop where
  -- your constructors go here

-- Now prove the following propositions.

-- 2.1
theorem nine_odd : Odd 9 :=
  sorry

-- 2.2
theorem four_not_odd : ¬Odd 4 :=
  sorry

-- 2.3
theorem remove_two {n : Nat} : Odd (n + 2) → Odd n :=
  sorry

-- 2.4
theorem add_four {n : Nat} : Odd n → Odd (n + 4) :=
  sorry

-- 2.5 [Proficiency] In class, we proved that
-- `Even (n + 2) → Even n`. One might try to state a similar property
-- using subtraction instead, as `∀ n, Even n → Even (n - 2)`. Perhaps
-- surprisingly, this statement is also provable, by the following
-- proof:

--    fun n => fun h => match h with
--    | base => base
--    | step hm' => hm'

-- The reason is that subtraction of natural numbers in Lean is
-- "truncated": if `m > n`, then `n - m = 0`. For example:

#eval 1 - 2     --> 0

-- So in the `base` case, the goal is `Even (0 - 2)`, which is the
-- same as `Even 0`. However, the analogous statement for `Odd` is
-- false. Prove this.
theorem odd_sub_two_false : ¬ ∀ n, Odd n → Odd (n - 2) :=
  sorry

-- ============================================================
-- 3. In this question you will prove some propositions relating
--    `Odd` to the inductive type `Even` from class, which we recall
--    below.

namespace Parity
open Odd

inductive Even : (n : Nat) → Prop where
  | base : Even 0
  | step : ∀ {n : Nat}, Even n → Even (n + 2)

-- 3.1 [Foundations]
theorem even_to_odd : ∀ {n : Nat}, Even n → Odd (n + 1) :=
  sorry

-- 3.2 [Foundations]
theorem odd_to_even : ∀ {n : Nat}, Odd n → Even (n + 1) :=
  sorry

-- 3.3 [Proficiency]
theorem odd_add_odd : ∀ {n m : Nat}, Odd n → Odd m → Even (n + m) :=
  sorry

-- 3.4 [Proficiency] Having `Even`, one could also define odd numbers
-- like this:

inductive Udd : Nat → Prop where
  | intro {n : Nat} : Even n → Udd (n + 1)

-- Prove that `Udd` is equivalent to `Odd`:

theorem odd_udd : ∀ n : Nat, Odd n ↔ Udd n :=
  sorry

-- 3.5 [Proficiency] Prove that every number is even or odd.
theorem even_or_odd : ∀ (n : Nat), Even n ∨ Odd n :=
  sorry

-- 3.6 [Proficiency] Prove that no number is both even and odd.
theorem not_even_and_odd : ∀ (n : Nat), ¬ (Even n ∧ Odd n) :=
  sorry

-- 3.7 [Proficiency] The following two theorems were left as an
-- exercise in Lecture 10. Hint: prove the first one by induction on
-- `k`, but the second one by induction on the predicate `Even n`.
-- Remember that when you do a proof by induction, you must remove
-- the `:=` as well as the `sorry`.
theorem k2_is_even : ∀ (n : Nat), (∃ k, n = 2 * k) → Even n :=
  sorry

theorem even_is_2k : ∀ (n : Nat), Even n → (∃ k, n = 2 * k) :=
  sorry

-- 3.8 [Proficiency] Now do the same for odd numbers.
theorem odd_iff_double : ∀ n : Nat, Odd n ↔ ∃ k, n = 2 * k + 1 :=
  sorry

end Parity

-- ============================================================
-- 4. Parameters and indices.
--
-- Recall from Lecture 10: in an inductive definition, a _parameter_
-- is fixed throughout the definition, and is written to the left of
-- the main `:`. An _index_ can vary, and is written to the right of
-- the main `:`. In this question, you will practice choosing between
-- the two. (The option `inductive.autoPromoteIndices false` at the
-- top of this file stops Lean from silently turning indices into
-- parameters.)

namespace Arguments

-- 4.1 [Foundations] Compare these two declarations. In the first
-- one, the number `n` is a parameter: it is just a label, which
-- stays the same throughout the definition. In the second one, `n`
-- is an index: it counts the number of steps.

inductive LabeledChain (n : Nat) : Type where
  | base : LabeledChain n
  | step : LabeledChain n → LabeledChain n

inductive CountedChain : Nat → Type where
  | base : CountedChain 0
  | step {n : Nat} : CountedChain n → CountedChain (n + 1)

-- Construct each value using two applications of `step` to `base`.
def labeledTwo : LabeledChain 2 :=
  sorry

def countedTwo : CountedChain 2 :=
  sorry

-- Now construct a value of `LabeledChain 2` that uses three
-- applications of `step`. Can you do the same for `CountedChain 2`?
def labeledThree : LabeledChain 2 :=
  sorry

-- In each of the following questions, you are given an informal
-- definition, in the form of inference rules. Write the inductive
-- definition in Lean. Use the names given for the type and its
-- constructors. Make as many arguments as possible parameters, and
-- only use indices where necessary. Then uncomment the examples to
-- check that your definition works.

-- 4.2 [Foundations] Vectors. For a type `A` and a natural number
-- `n`, the type `Vec A n` consists of lists of elements of `A` of
-- length exactly `n`. It is defined by these rules:
--
--                                x : A     v : Vec A n
--  ──────────────── (nil)      ─────────────────────── (cons)
--   nil : Vec A 0                cons x v : Vec A (n + 1)
--
-- YOUR CODE HERE.

-- example : Vec Bool 2 := .cons true (.cons false .nil)

-- 4.3 [Proficiency] One advantage of indices is that Lean can
-- sometimes tell that a case is impossible. Define the function
-- that returns the first element of a non-empty vector. Note that
-- there is no need to handle the `nil` case. Why not? Then define
-- the conversion to lists, and prove that it gives a list of the
-- correct length. (Uncomment when you have defined `Vec`.)

-- def Vec.head {A : Type} {n : Nat} : Vec A (n + 1) → A :=
--   sorry

-- def Vec.toList {A : Type} {n : Nat} : Vec A n → List A :=
--   sorry

-- theorem Vec.length_toList {A : Type} {n : Nat} (v : Vec A n) :
--     v.toList.length = n :=
--   sorry

-- 4.4 [Foundations] Less-than-or-equal. Here is one way to define
-- the relation `n ≤ m` on natural numbers. (In fact, this is how the
-- standard library defines it.)
--
--                               Le n m
--  ────────── (refl)        ──────────────── (step)
--   Le n n                    Le n (m + 1)
--
-- YOUR CODE HERE.

-- example : Le 2 4 := .step (.step .refl)

-- 4.5 [Foundations] Here is a different way to define the same
-- relation.
--
--                                Le' n m
--  ─────────── (zero)       ────────────────────── (succ)
--   Le' 0 m                  Le' (n + 1) (m + 1)
--
-- YOUR CODE HERE.

-- example : Le' 2 4 := .succ (.succ .zero)

-- 4.6 [Foundations] Reachability. Given a type `A`, a relation
-- `R : A → A → Prop`, and an element `a : A`, we say that `b` is
-- reachable from `a` if `b` can be reached from `a` in zero or more
-- `R`-steps:
--
--                                   Reach R a b     R b c
--  ───────────────── (refl)      ───────────────────────── (step)
--   Reach R a a                        Reach R a c
--
-- YOUR CODE HERE.

-- example : Reach (fun m n : Nat => n = m + 1) 0 3 :=
--   .step (.step (.step .refl rfl) rfl) rfl

-- 4.7 [Mastery] Prove that the two definitions of `≤` agree. You will
-- need several lemmas, for example that `Le' n n` holds for all `n`,
-- and that `Le' n m` implies `Le' n (m + 1)`.

-- theorem le_iff_le' : ∀ n m : Nat, Le n m ↔ Le' n m :=
--   sorry

end Arguments

-- ============================================================
-- 5. Constructing monoids.

namespace Monoid

-- Recall from Lecture 11 that `structure` defines an inductive type
-- with only one constructor. A monoid structure on a type `A`
-- consists of a binary operation, an identity, and proofs of
-- associativity and the two identity laws. Note that, unlike the
-- groups from Lecture 11 (see Question 6), this definition is
-- _unbundled_: the type `A` is a parameter, not a field.

structure Monoid (A : Type) where
  mul : A → A → A
  one : A
  mul_assoc : ∀ a b c : A, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a : A, mul one a = a
  mul_one : ∀ a : A, mul a one = a

-- Lean automatically supplies projections for structures:
#check Monoid.mul
#check Monoid.one
#check Monoid.mul_assoc

-- 5.1 [Proficiency] Construct a monoid for `Nat` under addition.
-- Available lemmas: `Nat.add_assoc`, `Nat.zero_add`, `Nat.add_zero`.
def additionMonoid : Monoid Nat :=
  sorry

-- 5.2 [Proficiency] Construct a monoid for lists under append.
-- Available lemmas: `List.append_assoc`, `List.nil_append`,
-- `List.append_nil`.
def listMonoid (A : Type) : Monoid (List A) :=
  sorry

-- 5.3 [Mastery] Given monoids on `A` and `B`, construct a monoid on
-- `A × B`, multiplying the components separately. Its identity
-- should be the pair of the two identities. (Hint: if Lean has
-- trouble recognizing that an equation has the form you expect, you
-- can restate the goal using `show ... from ...`, as in Lecture 6.)
def productMonoid {A B : Type} (M : Monoid A) (N : Monoid B) : Monoid (A × B) :=
  sorry

-- Use this construction to combine addition and list append.
def countAndList : Monoid (Nat × List Bool) :=
  sorry
example : countAndList.mul (2, [true]) (3, [false, true]) = (5, [true, false, true]) :=
  sorry

-- 5.4 [Mastery] Given a monoid `M` with multiplication `*`, we can
-- define another monoid structure `*'` on the same type, by
-- `a *' b = b * a`, with the same identity. It is called the
-- _opposite_ monoid. Define it.
def opposite {A : Type} (M : Monoid A) : Monoid A :=
  sorry

-- Taking the opposite twice should give back the original monoid.
-- Prove this. (If your definition of `opposite` is the expected one,
-- this proof is very short.)
theorem opposite_opposite {A : Type} (M : Monoid A) : opposite (opposite M) = M :=
  sorry

-- 5.5 [Proficiency] For any type `A`, the functions `A → A` form a
-- monoid under composition. Construct it. The identity should be
-- the identity function.
def functionMonoid (A : Type) : Monoid (A → A) :=
  sorry

-- 5.6 [Mastery] The identity of a monoid is unique: if `e` is any
-- element that acts as a left identity, then `e` is equal to
-- `M.one`.
theorem one_unique {A : Type} (M : Monoid A) (e : A) (h : ∀ a, M.mul e a = a) :
    e = M.one :=
  sorry

end Monoid

-- ============================================================
-- 6. Groups.
--
-- In Lecture 11, we defined groups as a bundled structure, and left
-- some exercises. Here they are again.

namespace Bundled

structure Group where
  carrier : Type
  mul : carrier → carrier → carrier
  one : carrier
  inv : carrier → carrier
  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a, mul one a = a
  inv_mul : ∀ a, mul (inv a) a = one

local infixl:70 " * " => Group.mul _
local postfix:max "⁻¹" => Group.inv _

-- 6.1 [Foundations] Define the 1-element group. Its carrier is the
-- type `Unit`, whose unique element is called `()`.
def trivialGroup : Group where
  carrier := Unit
  mul := sorry
  one := sorry
  inv := sorry
  mul_assoc := sorry
  one_mul := sorry
  inv_mul := sorry

-- 6.2 [Proficiency] Prove the left cancellation law.
theorem left_cancel : ∀ (G : Group) (a b c : G.carrier),
    (a * b = a * c) → b = c :=
  sorry

-- 6.3 [Mastery] Prove that the three laws (associativity, left unit,
-- and left inverse) are sufficient to axiomatize groups. In
-- particular, prove the right inverse law and the right unit law.
-- Hint: prove the right inverse law first, and use it to prove the
-- right unit law. For the right inverse law, it may help to multiply
-- `a * a⁻¹` on the left by a cleverly chosen expression equal to
-- `G.one`.
theorem mul_inv : ∀ (G : Group) (a : G.carrier), a * a⁻¹ = G.one :=
  sorry

theorem mul_one : ∀ (G : Group) (a : G.carrier), a * G.one = a :=
  sorry

end Bundled
end Homework5

-- ============================================================
-- Investigations: for each investigation, state what you tried,
-- what you found, and what remains unresolved.

-- ============================================================
-- Investigation A: incidence geometry
-- ------------------------------------------------------------
-- In Euclid's geometry, and in Hilbert's modern axiomatization of
-- it, the most basic notions are points, lines, and the relation
-- "the point `p` lies on the line `l`". The following _incidence
-- axioms_ describe how these notions interact:
--
--   (I1) For any two distinct points, there exists a line through
--        both of them.
--   (I2) This line is unique.
--   (I3) Every line contains at least two distinct points, and there
--        exist three points that do not all lie on one line.
--
-- An _incidence geometry_ is a set of points, a set of lines, and an
-- incidence relation satisfying these axioms. Just like the bundled
-- groups from Lecture 11, we can define it as a structure:

namespace Geometry

structure IncidenceGeometry where
  Point : Type
  Line : Type
  On : Point → Line → Prop
  line_through : ∀ p q : Point, p ≠ q → ∃ l : Line, On p l ∧ On q l
  line_unique : ∀ (p q : Point) (l m : Line),
    p ≠ q → On p l → On q l → On p m → On q m → l = m
  two_points : ∀ l : Line, ∃ p q : Point, p ≠ q ∧ On p l ∧ On q l
  three_points : ∃ p q r : Point,
    p ≠ q ∧ p ≠ r ∧ q ≠ r ∧ ¬ ∃ l : Line, On p l ∧ On q l ∧ On r l

-- A.1 Prove the following theorem, which holds in every incidence
-- geometry: two distinct lines have at most one point in common.
theorem at_most_one_common_point (G : IncidenceGeometry) (l m : G.Line) (p q : G.Point) :
    l ≠ m → p ≠ q → G.On p l → G.On q l → G.On p m → G.On q m → False :=
  sorry

-- A.2 Of course, Euclidean geometry is an incidence geometry. But
-- there are also much smaller ones. The smallest one has three
-- points `a`, `b`, `c` and three lines: one through each pair of
-- points (picture a triangle). Construct it. Hints: it is
-- convenient to use the same type for points and lines, naming each
-- line after the vertex opposite to it. Then a point lies on a line
-- if and only if the two are different. You will also need a
-- function that, given two distinct vertices, returns the third one,
-- and some lemmas about it. To prove that two concrete vertices are
-- different, you can use `nofun`, which is short for
-- `fun h => nomatch h`.

inductive Vertex : Type where
  | a | b | c

def triangle : IncidenceGeometry :=
  sorry

-- A.3 Two lines are _parallel_ if they have no point in common. The
-- following is Playfair's version of Euclid's parallel postulate:
-- given a line `l` and a point `p` not on `l`, there exists a line
-- through `p` that is parallel to `l`. (It is usually also stated
-- that this line is unique, but we will not need this.)

def Parallel (G : IncidenceGeometry) (l m : G.Line) : Prop :=
  ¬ ∃ p : G.Point, G.On p l ∧ G.On p m

def Playfair (G : IncidenceGeometry) : Prop :=
  ∀ (l : G.Line) (p : G.Point), ¬ G.On p l → ∃ m : G.Line, G.On p m ∧ Parallel G l m

-- Prove that the parallel postulate fails in the triangle geometry.
-- It follows that the parallel postulate cannot be derived from the
-- incidence axioms. Why?
theorem triangle_not_playfair : ¬ Playfair triangle :=
  sorry

-- ANSWER:

-- A.4 Explore further. Here are some suggestions; pick one or more,
-- or come up with your own.
--
--   * The smallest incidence geometry in which Playfair's postulate
--     holds has 4 points and 6 lines. Construct it and prove that it
--     satisfies the postulate.
--   * In the _Fano plane_, every two distinct lines meet in exactly
--     one point. It has 7 points and 7 lines. Construct it.
--   * Show that the incidence axioms do not determine the number of
--     points, or the number of points on a line.
--   * Instead of a separate type of lines, one could represent a line
--     by two distinct points on it. But then different pairs of
--     points can represent the same line. Explore how to deal with
--     this, for example by defining when two such representations
--     should count as the same line.
--
-- Hint: the more points and lines your model has, the more cases you
-- need to consider. Try to organize your proofs to keep the number of
-- cases manageable, e.g., by proving suitable lemmas first.
-- REPORT:

end Geometry

-- ============================================================
-- Investigation B: dependent pairs
-- ------------------------------------------------------------
-- Lean has several types whose elements are "dependent pairs"
-- `⟨x, y⟩`, where the type of the second component `y` depends on the
-- first component `x`:
--
--   * `∃ x : A, P x`       (`Exists`; you defined it in Question 1)
--   * `{x : A // P x}`     (subtypes; we used them in Homework 3)
--   * `Σ x : A, B x`       (Sigma types)
--   * `Σ' x : A, B x`      (a variant of Sigma types)
--
-- Here, `P : A → Prop` is a predicate, whereas `B : A → Type` is a
-- family of types. (Lean prints `Σ x : A, B x` as `(x : A) × B x`,
-- and `Σ'` as `×'`.) In this investigation, you will find out what
-- these types have in common, and how they differ.

namespace DependentPairs

-- B.1 Construct an element of each of the following types. Then use
-- `#check` to find out which universe each type lives in, and record
-- the answer. Also find out what `B` is allowed to be in `Σ` and in
-- `Σ'`: can it return a `Prop`? A `Type`? A `Type 1`?

example : ∃ n : Nat, n + n = 6 :=
  sorry

example : {n : Nat // n + n = 6} :=
  sorry

example : Σ' n : Nat, n + n = 6 :=
  sorry

example : Σ A : Type, A :=
  sorry

-- Here is a more interesting Sigma type. An element of
-- `Σ n : Nat, BoolList n` is a natural number `n`, together with a
-- list of booleans of length `n`.

def BoolList (n : Nat) : Type := {l : List Bool // l.length = n}

example : Σ n : Nat, BoolList n :=
  sorry

-- REPORT:

-- B.2 Subtypes and `Σ'` types are almost the same thing. Construct
-- maps in both directions, and prove that they are inverse to each
-- other.

def toPSigma {A : Type} {P : A → Prop} : {x : A // P x} → Σ' x : A, P x :=
  sorry

def ofPSigma {A : Type} {P : A → Prop} : (Σ' x : A, P x) → {x : A // P x} :=
  sorry

theorem ofPSigma_toPSigma {A : Type} {P : A → Prop} (a : {x : A // P x}) :
    ofPSigma (toPSigma a) = a :=
  sorry

theorem toPSigma_ofPSigma {A : Type} {P : A → Prop} (a : Σ' x : A, P x) :
    toPSigma (ofPSigma a) = a :=
  sorry

-- B.3 Every element of a subtype gives rise to a proof of an
-- existential statement. Prove this.

theorem toExists {A : Type} {P : A → Prop} : {x : A // P x} → ∃ x, P x :=
  sorry

-- What about the converse? The obvious definition does not work; try
-- it, and record the error message. Then define the converse anyway,
-- using the axiom of choice as in Homework 3.

noncomputable def ofExists {A : Type} {P : A → Prop} (h : ∃ x, P x) : {x : A // P x} :=
  sorry

-- REPORT:

-- B.4 Why can't we extract the witness from a proof of `∃ x, P x`?
-- Here is the reason. Because all proofs of a proposition are equal
-- (proof irrelevance), the following holds by `rfl`, even though the
-- two proofs use different witnesses:

theorem exists_proofs_equal : (⟨0, trivial⟩ : ∃ n : Nat, True) = ⟨1, trivial⟩ :=
  rfl

-- Use this to show that there is no function that extracts the
-- witness.

theorem no_witness (w : (∃ n : Nat, True) → Nat) (hw : ∀ n h, w ⟨n, h⟩ = n) :
    False :=
  sorry

-- B.5 For subtypes, the second component is a proof, so by proof
-- irrelevance, two elements are equal as soon as their first
-- components are equal. Prove this.

theorem subtype_ext {A : Type} {P : A → Prop} :
    ∀ a b : {x : A // P x}, a.val = b.val → a = b :=
  sorry

-- For `Σ` types, this is not true. Prove it.

theorem sigma_not_ext :
    (⟨2, ⟨[true, false], rfl⟩⟩ : Σ n : Nat, BoolList n) ≠ ⟨2, ⟨[false, true], rfl⟩⟩ :=
  sorry

-- B.6 Summarize your findings in a table: for each of the four kinds
-- of dependent pairs, state which universe it lives in, what the
-- second component can be, whether you can project out the first and
-- second components, and when two elements are equal.
-- REPORT:

end DependentPairs

-- ============================================================
-- Investigation C: race to one
-- ------------------------------------------------------------
-- Here is a one-player game. Start at a positive integer. On each
-- turn, the player chooses one of the following legal moves:
--   * subtract one, if the number is greater than 1;
--   * divide by two, if the number is divisible by two;
--   * divide by three, if the number is divisible by three.
-- Subtraction is still an option when division is available.
-- The goal is to reach 1, where the game ends, in as few moves as
-- possible.
--
-- For example, starting from 10, one could play 10 → 5 → 4 → 2 → 1
-- (4 moves). Can you do better?

namespace RaceToOne

-- `Path n k` records a play from `n` to 1 in exactly `k` moves.
-- Each constructor prepends a move to an already built play.
inductive Path : Nat → Nat → Type where
  | done : Path 1 0
  | minus_one {n k : Nat} : Path (n + 1) k → Path (n + 2) (k + 1)
  | div_two {n k : Nat} : 0 < n → Path n k → Path (2 * n) (k + 1)
  | div_three {n k : Nat} : 0 < n → Path n k → Path (3 * n) (k + 1)

-- Note that `Path n k` is a `Type`, not a `Prop`: a path is data,
-- and different paths are different. Two hints for constructing
-- paths:
--
--   * Lean cannot figure out by itself that, e.g., `9 = 3 * n` means
--     `n = 3`. You can tell it by giving the implicit argument
--     explicitly: `Path.div_three (n := 3) ...`.
--   * To prove inequalities between concrete numbers, such as
--     `0 < 3`, you can use `Nat.le_of_ble_eq_true rfl`.

-- C.1 Construct the play from 10 to 1 shown above, and then a play
-- from 10 to 1 in exactly three moves.
def playTenSlow : Path 10 4 :=
  sorry

def playTen : Path 10 3 :=
  sorry

-- C.2 Show that every positive starting number has a play to 1.
def countdown : (n : Nat) → Path (n + 1) n :=
  sorry

-- To say that a play is the best possible, we use a structure (see
-- Lecture 11). An element of `Shortest n` consists of three things:
-- a number `length`, a play from `n` of that length, and a proof that
-- no play from `n` is shorter.
structure Shortest (n : Nat) where
  length : Nat
  path : Path n length
  optimal : ∀ k : Nat, Path n k → length ≤ k

-- For the optimality proofs, these two facts are provided.
theorem zero_start : ∀ {n : Nat}, Path n 0 → n = 1
  | _, Path.done => rfl

theorem one_step_start : ∀ {n : Nat}, Path n 1 → n = 2 ∨ n = 3
  | _, @Path.minus_one 0 _ q => Or.inl rfl
  | _, @Path.minus_one (n + 1) _ q => nomatch (zero_start q)
  | _, Path.div_two hn q => match q with | Path.done => Or.inl rfl
  | _, Path.div_three hn q => match q with | Path.done => Or.inr rfl

-- C.3 Construct `Shortest 2`. (Hint: for the optimality proof, do a
-- case distinction on `k`.)
def shortestTwo : Shortest 2 :=
  sorry

-- C.4 Construct a two-move play from 4, then prove that no play
-- from 4 has fewer moves.
-- The two supplied lemmas rule out lengths 0 and 1.
-- Useful lemma: `Nat.le_add_left 2 k : 2 ≤ k + 2`.
def playFour : Path 4 2 :=
  sorry

theorem four_minimum : ∀ k : Nat, Path 4 k → 2 ≤ k :=
  sorry

-- C.5 Prove that your play from C.1 is the best possible. To do so,
-- you will first need to know which numbers can reach 1 in exactly
-- two moves. Use `one_step_start` to prove this.
theorem two_step_start : ∀ {n : Nat}, Path n 2 → n = 3 ∨ n = 4 ∨ n = 6 ∨ n = 9 :=
  sorry

def shortestTen : Shortest 10 :=
  sorry

-- C.6 A natural strategy for this game is the _greedy_ strategy:
-- divide by three if you can; otherwise, divide by two if you can;
-- otherwise, subtract one. The play 10 → 5 → 4 → 2 → 1 is the greedy
-- play from 10, and C.5 shows that greedy play is not always
-- optimal. Find another starting number for which greedy play is
-- not optimal. Construct the greedy play from that number and a
-- shorter play, and prove that your shorter play is optimal. What
-- extra lemmas did you need?
--
-- If you want to go further: can you find a better strategy, i.e.,
-- a simple rule for choosing the next move that always leads to a
-- shortest play? Test it on many numbers. (You do not need to prove
-- that your strategy is optimal; but if you can, even better.)

end RaceToOne