stuck on type-theory/logic exercise (Nederpelt 7.13)

Stream: new members

[rzeta0]

After completing the MacBeth Lean course, I wanted deeper understanding of how theorem provers worked, so someone here advised I work through Type Theory and Formal Proof (Nederpelt). I'm now at the end of Chapter 7, working through all the exercises.

I've been stuck on exercise 7.13 for a week and would really appreciate help. I'm told on stack exchange that it is easy but I'm just not seeing it.

---

Exercise

The exercise is to show the following logical statement is a tautology:

$$\exists_{x \in S}(P(x)) \quad \implies \quad ( \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z)) )$$

This tautology makes intuitive sense. Here is a natural deduction tree proof I developed to ensure I understood it properly.

type_theory_and_formal_proof-2.png

---

Solution Step 1

As a first step I need to find the corresponding type for this statement, and then as a second step I need to derive an inhabitant of that type (in λC).

We have learned how to encode the existential quantifiers $\exists, \forall$ and also implication $\implies$. The type is

$$\begin{gather*} \Pi \alpha : * . ((\Pi x : S. (P x \to \alpha )) \to \alpha) \\ \to \\ \Pi y:S.(Py \to Qy) \\ \to \\ \Pi \alpha : * . ((\Pi z : S. (Q z \to \alpha )) \to \alpha) \end{gather*}$$

I think this is correct.

---

Solution Step 2

The book has been teaching us to use "flag-notation" for derivations (with natural deduction trees as a comparative exercise). These are useful because they help visualise the "scope" of assumptions. (some examples I've completed)

Most proofs follow the samestructure because to prove $A \implies (B \implies C)$ we assume $A$ and $B$ and use inhabitants of these (functions) to derive an inhabitant of $C$.

The attached image shows the start of such a proof.

type_theory_and_formal_proof.png

---

Discussion

I need to derive an inhabitant of type $\alpha$, with the following assumptions (in addition to the context $S: *, P,Q:S \to *$)

*$f \; : \; \Pi \alpha : * . (\Pi x : S. (P x \to \alpha )) \to \alpha$

• $g \; : \; \Pi y:S.Py \to Qy$
• $\alpha \; : \; *$
• $h \; : \; \Pi z : S. (Q z \to \alpha )$

The only way forward I can see is to apply $f$ to $\alpha$ to give

$$f \alpha \; : \; (\Pi x:S . (Px \to \alpha)) \to \alpha$$

In other exercises I have another assumed function of type $(\Pi x:S . (Px \to \alpha))$ so I can apply $f \alpha$ to it.

But here the argument to $f \alpha$ doesn't match anything I have or can easily construct. The type of $h$ is not compatible.

I've been stuck for over a week, I'd really welcome guidance.

[Aaron Liu]

You are in the right track - $f \alpha$ is correct

[Aaron Liu]

Next you should construct something you can feed to $f \alpha$

[rzeta0]

I'd welcome a more revealing hint. I've been staring at it for 2 weeks!

[Aaron Liu]

What's the way to build an element of a pi-type?

[rzeta0]

Assume something then abstract over it. Here is an example I've done where the conclusion is a pi-type. https://type-theory-and-formal-proof.blogspot.com/2025/10/chapter-7-exercise-12.html

[Aaron Liu]

so the next step is to assume a $x : S$

[rzeta0]

ok - I'll try that this evening. My brain has been really stuck on it for some reason.

I've managed to do all the exercises up to this one without a 2-week hiatus: https://type-theory-and-formal-proof.blogspot.com/p/contents.html

Something about this one just blocked my brain.

[rzeta0]

@Aaron Liu I'm still not seeing it. Let me explain my thought processes:

• we have $f \alpha \; : \; (\Pi x:S . (Px \to \alpha)) \to \alpha$
• I need to construct a pi-type $\Pi x:S . (Px \to \alpha)$ to feed it
• the normal way to construct such a type is to "assume-abstract on $x:S$" - that's fine
• but I can't find path to deriving something with type $Px \to \alpha$
• $hx$ is of type $Qx \to \alpha$ but this doesn't seem helpful

Over the last week I tried experimenting with $f(Qx)$ because this of type $(\Pi s:S . (Ps \to Qx)) \to Qx$ and that looked promising, but again that didn't work out because $s$ is not $x$ in that expression.

[Aaron Liu]

How do you construct a term of type $A \to B$

[rzeta0]

assume x:A and somehow use it to find an inhabitant of B.

• assume x:A
• do something with x, A, B, and any other assumptions, to get y:B
• conclude λx:a.y : A → B

but I can't seem to find an inhabitant of B here.

[Aaron Liu]

So next is to assume $x : Px$ and try to derive an $\alpha$

[Aaron Liu]

You said you couldn't figure it out so I'll give another hint

[Aaron Liu]

What things in your context at this point can let you conclude $\alpha$?

[rzeta0]

$h$ is what I use to conclude $\alpha$

I think the $a : Px$ assumption is what I was missing, let me try that when I get back home.

[Aaron Liu]

perhaps this will be helpful

example {S : Type u} (P Q : S → Prop) :
    (∃ x : S, P x) →
    (∀ y : S, P y → Q y) →
    (∃ z : S, Q z) :=
  fun he ha =>
    Exists.elim he fun x hx =>
      Exists.intro x (ha x hx)

-- universe monomorphic in order to not be annoying
example {S : Type} (P Q : S → Type) :
    (∀ α : Type, (∀ x : S, P x → α) → α) →
    (∀ y : S, P y → Q y) →
    (∀ α : Type, (∀ x : S, Q x → α) → α) :=
  fun f g α h =>
    f α fun x => sorry

[rzeta0]

I think I did it finally, thanks to your nudging me in the right direction.
type_theory_and_formal_proof.png

It's overly verbose but the central expression is $f(\lambda x:S. \lambda a:Px . hx(gxa)) \; : \; \alpha$

What did I learn from this exercise? So far there have only been a very small number of exercises that have needed me to construct a type that wasn't immediately available from the straightforward application of the existing assumptions. Ive not had much practice at this. I don' think there are any general rules to be learned.

What do I mean by "general rules". Well, just though practice - and not by direction of the author - I have learned a strategy for most proofs which his to "assume the left of each implication / mapping → and prove the right. This has worked well to create a first skeleton of most of my proofs.

Question: Is this a question of practice and experience ... or am I missing some heuristic or rule to help create such proofs?

Finally - thank you @Aaron Liu you have helped in a way that was educational.

[Aaron Liu]

Try the version in Lean

-- universe monomorphic in order to not be annoying
example {S : Type} (P Q : S → Type) :
    (∀ α : Type, (∀ x : S, P x → α) → α) →
    (∀ y : S, P y → Q y) →
    (∀ α : Type, (∀ x : S, Q x → α) → α) := by
  intro f g α h
  apply f
  sorry

[rzeta0]

I've lost my lean skills from lack of use .. but I think the following is an inelegant proof.

I say inelegant because instead of thinking about the problem and its nature, I'm falling into "goal chasing", which can work, but feels less intellectually honest ! :)

-- universe monomorphic in order to not be annoying
example {S : Type} (P Q : S → Type) :
    (∀ α : Type, (∀ x : S, P x → α) → α) →
    (∀ y : S, P y → Q y) →
    (∀ α : Type, (∀ x : S, Q x → α) → α) := by
  intro f g α h
  apply f
  ---
  intro x
  intro px
  have pq : P x → Q x := g x
  have qx : Q x := pq px
  have h2 : Q x → α := h x
  apply h2
  exact qx

[Aaron Liu]

rzeta0 said:

I say inelegant because instead of thinking about the problem and its nature, I'm falling into "goal chasing", which can work, but feels less intellectually honest ! :)

Usually when I want to prove something in Lean I split it up into some manageable size subproblems based on the proof I'm following (my own proof or someone else's) and then for each subproblem I do "goal chasing" which usually works, and when it doesn't work I go in circles for an hour or two before thinking about it seriously and solving the problem in five minutes

