Implementing a Prototype for Combinatory Logic

Stream: general

[Creative Salmon]

Hi everyone,

I am a beginner in Lean and Combinatory Logic, trying to formalize basic combinators from Raymond Smullyan's "To Mock a Mockingbird". The "birds" here are just combinators (functions). My goal is to work through the book's puzzles.

Here’s my setup:

axiom Bird : Type
axiom response : Bird → Bird → Bird
infixl:90 " ⬝ " => response

axiom response_ext : (∀ x, a ⬝ x = b ⬝ x) → a = b

def is_kestrel (K : Bird) : Prop :=
  ∀ x y, K ⬝ x ⬝ y = x

@[simp]
theorem kestrel_simp (h: is_kestrel K) : K ⬝ x ⬝ y = x := h x y

example (h : is_kestrel K) : K ⬝ x ⬝ y ⬝ z = x ⬝ z := by
  simp [h]

My questions:

1. The kestrel_simp lemma feels redundant — can simp use is_kestrel K directly?
2. I currently have to manually pass h to simp. Can this be automatic?
3. I would like extensionality so that K ⬝ x ⬝ y ⬝ z = x ⬝ z reduces to K ⬝ x ⬝ y = x automatically, maybe even via simp?

I suspect Lean has mechanisms for all of this, but I am not familiar with them. What is the idiomatic way to handle this in Lean?

[Aaron Liu]

Creative Salmon said:

1. The kestrel_simp lemma feels redundant — can simp use is_kestrel K directly?

No. Since is_kestrel is not reducible, simp can't see through its definition. simp [h _ _] works because the type of h _ _ is an equality, but simp [h] alone does not work because the type of h is is_kestrel K which is not an equality at reducible transparency.

[Aaron Liu]

Creative Salmon said:

2. I currently have to manually pass h to simp. Can this be automatic?

You could configure the discharger to search through the local hypotheses, so simp (disch := assumption) for example, or you could use simp_all or simp [*] which both give simp access to all the local hypotheses.

[Aaron Liu]

Creative Salmon said:

3. I would like extensionality so that K ⬝ x ⬝ y ⬝ z = x ⬝ z reduces to K ⬝ x ⬝ y = x automatically, maybe even via simp?

This isn't sound, since if you could do this then you could prove K ⬝ x ⬝ y ⬝ z = x ⬝ z → K ⬝ x ⬝ y = x by simplifying it to K ⬝ x ⬝ y = x → K ⬝ x ⬝ y = x.

[Creative Salmon]

Is there a better way to implement all of this (maybe the whole axiom approach is not a good fit)?

Aaron Liu said:

No. Since is_kestrel is not reducible, simp can't see through its definition. simp [h _ _] works because the type of h _ _ is an equality, but simp [h] alone does not work because the type of h is is_kestrel K which is not an equality at reducible transparency.

Ok. Out of curiosity, why simp does not try to "instantiate" that (as in you example, simp [h _ _])? Are there not too many theorems for simp to use which are behind this kind of quantifiers? Maybe there is a pattern to write simp theorems I miss.

Aaron Liu said:

You could configure the discharger to search through the local hypotheses, so simp (disch := assumption) for example, or you could use simp_all or simp [*] which both give simp access to all the local hypotheses.

Yes, these help with the current approach. Thank you.

Aaron Liu said:

This isn't sound, since if you could do this then you could prove K ⬝ x ⬝ y ⬝ z = x ⬝ z → K ⬝ x ⬝ y = x by simplifying it to K ⬝ x ⬝ y = x → K ⬝ x ⬝ y = x.

Why isn't that sound? Isn't that the definition of is_kestrel K?

[Aaron Liu]

Creative Salmon said:

Aaron Liu said:

This isn't sound, since if you could do this then you could prove K ⬝ x ⬝ y ⬝ z = x ⬝ z → K ⬝ x ⬝ y = x by simplifying it to K ⬝ x ⬝ y = x → K ⬝ x ⬝ y = x.

Why isn't that sound? Isn't that the definition of is_kestrel K?

Well I guess if you have an is_kestrel K hypothesis then it's sound, but you would also never need such an extensionality lemma in this case because K ⬝ x ⬝ y ⬝ z = x ⬝ z simplifies to True.