-- Homework 4
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Due: Thursday, October 15.
--
-- Group members (up to 3):
-- _______________________
-- _______________________
-- _______________________
--
-- ============================================================
-- The tasks below are labelled [Foundations], [Proficiency], and
-- [Mastery]. See Homework 1 for the instructions.
-- ============================================================

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

namespace Homework4

-- ============================================================
-- 1. [Foundations] Fill every `sorry` below. Do not use tactics. You
-- may use `rfl`, the equality rules from Lecture 8, and basic
-- arithmetic lemmas in `Nat`. You can type `Nat.` to get a popup
-- menu and explore the available lemmas. You do not need induction
-- or any arithmetic automation.

section
  variable (a b c d : Nat)

  -- 1.1
  example : a + b = c → b + a = c :=
    sorry

  -- 1.2
  example : a * 1 + 0 * b = a :=
    sorry

  -- 1.3
  example : a = b + c → a * d = b * d + c * d :=
    sorry

  -- 1.4
  example : a + b + c = a + (c + b) :=
    sorry

  -- 1.5
  example : (a + b) + c = (b + a) + c :=
    sorry

  -- 1.6 There is a single lemma in `Nat` that proves this in one
  -- step. Don't use it! Build the proof out of `Nat.mul_assoc` and
  -- `Nat.mul_comm` instead. (You will revisit this one in 5.4.)
  example : a * (b * c) = b * (a * c) :=
    sorry

  -- 1.7 Hint: `a ^ 2` is notation for `Nat.pow a 2`. Look for the
  -- lemmas that describe how `Nat.pow` behaves.
  example : a ^ 2 = a * a :=
    sorry

  -- 1.8
  example : a + c = c + b → a = b :=
    sorry

  -- 1.9
  example : ∃ n : Nat, a + b + n = a + (b + c) :=
    sorry

  -- 1.10
  example : (∀ n : Nat, a + n = n + b) ↔ a = b :=
    sorry

end

-- ============================================================
-- 2. [Proficiency] Fill each `sorry` below. Do not use tactics. Your
-- proofs must use `Eq.subst` with an explicit `motive := ...`
-- instead of using `Eq.symm`, `Eq.trans` and other theorems from
-- `Eq`. (In Lecture 8 we proved symmetry this way; 2.1 is the
-- exercise that was left over from that lecture.)

section
  variable {A B : Type} {a b c : A} {P : A → Prop}

  -- 2.1
  example : a = b → b = c → a = c :=
    sorry

  -- 2.2
  example (n m : Nat) (h : n = m) : m + 1 = n + 1 :=
    sorry

  -- 2.3
  example (R : A → B → Prop) :
      a = b → (∀ y : B, R a y) → ∀ y : B, R b y :=
    sorry

  -- 2.4
  example : (∃ x : A, x = a ∧ P x) ↔ P a :=
    sorry

end

-- ============================================================
-- 3. Equational reasoning from hypotheses.
--
-- In each item below, you are given some equations as hypotheses, and
-- you must derive another equation from them. Write each proof as a
-- single `calc` block. You may use `Eq.symm` and `Eq.trans` freely
-- here, as well as `congrArg` and the lemmas in `Nat`.
--
-- Style note: a `calc` proof is meant to be *readable*. Each step
-- should be one identifiable move -- apply a hypothesis, apply one
-- arithmetic lemma, rewrite one subterm -- so that a person can check
-- the chain line by line.

