hitchhikers guide

Stream: new members

[Patrick Thomas]

Some questions referring to https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf

On page 6: "The local context gives the types of the variables in t that are not bound by any λ." Does variables in this statement refer to the formal definition of a variable given by the second rule below this statement?

How does a variable get added to the local context? For instance, how did x : Z get added to the local context at the top of the example below? I don't see a rule for adding a variable to the local context. Do we just declare whatever variables of whatever type we want to be in the local context at the start like we do with hypotheses?

On page 7: "Given a type σ, the type inhabitation problem consists of finding an “inhabitant” of that type—i.e., a term of type σ". Should the phrase "given a fixed local context" be added to this statement? Why can't we just declare a constant of the given type?

[Mario Carneiro]

The lam rule on page 6 shows how variables get added to the context (you read the rule from bottom to top)

[Mario Carneiro]

you usually construct derivation trees by starting with the statement of what you want to prove and the context you want to prove it in (usually initially empty), i.e. |- ? : my theorem, and then you work backwards applying rules, including the lam rule that adds a variable to the context. Eventually you get to a point where the thing you want to prove is in the context, and then the var rule allows you to deduce ..., x : A, ... |- x : A

[Mario Carneiro]

If you read rules from top to bottom, then the var rule appears to pull a context out of nowhere to prove x : A. The context is a set of assumptions, so this is fine

[Mario Carneiro]

depending on how you set things up, you can either require that the context is always valid, in which case the var rule would need a proof that C is a valid context, or you can only ensure this when adding variables (reading backwards), i.e. in the lam rule, in which case you would have a hypothesis C |- A : Type and C, x : A |- e : B yields C |- (\lam x : A, e) : A -> B

[Mario Carneiro]

On page 7: "Given a type σ, the type inhabitation problem consists of finding an “inhabitant” of that type—i.e., a term of type σ". Should the phrase "given a fixed local context" be added to this statement?

Yes, it is given a fixed local context, although WLOG you can assume the context is empty, by universally closing over all variables in the context.

Why can't we just declare a constant of the given type?

That is also known as adding an axiom. You can do it, but you have extended the system and now more things are provable

[Patrick Thomas]

I'm not sure how to read C |- A : Type? This is saying that A is a well formed type? And this is produced by going backwards from the lambda rule? Would there also be C |- B : Type then?

[Patrick Thomas]

"Yes, it is given a fixed local context, although WLOG you can assume the context is empty, by universally closing over all variables in the context."
If you are going backwards following steps 1 and 2 in the text, then you end up determining what the context needs to be for the type to be inhabited right?

[Mario Carneiro]

well generally the type is just given, i.e. the theorem statement

[Mario Carneiro]

and it should be a closed term, meaning it is valid in the empty context

[Mario Carneiro]

C |- A : Type means that A is a type that can refer to variables in C. For example A : Type, B : Type |- (A -> B) -> B : Type

[Mario Carneiro]

Would there also be C |- B : Type then?

That also depends on how you set up the theory. It is often implied from C, x : A |- e : B. It should also be C, x : A |- B : Type btw, this is one of the things that makes dependent type theory dependent

[Mario Carneiro]

although in that case you would write Pi x : A, B instead of A -> B for the type of the lambda

[Patrick Thomas]

Thank you.

[Jasmin Blanchette]

I've clarified the text a bit based on Patrick's initial comments. (Patrick, I'd like to add your name to the acknowledgments, if you don't object.)

Concerning your very first question, the answer is no. Variables are defined on p. 4, in italics. (What you see on p. 6 is a typing rule called "Var".) Concerning your second question, "I don't see a rule for adding a variable to the local context", well that's exactly what Lam does. On p. 7, what I had in mind was an empty context. I think that's how inhabitation is usually defined, and indeed if one isn't careful, one can say that every type is trivially inhabited, in some context.

[Jasmin Blanchette]