[Aaron Liu]

Now let's reduce/evaluate this proof you made:

-- universe monomorphic in order to not be annoying
def proof {S : Type} (P Q : S → Type) :
    (∀ α : Type, (∀ x : S, P x → α) → α) →
    (∀ y : S, P y → Q y) →
    (∀ α : Type, (∀ x : S, Q x → α) → α) := by
  intro f g α h
  apply f
  ---
  intro x
  intro px
  have pq : P x → Q x := g x
  have qx : Q x := pq px
  have h2 : Q x → α := h x
  apply h2
  exact qx

variable {S : Type} (P Q : S → Type)
set_option pp.funBinderTypes true

/-
fun (f : (α : Type) → ((x : S) → P x → α) → α) (g : (y : S) → P y → Q y)
  (α : Type) (h : (x : S) → Q x → α) =>
    f α fun (x : S) (px : P x) => h x (g x px)
-/
#reduce @proof S P Q

Do you recognize this expression? It's the same as the proof you did in λC

[rzeta0]

very interesting!

so looking at the tooltip for reduce I understand that it reduces a high level proof (lean tactics) to a low-level internal proof (terms corresponding to λC) ?

[Aaron Liu]

So what actually gets typechecked by the Lean kernel are the Expressions that the tactics produce, which you can see here if I #print the proof instead

/-
def proof : {S : Type} →
  (P Q : S → Type) →
    ((α : Type) → ((x : S) → P x → α) → α) →
      ((y : S) → P y → Q y) → (α : Type) → ((x : S) → Q x → α) → α :=
fun {S} P Q f g α h =>
  f α fun x px =>
    have pq := g x;
    have qx := pq px;
    have h2 := h x;
    h2 qx
-/
#print proof

Tactics are just a way to streamline the process of writing these expressions by building them up incrementally, and these are what #reduce operates on by beta and eta and all the other reductions.

[rzeta0]

thanks again, I'm learning a lot !