section
  variable (x y z : Nat)

  -- 3.1 [Foundations]
  example : (x = y + 1) → (y = z * z) → (x = z * z + 1) :=
    sorry

  -- 3.2 [Foundations]
  example : (x = 2 * x - 1) → x = 2 * (2 * x - 1) - 1 :=
    sorry

  -- 3.3 [Proficiency]
  example (a b : Nat) : (a + 1) * (b + 1) = a * b + a + b + 1 :=
    sorry

  -- 3.4 [Proficiency]
  example (h1 : x + y = 10) (h2 : y = 2 * x) : 3 * x = 10 :=
    sorry

  -- 3.5 [Proficiency] Here the hypothesis `h` is itself a universally
  -- quantified equation, so you can use it at as many values of `n` as
  -- you like.
  example (f : Nat → Nat) (h0 : f 0 = 1) (h : ∀ n : Nat, f (n + 1) = f n + 2) :
      f 3 = 7 :=
    sorry

  -- 3.6 [Proficiency] This one is a theorem of algebra in disguise:
  -- `m` is an associative operation with unit `e`, the element `b` is
  -- a right inverse of `a`, and `c` is a right inverse of `b`. Show
  -- that `a = c`. (In other words, inverses are unique.) Notice that
  -- your proof uses nothing about the natural numbers -- only the five
  -- hypotheses.
  example (m : Nat → Nat → Nat) (e : Nat) (a b c : Nat)
      (assoc : ∀ x y z : Nat, m (m x y) z = m x (m y z))
      (unitl : ∀ x : Nat, m e x = x)
      (unitr : ∀ x : Nat, m x e = x)
      (h1 : m a b = e)
      (h2 : m b c = e) :
      a = c :=
    sorry

end

-- ============================================================
-- 4. Proofs by induction.
--
-- In Lecture 9 we defined the natural numbers and lists from scratch,
-- and proved a few theorems about them by induction (which, as we
-- saw, is the same thing as recursion). Here you will prove some
-- more. The definitions from the lecture are repeated below; do not
-- change them.
--
-- Do not use tactics, and do not use any lemma from `Nat` about our
-- `add` or `mul` -- the point is to prove these from the definitions.
-- (Lemmas from `Nat` about `+` on the honest `Nat` are fine in 4.10,
-- where `length` really does return a `Nat`.)
--
-- You will probably want to use `congrArg`, and you may use the
-- earlier items of this question when proving the later ones.

namespace MyNat

  inductive N : Type where
    | zero : N
    | succ : N → N

  open N

  def add : N → N → N
    | m, zero => m
    | m, succ n => succ (add m n)

  -- 4.1 [Foundations] Note that `add m zero = m` holds by `rfl`,
  -- because `add` recurses on its second argument. The next one does
  -- not:
  theorem zero_add : ∀ n : N, add zero n = n :=
    sorry

  -- 4.2 [Foundations]
  theorem add_assoc : ∀ k m n : N, add (add k m) n = add k (add m n) :=
    sorry

  -- 4.3 [Foundations]
  theorem succ_add : ∀ m n : N, add (succ m) n = succ (add m n) :=
    sorry

  -- 4.4 [Proficiency] Commutativity. Use 4.1 and 4.3.
  theorem add_comm : ∀ m n : N, add m n = add n m :=
    sorry

  -- 4.5 [Foundations] Define multiplication by recursion on the
  -- second argument, in the style of `add`: `mul m zero` should be
  -- `zero`, and `mul m (succ n)` should be `add (mul m n) m`.
  def mul : N → N → N :=
    sorry

  -- 4.6 [Proficiency] One of the following two needs induction and
  -- the other does not. (Which one, and why?)
  theorem mul_one : ∀ m : N, mul m (succ zero) = m :=
    sorry

  theorem zero_mul : ∀ n : N, mul zero n = zero :=
    sorry

end MyNat

namespace MyList

  inductive L (α : Type) : Type where
    | nil : L α
    | cons : α → L α → L α

  open L

  def length {α : Type} : L α → Nat
    | nil => 0
    | cons x xs => (length xs) + 1

  def append {α : Type} : L α → L α → L α
    | nil, ys => ys
    | cons x xs, ys => cons x (append xs ys)

  -- 4.7 [Foundations] As in 4.1, one of the two unit laws holds by
  -- `rfl` and the other one does not -- but this time it is the other
  -- way round, since `append` recurses on its *first* argument. Here
  -- is the one that needs a proof.
  theorem append_nil {α : Type} : ∀ xs : L α, append xs nil = xs :=
    sorry

  -- 4.8 [Foundations]
  theorem append_assoc {α : Type} :
      ∀ xs ys zs : L α, append (append xs ys) zs = append xs (append ys zs) :=
    sorry

  -- 4.9 [Foundations] Define the `map` function, which applies `f` to
  -- every element of a list, and prove that it preserves the length.
  def map {α β : Type} (f : α → β) : L α → L β :=
    sorry

  theorem length_map {α β : Type} (f : α → β) :
      ∀ xs : L α, length (map f xs) = length xs :=
    sorry

  -- 4.10 [Proficiency] In class we proved
  --
  --   length (append xs ys) = length ys + length xs,
  --
  -- and we remarked that the order of the summands on the right was
  -- chosen to make both cases go through by computation alone. Prove
  -- the version with the summands in the order one would normally
  -- write them. You will need two lemmas from `Nat`; the relevant
  -- ones are about `0 + n` and about `succ n + m`.
  theorem length_append {α : Type} :
      ∀ xs ys : L α, length (append xs ys) = length xs + length ys :=
    sorry