One more comment, perhaps as much to Mario as to Patrick: Our typing rules are deliberately simplistic and don't attempt to check that types are well typed. The whole section is about the simply typed fragment of DTT anyway, so we're following the HOL tradition of ignoring ill-formed (= ill-aried or undeclared) types altogether.

[Mario Carneiro]

Ah, yes I was aware of this, but realized during the explanation that I had to refer to concepts like C |- A : Type and |- C ok that weren't explained in the provided rules, so I ended up talking about some hybrid of STT and DTT which may have been more confusing. :/

[Patrick Thomas]

"Patrick, I'd like to add your name to the acknowledgments, if you don't object." I have no objections, I'd be honored.

Sorry, I was reading it from top to bottom instead of from bottom to top.

"if one isn't careful, one can say that every type is trivially inhabited, in some context." I think that is true? In the same sense that every proposition is trivially true under the right assumptions? If type inhabitation is usually defined as requiring an empty context, and you haven't already, would it help to add that to the text?

An unrelated question: On page 27 we have: "The eq.subst instance we use has ?a := a,?b := a’, and?p := (λx, f x b)". Should it be "?p := (λx, f a b = f x b)"?

[Mario Carneiro]

I think you are right about the last bit. That p looks like an argument to congr_arg, not eq.subst

[Patrick Thomas]

Ok. Thank you.

[Anne Baanen]

Patrick Thomas said:

An unrelated question: On page 27 we have: "The eq.subst instance we use has ?a := a,?b := a’, and?p := (λx, f x b)". Should it be "?p := (λx, f a b = f x b)"

Yes, it should be (λ x, f a b = f x b), as is also correctly substituted in the next line.

[Anne Baanen]

I have committed a fix to the guide, thank you!

[Jasmin Blanchette]

Patrick Thomas said:

If type inhabitation is usually defined as requiring an empty context, and you haven't already, would it help to add that to the text?

I completely agree. I fixed that in the text last week as well. ;)

[Patrick Thomas]

On page 54, should fact 0 = 1?

[Kevin Buzzard]

Ha ha you're not the first person to fall for this :-)

[Kevin Buzzard]

Yes and no

[Patrick Thomas]

?

[Kevin Buzzard]

read more

[Patrick Thomas]

By the way, I recognized a name here: https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

[Patrick Thomas]

I see, last paragraph.

[Patrick Thomas]

On page 65, in the definition of zip, I was curious why it was | (_ :: _) [] := [] instead of | _ [] := []?

[Patrick Thomas]

I see. I am guessing it is because | _ [] allows for | [] [] which is already an instance of the previous case and | (_ :: _) [] does not.

[Mario Carneiro]

they are equivalent. You will have to ask Jasmin

[Jasmin Blanchette]

The answer is given on p. 67:

In the definition of zip and in the proof of map_zip, we were careful to specify three nonoverlapping patterns. It is also possible to write equations with overlap- ping patterns, as in

I know chat makes it attractive to ask questions or write comments immediately, but a case could be made for reading until the end of a subsection before doing so. ;)

[Jasmin Blanchette]

A few lines below:

We generally recommend the latter, more explicit style, because it leads to fewer surprises, especially in proofs.

[Patrick Thomas]

I'm sorry, you're right.

[Jasmin Blanchette]

No worries. ;) I'm just warning you that I'm an old-fashioned author who expects his readers to keep on reading...

[Jasmin Blanchette]

I'm actually very happy when somebody, anybody, writes about the guide. I have no idea how many readers we have for it (10? 100? 1000?), how far they get, or what they think along the way.

[Jasmin Blanchette]

That is, apart from a few exceptions like you. Keep on reading, and keep on commenting (in that order I guess? ;)).

[Johan Commelin]

A Jasmin, you must be some dinosaur from the last century. These days you have to package your story in 3-minute video clips on youtube.

[Patrick Thomas]

What does 8791 mean?

[Jasmin Blanchette]

Good question. I entered 1978 but Zulip decided to turn it around.

[Jasmin Blanchette]

It's a reference to "some dinosaur from the last century".

[Patrick Thomas]

Ah. Only one year older than me :)

