## Stream: new members

### Topic: hitchhikers guide

#### Patrick Thomas (Aug 18 2020 at 19:20):

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 (Aug 18 2020 at 19:31):

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

#### Mario Carneiro (Aug 18 2020 at 19:33):

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 (Aug 18 2020 at 19:35):

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 (Aug 18 2020 at 19:37):

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 (Aug 18 2020 at 19:39):

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 (Aug 18 2020 at 20:15):

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 (Aug 18 2020 at 20:22):

"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 (Aug 18 2020 at 20:56):

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

#### Mario Carneiro (Aug 18 2020 at 20:56):

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

#### Mario Carneiro (Aug 18 2020 at 20:57):

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 (Aug 18 2020 at 21:00):

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 (Aug 18 2020 at 21:01):

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

Thank you.

#### Jasmin Blanchette (Aug 20 2020 at 11:06):

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 (Aug 20 2020 at 11:12):

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 (Aug 20 2020 at 17:33):

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 (Aug 24 2020 at 02:29):

"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 (Aug 24 2020 at 02:46):

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

Ok. Thank you.

#### Anne Baanen (Aug 24 2020 at 08:59):

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 (Aug 24 2020 at 09:12):

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

#### Jasmin Blanchette (Aug 24 2020 at 10:56):

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 (Aug 28 2020 at 01:07):

On page 54, should fact 0 = 1?

#### Kevin Buzzard (Aug 28 2020 at 07:27):

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

Yes and no

?

#### Patrick Thomas (Aug 28 2020 at 20:41):

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

#### Patrick Thomas (Aug 28 2020 at 20:44):

I see, last paragraph.

#### Patrick Thomas (Aug 30 2020 at 19:31):

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

#### Patrick Thomas (Aug 31 2020 at 01:20):

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

#### Mario Carneiro (Aug 31 2020 at 01:33):

they are equivalent. You will have to ask Jasmin

#### Jasmin Blanchette (Aug 31 2020 at 19:31):

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 (Aug 31 2020 at 19:32):

A few lines below:

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

#### Patrick Thomas (Aug 31 2020 at 22:33):

I'm sorry, you're right.

#### Jasmin Blanchette (Sep 01 2020 at 07:33):

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

#### Jasmin Blanchette (Sep 01 2020 at 07:34):

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 (Sep 01 2020 at 07:35):

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

#### Johan Commelin (Sep 01 2020 at 07:38):

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 (Sep 02 2020 at 16:16):

What does 8791 mean?

#### Jasmin Blanchette (Sep 02 2020 at 16:38):

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

#### Jasmin Blanchette (Sep 02 2020 at 16:38):

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

#### Patrick Thomas (Sep 02 2020 at 16:39):

Ah. Only one year older than me :)

#### Jasmin Blanchette (Sep 02 2020 at 16:39):

I hope you're a Smashing Pumpkins fan then.

:)

#### Ian Riley (Sep 03 2020 at 14:14):

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 (Sep 03 2020 at 15:04):

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 (Sep 03 2020 at 15:05):

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 (Sep 03 2020 at 15:12):

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

#### Ian Riley (Sep 03 2020 at 16:42):

Thanks @Anne Baanen . That helps a lot actually,

#### Ian Riley (Sep 03 2020 at 22:28):

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 (Sep 04 2020 at 00:16):

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

#### Mario Carneiro (Sep 04 2020 at 00:21):

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

#### Mario Carneiro (Sep 04 2020 at 00:22):

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

#### Mario Carneiro (Sep 04 2020 at 00:23):

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 (Sep 04 2020 at 19:22):

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?

yes

#### Patrick Thomas (Sep 04 2020 at 19:31):

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

#### Patrick Thomas (Sep 04 2020 at 19:32):

Does it just mean all the arguments are implied?

(deleted)

(deleted)

#### Ian Riley (Sep 04 2020 at 21:18):

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 (Sep 04 2020 at 21:20):