end MyList

-- ============================================================
-- 5. [Proficiency] Prove the following items from [Foundations] again.
-- Each time, use the syntax indicated as part of your proof.

section
  variable (a b c d : Nat)

  -- 5.1 (Item 1.7) Use `have`.
  example : a ^ 2 = a * a :=
    sorry

  -- 5.2 (Item 1.3) Use `match ... with ...`, matching on a proof of
  -- the equality. Hint: `match h with | rfl => ...` will not work on
  -- its own. Lean must substitute for a variable, and it will not do
  -- that unless you also match on the variable in question.
  example : a = b + c → a * d = b * d + c * d :=
    sorry

  -- 5.3 (Item 1.4) Use `show ... from ...`.
  example : a + b + c = a + (c + b) :=
    sorry

  -- 5.4 (Item 1.6) Use `calc`.
  example : a * (b * c) = b * (a * c) :=
    sorry

  -- 5.5 (Item 1.5) Use `▸` (type it as `\t`).
  example : (a + b) + c = (b + a) + c :=
    sorry

end

-- ============================================================
-- 6. [Proficiency]
-- Concise inductive types can serve as sandboxes for practice.
-- In this exercise, we construct a simple inductive type `Signal` and
-- prove some theorems about it.

namespace Signals
  inductive Signal : Type where
    | red : Signal
    | amber : Signal
    | green : Signal

  open Signal

  -- 6.1 Define the cycle `red` → `green` → `amber` → `red` by
  -- pattern matching.
  def next : Signal → Signal :=
    sorry

  -- 6.2 Prove this concrete computation using `rfl`.
  example : next (next (next red)) = red :=
    sorry

  -- 6.3 Prove the following statement by matching on `s`.
  theorem three_steps : ∀ s : Signal, next (next (next s)) = s :=
    sorry

  -- 6.4 Complete the computation with quantifiers and substitution.
  example (P : Signal → Prop) :
      (∃ s : Signal, P (next (next (next s)))) ↔ (∃ s : Signal, P s) :=
    sorry

end Signals

-- ============================================================
-- 7. [Proficiency] Currying, revisited.
--
-- In Homework 1, Question 5.4, you defined two functions
--
--     curryNat   : (Nat × Nat → Nat) → (Nat → Nat → Nat)
--     uncurryNat : (Nat → Nat → Nat) → (Nat × Nat → Nat)
--
-- and checked on a few examples that they are inverse to each other.
-- At the time we had no way to *state* that they are inverse, let
-- alone prove it. Now we do.
--
-- 7.1 Define the two functions again, this time polymorphically.