[Jasmin Blanchette]

I hope you're a Smashing Pumpkins fan then.

[Patrick Thomas]

:)

[Ian Riley]

Hey everyone, I’ve been reading over the guide and have been implementing the work under program semantics, such as big step and small step. I’ve implemented the state type as def state := \Pi (v : string), \nat . I tried constant first, and Lean reported errors when I used state in the definition of big step, such as ... : string -> (state -> \nat) -> stmt. Does anyone have any advice about the differences in using keywords constant, def, and axiom?

[Anne Baanen]

Hi! Indeed, it would not work if you use constant state : Type, for the reason that a constant creates a new, unspecified, term of a given type which is a priori different from the other values of that type.

[Anne Baanen]

When you write def state := \Pi (v : string), \nat, then Lean will remember the definition of state. So when it typechecks for example λ x, 0 : state, it will unfold the definition of state, and to get λ x, 0 : string -> nat, which does typecheck. If state was a constant, it does not know how to unfold and it gives up with an error.

[Anne Baanen]

There is a short discussion about axiom and constant when they are introduced in section 1.4 in the Guide.

[Ian Riley]

Thanks @Anne Baanen . That helps a lot actually,

[Ian Riley]

In the guide, it provides an inductive type for aexp. How would I define a function to reduce (aexp.var “x”) to “x”?

[Ian Riley]

And also how to define the notation such that s{x -> n} := (lambda ...)

[Mario Carneiro]

What do you want things other than aexp.var to reduce to?

[Mario Carneiro]

It might help to post a #mwe with your work since it serves as a useful framing device

[Mario Carneiro]

I'm not sure exactly what you mean by s{x -> n}, but I would guess it is something like function.update, that is, s{x -> n} y := if x = y then n else s y

[Patrick Thomas]

To make sure I understand. We have to do this:

inductive vec (α : Type) : ℕ → Type
| nil {} : vec 0
| cons (a : α) {n : ℕ} (v : vec n) : vec (n + 1)

and cannot do this:

inductive vec (α : Type) (n : ℕ) : Type
| nil {} : vec 0
| cons (a : α) {n : ℕ} (v : vec n) : vec (n + 1)

because we need to use different terms of type ℕ in the definition?

[Kenny Lau]

yes

[Patrick Thomas]

Thank you. What does the {} refer to after nil? It seems to still compile without it.

[Patrick Thomas]

Does it just mean all the arguments are implied?

[Patrick Thomas]

(deleted)

[Patrick Thomas]

(deleted)

[Ian Riley]

I have another question related to inductive types. Let's say that we have the following inductive type

inductive aexp : Type
| nat : \nat -> aexp
| num : \int -> aexp
| nil : aexp

We would like to show

#eval (aexp.nat 1) + (aexp.nat 1) = (aexp.nat 2)

without having to define add and equality for aexp. How would that be done?

[Jasmin Blanchette]

Patrick Thomas said:

Does it just mean all the arguments are implied?

See p. 67.

[Patrick Thomas]

This time I did read it, I just forgot it and couldn't find it again :) Does not putting {} in default to {}?

[Patrick Thomas]

#print shows the same result for both.

[Jasmin Blanchette]

I'm pretty sure it's different but I can't check now.

[Patrick Thomas]

No problem, not important, just curious. Thank you.

[Jasmin Blanchette]

I'd think without {} you'd have to write tree.empty nat instead of tree.empty, etc.

[Logan Murphy]

Ian Riley said:

We would like to show

#eval (aexp.nat 1) + (aexp.nat 1) = (aexp.nat 2)

without having to define add and equality for aexp. How would that be done?

The only way I can think of is just splitting the definition of addition into a coercion to nat/int and making a has_add instance. But it would be easier to just define addition for the whole type. For example, if I wanted to use integer addition I would write

def aexp.to_int : aexp → int
| (aexp.nat n) := int.of_nat n
| (aexp.num n) := n
| nil := 0