Patrick Thomas said:

Does it just mean all the arguments are implied?

See p. 67.

#### Patrick Thomas (Sep 04 2020 at 21:23):

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

#### Patrick Thomas (Sep 04 2020 at 21:24):

#print shows the same result for both.

#### Jasmin Blanchette (Sep 04 2020 at 21:25):

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

#### Patrick Thomas (Sep 04 2020 at 21:25):

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

#### Jasmin Blanchette (Sep 04 2020 at 21:45):

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

#### Logan Murphy (Sep 05 2020 at 00:32):

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

⟨λ a b, aexp.num (int.add (aexp.to_int a) (aexp.to_int b))

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

#### Patrick Thomas (Sep 11 2020 at 17:08):

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 (Sep 11 2020 at 17:56):

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

#### Adam Topaz (Sep 11 2020 at 19:45):

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

#### Patrick Thomas (Sep 11 2020 at 19:47):

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

#### Reid Barton (Sep 11 2020 at 19:48):

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

#### Patrick Thomas (Sep 11 2020 at 20:05):

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

#### Adam Topaz (Sep 11 2020 at 20:10):

(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 (Sep 11 2020 at 21:38):

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

#### Alexandre Rademaker (Sep 13 2020 at 03:40):

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 (Sep 13 2020 at 04:00):

It was a conscious choice on Jasmin's part

#### Jasmin Blanchette (Sep 13 2020 at 08:40):

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

#### Jasmin Blanchette (Sep 13 2020 at 08:42):

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 (Sep 13 2020 at 14:28):

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 (Sep 13 2020 at 14:29):

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

#### Jasmin Blanchette (Sep 13 2020 at 16:17):

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

#### Patrick Thomas (Sep 14 2020 at 01:15):

We do:

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

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 (Sep 14 2020 at 01:27):

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

#### Mario Carneiro (Sep 14 2020 at 01:28):

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

Oh. Ok.

#### Patrick Thomas (Sep 14 2020 at 01:34):

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

#### Mario Carneiro (Sep 14 2020 at 07:26):

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

See p. 15 of HG.

#### Patrick Thomas (Sep 14 2020 at 20:03):

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 (Sep 14 2020 at 20:26):

Probably #print prefix even

#### Patrick Thomas (Sep 14 2020 at 20:33):

I think that just shows the declared constructors?

#### Patrick Thomas (Sep 14 2020 at 23:41):

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

#### Patrick Thomas (Sep 15 2020 at 01:56):

Or 0 = 1 → false?

#### Kyle Miller (Sep 15 2020 at 02:26):

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 (Sep 15 2020 at 02:49):

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

#### Patrick Thomas (Sep 15 2020 at 03:00):

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

#### Patrick Thomas (Sep 15 2020 at 03:01):

Is there a way to see that function?

#### Patrick Thomas (Sep 15 2020 at 03:05):

Like and reduces to lx.ly.xyx?

#### Floris van Doorn (Sep 15 2020 at 03:15):

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 (Sep 15 2020 at 03:17):

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

#### Patrick Thomas (Sep 15 2020 at 03:35):

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

#### Floris van Doorn (Sep 15 2020 at 04:06):

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

#### Patrick Thomas (Sep 15 2020 at 21:14):

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 (Sep 15 2020 at 21:47):

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 (Sep 15 2020 at 21:49):

I see. Thank you.

#### Logan Murphy (Sep 16 2020 at 18:44):

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 (Sep 16 2020 at 18:50):

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 (Sep 16 2020 at 18:54):

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 (Sep 16 2020 at 18:54):

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 (Sep 16 2020 at 18:55):

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

Thanks!

#### Alex J. Best (Sep 16 2020 at 18:57):

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

#### Alex J. Best (Sep 16 2020 at 18:57):

return () is used in mathlib way more often.

#### Jasmin Blanchette (Sep 17 2020 at 09:01):

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.

Last updated: Dec 20 2023 at 11:08 UTC