section
  variable {A B C : Type}

  def curry : (A × B → C) → (A → B → C) :=
    sorry

  def uncurry : (A → B → C) → (A × B → C) :=
    sorry

  -- 7.2 First, the pointwise statements: applied to arguments, the
  -- round trips give back what you started with. Before writing
  -- anything, unfold the definitions and work out what each side
  -- reduces to.
  example (f : A × B → C) (p : A × B) : uncurry (curry f) p = f p :=
    sorry

  example (g : A → B → C) (x : A) (y : B) : curry (uncurry g) x y = g x y :=
    sorry

  -- 7.3 But 7.2 does not yet say that the round trip is the identity
  -- *function*; it only says that it agrees with the identity on every
  -- argument. To get from the one statement to the other, we need a
  -- principle we have not used before: two functions that agree on
  -- every argument are equal. In Lean this is called `funext`, for
  -- "function extensionality".
  #check @funext
       --> @funext : ∀ {α : Sort u_1} {β : α → Sort u_2}
       --      {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g

  -- Use `funext` and 7.2 to prove the function-level statements.
  example (f : A × B → C) : uncurry (curry f) = f :=
    sorry

  example (g : A → B → C) : curry (uncurry g) = g :=
    sorry

  -- 7.4 Finally, state the same two facts as equations between
  -- composites, in the form `_ ∘ _ = id`, and prove them. Watch out:
  -- `curry` and `uncurry` take their types implicitly, and here there
  -- is no argument from which Lean could infer them, so you will need
  -- `@` to supply them yourself.
  --
  -- (Putting it all together: `curry` and `uncurry` exhibit
  -- `(A × B → C)` and `(A → B → C)` as isomorphic types. Investigation
  -- B makes the word "isomorphic" precise; Investigation A asks where
  -- the principle `funext` comes from.)

end

-- ============================================================
-- 8. [Mastery] Definitional equality.
--
-- Some equations can be proved by `rfl`, because Lean can evaluate
-- both sides to the same thing. Others are true but need a real proof.
-- In Lecture 8 we saw one such pair: `n + 0 = n` holds by `rfl`, but
-- `0 + n = n` does not.
--
-- 8.1 For each of the statements below, first *predict* whether `rfl`
-- proves it. Write your prediction down before you run anything --
-- the point of the exercise is the prediction, not the answer. Then
-- check your predictions by replacing `sorry` with `rfl` and seeing
-- which ones Lean accepts.

section
  example (n : Nat) : 0 + n = n := sorry
  example (n : Nat) : n * 1 = n := sorry
  example (n : Nat) : 1 * n = n := sorry
  example (n : Nat) : (n + 1) + 1 = n + 2 := sorry
  example (n : Nat) : 2 * n = n + n := sorry
  example (n : Nat) : n ^ 1 = n := sorry
  example (n : Nat) : (n + 1) - 1 = n := sorry
  example (f : Nat → Nat) : (fun x => f x) = f := sorry
  example (p : Nat × Nat) : (p.1, p.2) = p := sorry
  example (xs : List Nat) : [] ++ xs = xs := sorry
  example (xs : List Nat) : xs ++ [] = xs := sorry
end

-- 8.2 Now explain the pattern. One command makes this much easier.
-- Unlike `#eval`, `#reduce` reduces a term as far as it can even when
-- the term contains variables, and it is willing to reduce under a
-- `fun`. Compare the two cases of Lecture 8:

#reduce (fun n : Nat => n + 0)
#reduce (fun n : Nat => 0 + n)

-- The first prints `fun n => n`. The second prints a large term built
-- from `Nat.rec`: that is the definition of addition, waiting for its
-- second argument to become `0` or `n + 1` so that it can take a
-- step. It waits forever, because that argument is a variable.
--
-- For three of the statements that `rfl` does *not* prove, use
-- `#reduce` to see how far Lean gets on each side, and say what the
-- evaluation gets stuck on. Then state the general rule, in one or two
-- sentences. Your answer must use the phrase "definitional equality".
--
-- ANSWER: ...
--
-- 8.3 Two of the equations in 8.1 involve no computation at all, and
-- `rfl` proves them anyway:
--
--     (fun x => f x) = f
--     (p.1, p.2) = p
--
-- The reason is that Lean's definitional equality contains two rules
-- beyond unfolding definitions and computing with them. Both are
-- called *eta* rules, after the Greek letter η; they are named by
-- analogy with the *beta* rule, which says that `(fun x => t) a` is
-- definitionally `t` with `a` substituted for `x`.
--
--   • Eta for functions: for any `f` whose type is a function type,
--     `fun x => f x` is definitionally equal to `f`. A function is
--     determined by the way it is applied.
--
--   • Eta for structures: if a type has exactly one constructor, then
--     any element `p` of that type is definitionally equal to the
--     constructor applied to the projections of `p`. Here `Prod` has
--     the single constructor `Prod.mk`, so `p` and `(p.1, p.2)` are
--     the same. An element of a one-constructor type is determined by
--     its components.
--
-- The second rule is what made 7.2 work: `uncurry (curry f)` applied
-- to `p` unfolds to `f (p.1, p.2)`, and eta for structures identifies
-- `(p.1, p.2)` with `p`.
--
-- The restriction to one constructor is essential. Of the three
-- equations below, two are proved by `rfl` and one is not. Predict
-- which, then check.

example (f : Nat → Nat → Nat) : (fun x y => f x y) = f := sorry

example (p : Nat × Nat) : (match p with | (x, y) => (x, y)) = p := sorry

example (b : Bool) :
    (match b with | true => true | false => false) = b := sorry

-- Note that the last two statements have the same shape: take the
-- thing apart by pattern matching and put it back together again. The
-- only difference is the number of constructors.
--
-- The failing one is true, and you could prove it. How? And why can
-- Lean not simply extend eta for structures to cover it -- what would
-- it have to know about `b` that it does not know?
--
-- ANSWER: ...
--
-- 8.4 Now one of your own. Define a recursive function
-- `f : Nat → Nat` and exhibit two true equations about it, one that
-- `rfl` proves and one that it does not. Use `#reduce` to show where
-- the second one gets stuck, and account for the difference.

-- ============================================================
-- 9. [Mastery] (The converse of Leibniz's law.)
-- Leibniz's law says that if `a = b`, every property of `a` is also a
-- property of `b`. Does this characterize equality? In other words,
-- does the converse hold? If no predicate distinguishes `a` from `b`,
-- must they be equal?
--
-- Let us give the relation "no predicate distinguishes a from b" a
-- name. Following Leibniz, call `a` and `b` *indiscernible* if every
-- property of `a` is also a property of `b`:

section
  variable {A : Type}

  def Indisc (a b : A) : Prop := ∀ P : A → Prop, P a → P b

  -- 9.1 Prove that indiscernible elements are equal. (Hint: you get
  -- to choose `P`. Choose it well.)
  theorem eq_of_indisc : ∀ a b : A, Indisc a b → a = b :=
    sorry

  -- 9.2 Conversely, Leibniz's law itself says that equal elements are
  -- indiscernible. We know this one: it is `Eq.subst`. So the two
  -- notions coincide; prove it.
  theorem indisc_iff_eq : ∀ a b : A, Indisc a b ↔ a = b :=
    sorry

  -- 9.3 The definition of `Indisc a b` is not symmetric in `a` and
  -- `b`: it says that the properties of `a` are among the properties
  -- of `b`, not the other way around. Nevertheless, prove that the
  -- relation is symmetric. (You may use 9.1 and 9.2. Can you also give
  -- a direct proof?)
  theorem indisc_symm : ∀ a b : A, Indisc a b → Indisc b a :=
    sorry

  -- 9.4 Deduce the variant where the predicates are tested in both
  -- directions.
  example : ∀ a b : A, (∀ P : A → Prop, P a ↔ P b) → a = b :=
    sorry

end

-- 9.5 In 9.1 the quantifier `∀ P : A → Prop` was essential: the
-- hypothesis gives you the implication `P a → P b` for *every*
-- predicate, and you used it for one predicate of your choosing. What
-- if we only knew it for a single, fixed predicate? Show that this is
-- not enough, by filling in a predicate `P` below for which the
-- hypothesis holds but the conclusion fails.

#check Nat.zero_ne_one

def P : Nat → Prop :=
  sorry

example : P 0 → P 1 :=
  sorry

example : ¬(0 = 1) :=
  sorry

-- 9.6 Leibniz did not propose 9.2 as a theorem: he proposed
-- indiscernibility as the *definition* of equality. (As a theorem it
-- presupposes a notion of equality, or there would be nothing to
-- state.) So let us take him at his word, and ask whether the
-- definition can stand on its own.
--
-- Below, `LEq` is the same relation as `Indisc`, but now regarded as
-- *the* definition of equality. Prove the five theorems. The rule for
-- this part is that you may not use `=`, `rfl`, `Eq.subst`, or
-- anything else belonging to `Eq`, at any point.

namespace Leibniz
  variable {A B : Type}

  def LEq (a b : A) : Prop := ∀ P : A → Prop, P a → P b

  theorem refl (a : A) : LEq a a :=
    sorry

  theorem subst {a b : A} (P : A → Prop) : LEq a b → P a → P b :=
    sorry

  theorem symm {a b : A} : LEq a b → LEq b a :=
    sorry

  theorem trans {a b c : A} : LEq a b → LEq b c → LEq a c :=
    sorry

  theorem congr {a b : A} (f : A → B) : LEq a b → LEq (f a) (f b) :=
    sorry

end Leibniz

-- Two things to account for:
--
--   • Lean's `Eq` consists of a type, one constructor (`Eq.refl`) and
--     a recursor, whose essential content is `Eq.subst`. Which two of
--     your five theorems play those roles, and how long are their
--     proofs? Which of the five are then mere consequences?
--
--   • Your proof of `symm` cannot be the one you gave in 9.3, which
--     went through `=`. Which predicate did you feed to the hypothesis
--     instead, and what did you use in place of `rfl`?
--
-- ANSWER: ...
--
-- Together with 9.2, this says that in Lean the two accounts of
-- equality are interchangeable: each one proves everything the other
-- one does.

end Homework4

-- ============================================================
-- Investigation A: function extensionality
-- ------------------------------------------------------------
-- Question 7.3 used a principle you had met before in mathematics,
-- but not in Lean: two functions that agree on every argument are
-- equal. Question 8 showed that equality in Lean comes in two
-- flavours -- the definitional equality that `rfl` can see, and the
-- propositional equality `=` that needs proofs. This investigation is
-- about where `funext` sits in that picture, what it is good for, and
-- where in Lean it comes from.

namespace Extensionality

-- (A) There are two things one might mean by saying that two
-- functions are equal.
--
--   • *Extensionally*: they have the same value at every argument. No
--     attention is paid to how either one is defined. This is what
--     mathematicians normally mean, and it is what `funext` is about.
--
--   • *Intensionally*: the two definitions themselves agree -- "equal
--     as formulas". In Lean this is definitional equality, which
--     allows unfolding of definitions, computation, and the eta rules
--     of Question 8.3, and nothing else.
--
-- Here is a pair of functions that are intensionally equal. `rfl`
-- proves it, and `#reduce` shows why: the two definitions reduce to
-- the same formula, up to the name of the bound variable.

#reduce (fun n : Nat => n + 0)
#reduce (id : Nat → Nat)

example : (fun n => n + 0) = (id : Nat → Nat) :=
  sorry

-- The next pair is extensionally equal but not intensionally equal.
-- The lemma establishes the pointwise statement; neither definition
-- reduces to the other, so `rfl` fails. Check that it fails, then
-- prove the equation. Note: you will need `funext`.

theorem one_add (x : Nat) : 1 + x = x + 1 := Nat.add_comm 1 x

example : (fun x : Nat => 1 + x) = (fun x : Nat => x + 1) :=
  sorry

-- Here is a second pair of the same kind, where even the pointwise
-- statement takes an induction.

def double : Nat → Nat
  | 0 => 0
  | n + 1 => double n + 2

example : double = (fun n => 2 * n) :=
  sorry

-- (B) Try proving one of the last two examples without `funext`,
-- using only the tools of Lecture 8 (`Eq.subst`, `congrArg`,
-- `Eq.trans`, the lemmas in `Nat`, induction). Report what you tried
-- and where you got stuck. What *can* you prove about these pairs of
-- functions without `funext`?

-- (C) Now let us say exactly what `funext` adds. Call `f` and `g`
-- *extensionally equal*, written `f ~ g`, if they agree on every
-- argument. We can set up the notation ourselves, as in Lecture 9:

def EqExt {A B : Type} (f g : A → B) : Prop := ∀ x : A, f x = g x

infix:50 " ~ " => EqExt

-- Prove each direction of the following. One direction is `funext`;
-- for the other one, find out what `congrFun` does.

theorem eq_iff_eqExt {A B : Type} (f g : A → B) : f = g ↔ f ~ g :=
  sorry

-- So `funext` is precisely the statement that propositional equality
-- of functions *is* pointwise equality -- no finer, no coarser. Say
-- what this homework sheet would look like without it: which of your
-- proofs in Question 7 survive, and what is the strongest statement
-- about `curry` and `uncurry` you could still make?

-- (D) Where does `funext` come from? It cannot hold definitionally:
-- argue informally why not. (Hint: Lean must be able to *check*
-- definitional equality mechanically. What would it have to do to
-- check that two functions `Nat → Nat` agree on every argument?)
--
-- So it must be either an axiom or a theorem. Which one is it?
-- Investigate the dependencies, and report what you find:

#print axioms funext
#print axioms eq_iff_eqExt
#print axioms congrFun

-- It turns out that `funext` is not an axiom, but it _uses_ another
-- axiom. Find out what `Quot.sound` says (`#print Quot.sound`). It
-- turns out that `funext` is provable from properties of quotient
-- types, but asking you to prove it is too much to ask for this
-- investigation. Feel free to investigate this further if you like a
-- fun challenge.

-- (E) Finally, let's try to put `funext` in context. Lean has three
-- principles that all look like "things that behave the same are
-- equal", and they have three *different* statuses:
--
--   • proof irrelevance: any two proofs of the same proposition are
--     equal. (Homework 3, Question 4: it is proved by `rfl`.)
--   • propositional extensionality: logically equivalent
--     propositions are equal. (Lecture 6. Check its status below.)
--   • function extensionality: pointwise equal functions are equal.
--
#print axioms propext
example (p : Prop) (h1 h2 : p) : h1 = h2 := sorry
example (p q : Prop) : (p ↔ q) → p = q := sorry

-- Arrange the three in order of "how much you have to assume to get
-- them", and explain the ordering. Is proof irrelevance really the
-- same kind of statement as the other two? Note that `propext` is the
-- `funext` of propositions: what plays the role of "agreeing on every
-- argument"?

end Extensionality

-- ============================================================
-- Investigation B: equality and isomorphism
-- ------------------------------------------------------------
-- Recall that two types are "isomorphic" if there exist functions
-- `f : A → B` and `g : B → A` which compose to identities. In this
-- investigation you will explore this concept in some detail, and in
-- particular how it relates to equality of types.

namespace Equivalences

universe u
variable {A B : Sort u}

-- The following definition says what it means for `f : A → B` to be
-- an isomorphism. You can type `∘` by typing `\circ`.

def isIso (f : A → B) : Prop :=
  ∃ g : B → A, (g ∘ f = id) ∧ (f ∘ g = id)

def isomorphic (X Y : Sort u) : Prop :=
  ∃ f : X → Y, isIso f

-- (A) Warm-up: check that this definition behaves the way the word
-- "isomorphism" ought to behave. Prove the following. (Equalities of
-- functions are involved, so you will want `funext` and `congrFun`;
-- see Question 7.3 and Investigation A.)

theorem isIso_id : isIso (id : A → A) :=
  sorry

theorem isIso_comp {C : Sort u} (f : A → B) (g : B → C) :
    isIso f → isIso g → isIso (g ∘ f) :=
  sorry

-- Deduce that `isomorphic` is reflexive, symmetric and transitive.
-- (Symmetry is the interesting one: notice that the definition of
-- `isomorphic A B` is not symmetric on its face.)

theorem isomorphic_refl : isomorphic A A :=
  sorry

theorem isomorphic_symm : isomorphic A B → isomorphic B A :=
  sorry

theorem isomorphic_trans {C : Sort u} :
    isomorphic A B → isomorphic B C → isomorphic A C :=
  sorry

-- Also record the two isomorphisms you have already built elsewhere
-- on this sheet: `curry`/`uncurry` from Question 7, and one of the
-- isomorphisms from Homework 1 (say `(A × B) × C` and `A × (B × C)`).
-- For each one, write down the statement that says the two types are
-- `isomorphic`, and prove it.

-- (B) Prove that equal objects are isomorphic:
theorem idtoiso : (A = B) → isomorphic A B :=
  sorry

-- (C) Now the converse. Are isomorphic types equal? Pick a concrete
-- pair of types which are "obviously the same but not literally the
-- same" -- for instance two of your own two-element inductive types,
--
--     inductive Two  : Type where | a | b
--     inductive Two' : Type where | x | y
--
-- First prove `isomorphic Two Two'`. Then try to settle `Two = Two'`:
--
--   • Try to prove `Two = Two'`.
--   • Try to prove `¬(Two = Two')`.
--
-- Report how each attempt went. You should find that you can do
-- neither, and that is the point of this part: Lean's type theory
-- does not decide the question. Say as precisely as you can *why* you
-- cannot prove either one. (For the first: what are the ways of
-- proving an equality that we know? For the second: what would a proof
-- of `¬(Two = Two')` have to exploit, and is there anything in the
-- theory to exploit?)

-- (D) Since the theory does not decide it, we may consider adding an
-- axiom which does. The "univalence axiom" declares that isomorphic
-- types are equal:

axiom ua : isomorphic A B ↔ (A = B)

-- Assume it, and see what it buys you: use `ua` to prove `Two = Two'`,
-- and then use that equality to transport something -- find a
-- predicate `P : Type → Prop` which you can prove for `Two` and then
-- obtain for `Two'` by substitution.
--
-- Is assuming `ua` safe? Here is one thing to check before trusting
-- it. In Lean, `A = B` is a proposition, so any two proofs of it are
-- equal:

example (h1 h2 : A = B) : h1 = h2 := sorry

-- But a type typically has *many* different isomorphisms to itself
-- (find two different ones for `Two`). Does that contradict `ua`? Look
-- carefully at what `isomorphic A B` actually records: it is a `Prop`,
-- asserting only that an isomorphism *exists*, and not saying which
-- one. Explain why this means the obvious attempt at a contradiction
-- does not go through. (This is a real subtlety, and it is the point
-- where the type theory of this course and the type theory of
-- Homotopy Type Theory part company; see the readings below.)

-- (E) One case where the question *is* settled: propositions.
-- For `A B : Prop`, the univalence statement is not an axiom but a
-- theorem. Prove it. (You will need `propext` from Lecture 6.
-- Depending on what method you use, you may also need proof
-- irrelevance from Homework 3.)

theorem ua_prop (A B : Prop) : isomorphic A B ↔ (A = B) :=
  sorry

-- So: for propositions, "isomorphic" and "equal" provably coincide;
-- for types, Lean deliberately says nothing.

-- (F) Finally, a question about the definition itself. Here is a
-- second notion of "invertible": instead of asking for one `g` that is
-- inverse on both sides, ask separately for a left inverse and a right
-- inverse.

def isEquiv (f : A → B) : Prop :=
  (∃ g : B → A, g ∘ f = id) ∧ (∃ h : B → A, f ∘ h = id)

-- `isEquiv` looks weaker than `isIso`. Prove that it is not:

theorem isoToEquiv (f : A → B) : (isIso f) ↔ (isEquiv f) :=
  sorry

-- One direction is immediate. For the other, you must show that a
-- left inverse and a right inverse of the same function are equal --
-- which is exactly Question 3.6, with composition of functions as the
-- associative operation and `id` as its unit. Write the proof as a
-- `calc` chain and compare it with what you wrote there.
--
-- A closing remark on why anyone cares. We got away with treating
-- "`f` is an isomorphism" as a mere proposition: `isIso f` records
-- that an inverse exists and forgets which one, and all proofs of it
-- are equal. In type theories where this data is *not* forgotten --
-- HoTT, say, where `isIso f` is the type of inverses of `f` -- the two
-- definitions above come apart, and `isEquiv` is the better behaved
-- one. If you are curious, we recommend:
--
-- https://amelia.how/posts/the-complete-history-of-isotoequiv.html
--
-- https://www.cs.uoregon.edu/research/summerschool/summer23/_lectures/Introduction_to_HoTT_Notes.pdf

end Equivalences