@[instance] def aexp.has_add : has_add aexp :=
⟨λ a b, aexp.num (int.add (aexp.to_int a) (aexp.to_int b))⟩

#reduce (aexp.num 4) + (aexp.num 6)

[Patrick Thomas]

In the game of tennis on page 75, is it correct that the defined inductive predicate terminates at adv.srv and adv.rcv? That is, it does not allow for returns to 40-40 or advances to game.srv and game.rcv as described in the informal rules?

[Patrick Thomas]

Is there a way to change the number in the browser tab to only reflect selected topics?

[Adam Topaz]

You mean in zulip? I guess you can "unsubscribe" from certain streams.

[Patrick Thomas]

Yeah in Zulip. I was hoping there might be an option I wasn't seeing.

[Reid Barton]

You can also mute streams or topics--I think this would affect the unread count but I haven't tried it

[Patrick Thomas]

It's not quite what I was hoping for, but it helps. Thank you.

[Adam Topaz]

(If you don't mind the number in your browser tab being a bit larger, you can subscribe to the zulip meta stream too...)

[Patrick Thomas]

Looks like it has already been brought up in the meta.

[Alexandre Rademaker]

Chapter 3 introduces the fix proof command. The Lean version I am using does not recognize this command. It seems that it is the same of assume. Does anyone know the origin of this command in the hitchhikers guide?

[Mario Carneiro]

It was a conscious choice on Jasmin's part

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Proposal.3A.20.60fix.20x.60.20for.20.60assume.20x.60/near/194764067

[Jasmin Blanchette]

In the next edition of the guide, this will be more clearly identified as a private extension.

[Jasmin Blanchette]

The guide was designed for in-class use, not as a Lean tutorial. I never expected it would be so popular as a tutorial.

[Alexandre Rademaker]

It is a very nice material, thank you for making it. But how do you define fix? Do you have any list of definitions besides fix that you share with students?

[Mario Carneiro]

fix is just a synonym for \lam or assume in standard lean

[Jasmin Blanchette]

It's called LoVelib. See footnote 3 in the preface for a URL.

[Patrick Thomas]

We do:

def list_of_vec {α : Type} : ∀ {n : N}, vec α n → list α
| _ vec.nil := []
| _ (vec.cons a v) := a :: list_of_vec v

instead of

def list_of_vec : ∀ {α : Type} {n : N}, vec α n → list α
| _ vec.nil := []
| _ (vec.cons a v) := a :: list_of_vec v

because α is a type and not a term?

[Mario Carneiro]

No, it is because α is a parameter of the recursion

[Mario Carneiro]

Also the second version would need an extra underscore in the patterns

[Patrick Thomas]

Oh. Ok.

[Patrick Thomas]

What precisely are the rules for figuring out what you are matching against based on the type? Everything after the :?

[Mario Carneiro]

Yes, there is one argument to be matched for every pi/arrow after the colon

[Jasmin Blanchette]

See p. 15 of HG.

[Patrick Thomas]

On page 75:
"In contrast, the inductive definition guarantees that we obtain the least (i.e., the most false) predicate that satisfies the introduction rules even.zero and even.add_two , and provides elimination and induction principles that allow us to prove ¬ even 1 , ¬ even 17 , or ¬ even (2 * n + 1) ."
Is there a way in Lean to see all the rules and principles that are generated?

[Kevin Buzzard]

Probably #print prefix even

[Patrick Thomas]

I think that just shows the declared constructors?

[Patrick Thomas]

Is there an example of proving something like ¬ even 1?

[Patrick Thomas]

Or 0 = 1 → false?

[Kyle Miller]

Patrick Thomas said:

Is there an example of proving something like ¬ even 1 without tactics?

Maybe it's a little disappointing, but this works:

inductive even : ℕ → Prop
| zero : even 0
| add_two : ∀k : ℕ, even k → even (k + 2)

example : ¬ even 1
.

The dot means "no more patterns" for the equation compiler. Somehow it knows even 1 cannot be constructed. This is the term mode proof that the equation compiler generates:

λ (a : even 1),
  a.dcases_on (λ (a_1 : 1 = 0), nat.no_confusion a_1)
    (λ (a_k : ℕ) (a_a : even a_k) (a_1 : 1 = (a_k.add (1.add 0)).succ),
       nat.no_confusion a_1 (λ (a_1 : 0 = (a_k.add 0).succ), nat.no_confusion a_1))
    (eq.refl 1)
    (heq.refl a)

(I changed example to lemma foo then did #print foo.)

[Patrick Thomas]

Hmm. Ok. Are inductive data types defined in lambda calculus or are they something that functional programming languages tack on somehow?

[Patrick Thomas]

Everything is encoded as a function I guess? So an inductive data type must be encoded as a function?

[Patrick Thomas]

Is there a way to see that function?

[Patrick Thomas]

Like and reduces to lx.ly.xyx?

[Floris van Doorn]

Inductive types are primitive, they are not defined as anything, they are constants, with rules (constructors, recursors, computation rules) postulated for them.

[Floris van Doorn]

See Mario's thesis for the precise rules: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Patrick Thomas]

It appears to be over my head at present, but thank you.

[Floris van Doorn]

A much better introduction is https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

[Patrick Thomas]

Are definitions like and = lx.ly.xyx used at any level or are they replaced by other methods in languages like Lean? Because honestly those definitions are pretty cool :)

[Alex J. Best]

In lean bool is an inductive type in lean with two constructors, tt and ff, so any term you construct of bool is one of the two, and then boolean functions can just be defined by matching against those constructors. As we have types its not necessary to encode everything as a function in some clever way to get the desired behaviour, as Floris says inductive types themselves are a primitive notion. Its like how in set theory naturals can be encoded via von Neumann ordinals as sets of sets, but in type theories such as lean's we can make an inductive type to represent naturals instead of having to define everything as a set.

[Patrick Thomas]

I see. Thank you.

[Logan Murphy]

I'm not sure if tactic.any_goals was changed since the book was written, but when trying to typecheck the first custom tactic example

import tactic

inductive even : ℕ → Prop
| zero : even 0
| add_two : ∀ k : ℕ, even k → even (k + 2)

meta def intro_and_even : tactic unit :=
do
  tactic.repeat (tactic.applyc ``and.intro),
  tactic.any_goals (tactic.solve1 (tactic.repeat
    (tactic.applyc ``even.add_two
     <|> tactic.applyc ``even.zero)))

it seems the return type is tactic (list (option unit)) rather than tactic unit. Is there a way to get this to the type tactic unit? (Just starting to learn metaprogramming now)

[Logan Murphy]

By the way, I've found the HG to be a very useful supplement to TPiL, so my thanks to the authors!

[Alex J. Best]

You can put

     return ⟨⟩

on a newline after any_goals

meta def intro_and_even : tactic unit :=
do
  tactic.repeat (tactic.applyc ``and.intro),
  tactic.any_goals (tactic.solve1 (tactic.repeat
    (tactic.applyc ``even.add_two
     <|> tactic.applyc ``even.zero))),
     return ⟨⟩

to get the right type

[Floris van Doorn]

The typical way to throw out a result it to write >> skip after a tactic. In this case, you can do

meta def intro_and_even : tactic unit :=
do
  tactic.repeat (tactic.applyc ``and.intro),
  tactic.any_goals (tactic.solve1 (tactic.repeat
    (tactic.applyc ``even.add_two
     <|> tactic.applyc ``even.zero))),
  skip

[Floris van Doorn]

(Alex's suggestion is basically the same, since skip is defined to be return ⟨⟩)

[Logan Murphy]

Thanks!

[Alex J. Best]

Although my using angle braces instead of brackets is a bit idiosyncratic I guess!

[Alex J. Best]

return () is used in mathlib way more often.

[Jasmin Blanchette]

Logan Murphy said:

I'm not sure if tactic.any_goals was changed since the book was written

It has. We've updated our private version of the book but have yet to update the PDF. Expect a new version within one month or so, in time for my course.