Hitchhikers Guide to Logical Verification: Exercises

Stream: Type theory

[Maximilian Weichart]

Dear community,
I'm just getting to know Type Theory and Lean 4 by reading the book Hitchhiker's Guide to Logical Verification (https://lean-forward.github.io/hitchhikers-guide/2024/) which was mentioned in the Lean Documentation. I was wondering if there are solutions out there for the exercises or homework:

/- Copyright © 2018–2024 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/

import LoVe.LoVe01_TypesAndTerms_Demo


/- # LoVe Exercise 1: Types and Terms

Replace the placeholders (e.g., `:= sorry`) with your solutions. -/


set_option autoImplicit false
set_option tactic.hygienic false

namespace LoVe


/- ## Question 1: Terms

Complete the following definitions, by replacing the `sorry` markers by terms
of the expected type.

Hint: A procedure for doing so systematically is described in Section 1.4 of
the Hitchhiker's Guide. As explained there, you can use `_` as a placeholder
while constructing a term. By hovering over `_`, you will see the current
logical context. -/

def I : α → α :=
  fun a ↦ a

def K : α → β → α :=
  fun a b ↦ a

def C : (α → β → γ) → β → α → γ :=
  fun f b a ↦ f a b

def projFst : α → α → α :=
  fun a b ↦ a

/- Give a different answer than for `projFst`. -/

def projSnd : α → α → α :=
  fun _ b ↦ b

def someNonsense : (α → β → γ) → α → (α → γ) → β → γ :=
  fun f a _ b ↦ f a b


/- ## Question 2: Typing Derivation

Show the typing derivation for your definition of `C` above, on paper or using
ASCII or Unicode art. You might find the characters `–` (to draw horizontal
bars) and `⊢` useful. -/

-- write your solution in a comment here or on paper

end LoVe

These are my answers to the questions. Could you please tell me if they are going in the right direction? Also, I have no idea how to solve question 2. Any solution I come up with quickly becomes super complex, and this discourages me from continuing with the task. I feel like the book does too little to explain on that part (building type proof derivations), and other resources are challenging to get into as a beginner, not to mention that I'm not even certain my implementation is correct to begin with.

I'm happy that I've found a community with people interested in Type Theory and Lean and would really appreciate your support. Please let me know if I can assist with any clarifications .

[Henrik Böving]

Jasmin's group does hold this book as a lecture at LMU and previously at the university of amsterdam. The repository containing solutions for this year can be seen here: https://github.com/blanchette/interactive_theorem_proving_2024

[Henrik Böving]

For this specific chapter, as long as you provide something that lean accepts without errors you are doing the right thing :thumbs_up:

[Maximilian Weichart]

Thank you so much, this repository is just what I was looking for!