Zulip Chat Archive

Stream: new members

Topic: hitchhikers guide


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 18 2020 at 20:56):

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

view this post on Zulip Mario Carneiro (Aug 18 2020 at 20:56):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Aug 18 2020 at 21:57):

Thank you.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. :/

view this post on Zulip 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)"?

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Aug 24 2020 at 02:49):

Ok. Thank you.

view this post on Zulip 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.

view this post on Zulip Anne Baanen (Aug 24 2020 at 09:12):

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

view this post on Zulip 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. ;)

view this post on Zulip Patrick Thomas (Aug 28 2020 at 01:07):

On page 54, should fact 0 = 1?

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 07:27):

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

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 07:27):

Yes and no

view this post on Zulip Patrick Thomas (Aug 28 2020 at 20:38):

?

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 20:40):

read more

view this post on Zulip 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/

view this post on Zulip Patrick Thomas (Aug 28 2020 at 20:44):

I see, last paragraph.

view this post on Zulip Patrick Thomas (Aug 30 2020 at 19:31):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 31 2020 at 01:33):

they are equivalent. You will have to ask Jasmin

view this post on Zulip 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. ;)

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Aug 31 2020 at 22:33):

I'm sorry, you're right.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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? ;)).

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Sep 02 2020 at 16:16):

What does 8791 mean?

view this post on Zulip Jasmin Blanchette (Sep 02 2020 at 16:38):

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

view this post on Zulip Jasmin Blanchette (Sep 02 2020 at 16:38):

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

view this post on Zulip Patrick Thomas (Sep 02 2020 at 16:39):

Ah. Only one year older than me :)

view this post on Zulip Jasmin Blanchette (Sep 02 2020 at 16:39):

I hope you're a Smashing Pumpkins fan then.

view this post on Zulip Patrick Thomas (Sep 02 2020 at 16:40):

:)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ian Riley (Sep 03 2020 at 16:42):

Thanks @Anne Baanen . That helps a lot actually,

view this post on Zulip 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”?

view this post on Zulip Ian Riley (Sep 04 2020 at 00:16):

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

view this post on Zulip Mario Carneiro (Sep 04 2020 at 00:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 04 2020 at 19:28):

yes

view this post on Zulip Patrick Thomas (Sep 04 2020 at 19:31):

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

view this post on Zulip Patrick Thomas (Sep 04 2020 at 19:32):

Does it just mean all the arguments are implied?

view this post on Zulip Patrick Thomas (Sep 04 2020 at 20:49):

(deleted)

view this post on Zulip Patrick Thomas (Sep 04 2020 at 20:50):

(deleted)

view this post on Zulip 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?

view this post on Zulip Jasmin Blanchette (Sep 04 2020 at 21:20):

Patrick Thomas said:

Does it just mean all the arguments are implied?

See p. 67.

view this post on Zulip 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 {}?

view this post on Zulip Patrick Thomas (Sep 04 2020 at 21:24):

#print shows the same result for both.

view this post on Zulip Jasmin Blanchette (Sep 04 2020 at 21:25):

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

view this post on Zulip Patrick Thomas (Sep 04 2020 at 21:25):

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

view this post on Zulip 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.

view this post on Zulip 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

@[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)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Sep 11 2020 at 19:45):

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

view this post on Zulip Patrick Thomas (Sep 11 2020 at 19:47):

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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Sep 11 2020 at 20:05):

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

view this post on Zulip 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...)

view this post on Zulip Patrick Thomas (Sep 11 2020 at 21:38):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 13 2020 at 04:00):

It was a conscious choice on Jasmin's part

view this post on Zulip Mario Carneiro (Sep 13 2020 at 04:00):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:29):

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

view this post on Zulip Jasmin Blanchette (Sep 13 2020 at 16:17):

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

view this post on Zulip 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

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?

view this post on Zulip Mario Carneiro (Sep 14 2020 at 01:27):

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

view this post on Zulip Mario Carneiro (Sep 14 2020 at 01:28):

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

view this post on Zulip Patrick Thomas (Sep 14 2020 at 01:32):

Oh. Ok.

view this post on Zulip 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 :?

view this post on Zulip Mario Carneiro (Sep 14 2020 at 07:26):

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

view this post on Zulip Jasmin Blanchette (Sep 14 2020 at 08:00):

See p. 15 of HG.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 20:26):

Probably #print prefix even

view this post on Zulip Patrick Thomas (Sep 14 2020 at 20:33):

I think that just shows the declared constructors?

view this post on Zulip Patrick Thomas (Sep 14 2020 at 23:41):

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

view this post on Zulip Patrick Thomas (Sep 15 2020 at 01:56):

Or 0 = 1 → false?

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Patrick Thomas (Sep 15 2020 at 03:01):

Is there a way to see that function?

view this post on Zulip Patrick Thomas (Sep 15 2020 at 03:05):

Like and reduces to lx.ly.xyx?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Sep 15 2020 at 03:35):

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

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Sep 15 2020 at 21:49):

I see. Thank you.

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Sep 16 2020 at 18:55):

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

view this post on Zulip Logan Murphy (Sep 16 2020 at 18:56):

Thanks!

view this post on Zulip Alex J. Best (Sep 16 2020 at 18:57):

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

view this post on Zulip Alex J. Best (Sep 16 2020 at 18:57):

return () is used in mathlib way more often.

view this post on Zulip 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: May 16 2021 at 05:21 UTC