advice on learning to prove inhabitant has given type

Stream: new members

[rzeta0]

I previously worked through Heather MacBeth's Mechanics of Proof course completing all exercises (except 3).

I am currently working through Type Theory & Formal Proof by Nederpelt - my aim is to better understand how and why proof assistants work, centred around the idea of "terms as proofs, types as propositions".

As I work through the exercises, a few voices have suggested I try writing Agda proofs to check if my own solutions are correct.

I'm too old to learn YetAnotherLanguage(tm) so wondered about doing it in Lean.

Previously I used Lean to do very simple proofs, mostly algebraic in nature, eg algebraic identities, and maybe include some logic eg disjunctions in the hypotheses or goals.

Now I am starting to ask how to prove more general things like

$$∀_{x∈S} (Q(x)) ⇒ ∀_{y∈S}(P(y) ⇒Q(y))$$

I expect I would establish a context $S:*, Q:S \to *, P:S \to *$ and type $\Pi a:(\Pi x:S . (Qx)) . ( \Pi y:S.(\Pi b:(Py). Qy))$ in Lean, somehow, and then show there is an inhabitant of the type eg $\lambda a:(\lambda x:S.ax).(\lambda y:S . (\lambda b:(Py).ay ))$.

Question: Is there a beginner-friendly intro that will help me check that the inhabitants I come up with are actually of the correct type (and perhaps also check the type corresponds to the logical statement) ?

In MacBeth's course, more abstract "sets" were only briefly introduced.

[Kenny Lau]

you use variable (term : type) to set up a context, and use #check (term : type) to check that a term has a given type

[rzeta0]

Thanks Kenny. I'm not familiar enough to know where these 'variable' and 'check' go in a lean program. Is there anywhere I can read simple examples?

[Kenny Lau]

@rzeta0 they just go on their own lines.

variable (fib : Nat → Nat)
#check fib 1000

[Kenny Lau]

to run the example program above, click the button on the top right corner of the textbox when your mouse hovers over it

[Kenny Lau]

image.png

[Eric Wieser]

rzeta0 said:

Now I am starting to ask how to prove more general things like

$$∀_{x∈S} (Q(x)) ⇒ ∀_{y∈S}(P(y) ⇒Q(y))$$

Your first step should be "how do I _state_ this in Lean", because until you do that Lean has no way to check the proof

[Eric Wieser]

I would hope that Mechanics of Proof has prepared you for such a task, but if it hasn't this statement seems like something you could ask any remotely competent language model to translate, which should hopefully remind you how to do this kind of translation in future

[rzeta0]

Thanks @Kenny Lau

I'll try what you suggest. How do you write * in Lean?

The following doesn't work.

variable (S : *)
variable (P : S → *)

Thanks in advance for your patience with a beginner !

[Kenny Lau]

@rzeta0 * is indeed not a valid Lean syntax. What does it mean?

[Kenny Lau]

I suppose it means Unit?

[Aaron Liu]

it means Type

[Aaron Liu]

or maybe it means Prop

[Kenny Lau]

note that Prop in Agda behaves differently from Lean

[rzeta0]

@Kenny Lau It is the "type of types".

So 3 has type "Int" and "Int" has type *. (And * has type $\Box$)

In the textbook I'm following the idea is that propositions have type * too, and inhabitants of such types are proofs. So $S:*$ corresponds to a set and $$$P:S \to *$$ corresponds to a proposition on that set.

(I'm still new to this so might bit a bit imprecise)

[Kenny Lau]

propositions and Int can't have the same type

[Aaron Liu]

in Lean 3 : Int and Int : Type

[Aaron Liu]

(and Type : Type 1)

[rzeta0]

@Aaron Liu is this related to u_1 and u_2 that I once saw?

I will try Type as you suggest.

[Aaron Liu]

rzeta0 said:

In the textbook I'm following the idea is that propositions have type * too, and inhabitants of such types are proofs. So $S:*$ corresponds to a set and $$$P:S \to *$$ corresponds to a proposition on that set.

in Lean what makes propositions different from all the other types is that any two proofs are definitionally equal (and also docs#propext but that's an axiom) (and also impredicativity but that's not relevant right now)

[rzeta0]

Thanks @Aaron Liu .. I'm sure as I progress through the book I will better understand and see the implementation decisions in Lean like this one you suggest about definitional equality.

[Jakub Nowak]

I would say something like this would be an equivalent of your statement in Lean?

theorem foo (S : Sort u) (Q P : S → Prop) : (∀ (x : S), Q x) → (∀ (y : S), P y → Q y) := by
  sorry

[Jakub Nowak]

And the proof is probably also equivalent to what you have written at the beginning (without explicit type annotations):

theorem foo (S : Sort u) (Q P : S → Prop) : (∀ (x : S), Q x) → (∀ (y : S), P y → Q y) := fun a y _ => a y

[Jakub Nowak]

In Lean there's no type of all types, hence those u_1 u_2 you mentioned were invented. These are called universes. I'm sure you'll understand it as you progress through tutorials. If you want to avoid them, then I think you can state what you want just like this:

def foo (S : Type) (Q P : S → Type) : (∀ (x : S), Q x) → (∀ (y : S), P y → Q y) := fun a y _ => a y

[rzeta0]

Thanks @Jakub Nowak your code examples are ideal for me to study.

I think I understand most of the code, the exception is fun which I've not seen before so will explore that.

[Aaron Liu]

it's a lambda abstraction

[Kenny Lau]

it's the same as what you wrote as λ

[rzeta0]

thanks Aaron and Kenny.

Is there a way to check with Lean that the logical statement :

(S : Sort u) (Q P : S → Prop) : (∀ (x : S), Q x) → (∀ (y : S), P y → Q y)

is in fact the type :

$$\Pi a:(\Pi x:S . (Qx)) . ( \Pi y:S.(\Pi b:(Py). Qy))$$

[Aaron Liu]

well just look at it

[Kenny Lau]

no, there is currently no way to go from Lean code to an arbitrary language that you just specified

[Aaron Liu]

you can also write this as

(S : Sort u) (Q P : S → Prop) : ∀ (a : (∀ (x : S), Q x)), (∀ (y : S), (∀ (b : P y), Q y))

this is the same type to Lean

[Jakub Nowak]

That's one of the disadvantages of any formal language. You can write some definitions in this language (e.g Lean) and prove some statements about these definitions. But the only way to relate those formal definitions and statements with anything that doesn't have a formal computer specification is to do manual review by humans. And for this the human has to understand semantics of both the formal language and the pen-and-paper definition.