# Zulip Chat Archive

## Stream: new members

### Topic: tutorial about tactics?

#### Alexandre Rademaker (Sep 24 2019 at 01:22):

I am trying to understand tatics, how to prove the second lemma below? How to introduce a term `f a`

? Does anyone have any additional tutorial about tatics?

lemma lx1 (p q : ℕ → Prop) (f : ℕ → ℕ) : (∀ x : ℕ, p x) → (∀ x : ℕ, p (f x)) := begin intro h, intro a, exact h (f a) end lemma lx2 (p q : ℕ → Prop) (f : ℕ → ℕ) : (∀ x : ℕ, p (f x)) → (∀ x : ℕ, p x) := begin intro h, intro a, end

#### Floris van Doorn (Sep 24 2019 at 01:25):

The second lemma is false: the assumption is weaker than the conclusion.

#### Floris van Doorn (Sep 24 2019 at 01:28):

For some basics on tactics, you can take a look at the reference manual: https://leanprover.github.io/reference/tactics.html

#### Jesse Michael Han (Sep 24 2019 at 01:28):

if you also knew that `f`

was surjective, then you could case on that hypothesis to "introduce" a term of the form `f a`

(as it is, you could apply `lx2`

to the constant function to zero)

#### Alexandre Rademaker (Sep 24 2019 at 01:28):

Yep, this is the one I am reading. I was wondering if someone have any additional material.

#### Floris van Doorn (Sep 24 2019 at 01:31):

There is a list of all tactics defined in mathlib here: https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

But that is not at all a tutorial, more like a reference guide (and most tactics in it are very specialized).

#### Kevin Buzzard (Sep 24 2019 at 01:36):

You've presumably read the chapter in Theorem Proving In Lean on tactics?

#### Alexandre Rademaker (Sep 24 2019 at 01:40):

Yes, as I said above this is the one I am reading now.

#### Kevin Buzzard (Sep 24 2019 at 01:41):

My crappy notes from last year: http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_sheet_1/M1F_sheet_1_part_1.html

#### Kevin Buzzard (Sep 24 2019 at 01:41):

I will hopefully get something better written this year; I have some time later on in the week.

#### Alexandre Rademaker (Sep 24 2019 at 01:41):

My real goal is to prove

example (p q : ℕ → Prop) (f : ℕ → ℕ) : (∀x:ℕ, p (f x) → ∀x: ℕ, q (f x)) ∧ (∀ x: ℕ, p x) → ∃ x: ℕ, q x := begin intro h, end

proving lemma `lx1`

was just one exercise. But yes, you are right, `lx2`

is not a theorem without assuming more about f.

#### Kevin Buzzard (Sep 24 2019 at 01:43):

Do all of the exercises in TPIL and then discover your own exercises (e.g. work through a book). Just practice and keep asking here. That's my advice.

#### Kevin Buzzard (Sep 24 2019 at 01:45):

My real goal is to prove

example (p q : ℕ → Prop) (f : ℕ → ℕ) : (∀x:ℕ, p (f x) → ∀x: ℕ, q (f x)) ∧ (∀ x: ℕ, p x) → ∃ x: ℕ, q x := begin intro h, end

`h`

is a proof, but it's a proof of something quite messy. Do you know what the "head symbol" of h is? Is it called that? The "head term" or something? What tactic can you do to change `h`

?

#### Alexandre Rademaker (Sep 24 2019 at 01:45):

Thank you @Kevin Buzzard

#### Alexandre Rademaker (Sep 24 2019 at 01:46):

the head symbol of h is the conjunction.

#### Kevin Buzzard (Sep 24 2019 at 01:46):

And do you know the tactic which will replace h by its two parts?

#### Mario Carneiro (Sep 24 2019 at 01:47):

could you be more explicit of the precedence of the first conjunct of h? I'm not sure if it's the one you want

#### Alexandre Rademaker (Sep 24 2019 at 01:47):

From the left of the conjunction of h, we can obtain `forall x : nat, p f x`

and using MP I hope to obtain the conclusion,

#### Mario Carneiro (Sep 24 2019 at 01:48):

yep, that's not the precedence you wrote

#### Kevin Buzzard (Sep 24 2019 at 01:48):

Looking at the tactic state I am inclined to agree with Mario. My tactic state looks like this:

1 goal p q : ℕ → Prop, f : ℕ → ℕ, h1 : ∀ (x : ℕ), p (f x) → ∀ (x : ℕ), q (f x), h2 : ∀ (x : ℕ), p x ⊢ ∃ (x : ℕ), q x

#### Mario Carneiro (Sep 24 2019 at 01:48):

you need parentheses around `(∀ (x : ℕ), p (f x))`

#### Kevin Buzzard (Sep 24 2019 at 01:49):

That first "forall x : nat" stretches a long way otherwise

#### Alexandre Rademaker (Sep 24 2019 at 01:49):

I have this parenthesis. My state after the intro is

p q : ℕ → Prop, f : ℕ → ℕ, h : (∀ (x : ℕ), p (f x) → ∀ (x : ℕ), q (f x)) ∧ ∀ (x : ℕ), p x ⊢ ∃ (x : ℕ), q x

#### Kevin Buzzard (Sep 24 2019 at 01:50):

`h1 : ∀ (x : ℕ), (p (f x) → ∀ (y : ℕ), q (f y))`

#### Kevin Buzzard (Sep 24 2019 at 01:50):

split your `h`

with the `split`

tactic so you can see what's going on a bit better.

#### Kevin Buzzard (Sep 24 2019 at 01:50):

We have an operator precedence issue.

#### Mario Carneiro (Sep 24 2019 at 01:50):

not split, that splits the goal

#### Mario Carneiro (Sep 24 2019 at 01:50):

`cases h with h1 h2`

should do

#### Kevin Buzzard (Sep 24 2019 at 01:50):

yeah, `cases h`

#### Kevin Buzzard (Sep 24 2019 at 01:50):

sorry

#### Kevin Buzzard (Sep 24 2019 at 01:51):

I'm rubbish at Lean

#### Mario Carneiro (Sep 24 2019 at 01:51):

maybe `split at h`

should mean `cases h`

#### Kevin Buzzard (Sep 24 2019 at 01:52):

Your problem is that your `h`

is of this type: `(∀ (x : ℕ), (p (f x) → ∀ (x : ℕ), q (f x))) ∧ ∀ (x : ℕ), p x`

#### Kevin Buzzard (Sep 24 2019 at 01:52):

and this is independent of the fact that half of us don't know how to use basic tactics.

#### Alexandre Rademaker (Sep 24 2019 at 01:53):

Hum, cases worked somehow. Now I have

p q : ℕ → Prop, f : ℕ → ℕ, h1 : (∀ (x : ℕ), p (f x)) → ∀ (x : ℕ), q (f x), h2 : ∀ (x : ℕ), p x ⊢ ∃ (x : ℕ), q x

#### Mario Carneiro (Sep 24 2019 at 01:53):

that looks better

#### Kevin Buzzard (Sep 24 2019 at 01:54):

now what's the maths proof?

#### Kevin Buzzard (Sep 24 2019 at 01:54):

I'm on steadier ground there.

#### Alexandre Rademaker (Sep 24 2019 at 01:54):

Now I need to work with h2 to obtain the premisse of h1 to apply MP. With that result, I can obtain the conclusion.

#### Mario Carneiro (Sep 24 2019 at 01:55):

You can try working from the end, or `have`

ing an intermediate state

#### Kevin Buzzard (Sep 24 2019 at 01:55):

That's right. In Lean many tactics work backwords from the goal. Do you think you could write the entire argument backwards?

#### Mario Carneiro (Sep 24 2019 at 01:55):

working from the end, what's the existential witness here?

#### Kevin Buzzard (Sep 24 2019 at 01:56):

And then what's the tactic you can use to proceed?

#### Kevin Buzzard (Sep 24 2019 at 01:57):

I like to think that every head symbol has a "tactic-constructor" and a "tactic-eliminator" -- the first is the tactic you use if you want to move on `blah`

and `blah`

is in the goal, and the second is the tactic you use if you want to use `blah`

and `blah`

is in a hypothesis.

#### Alexandre Rademaker (Sep 24 2019 at 02:08):

Hum, almost there...

p q : ℕ → Prop, f : ℕ → ℕ, h1 : (∀ (x : ℕ), p (f x)) → ∀ (x : ℕ), q (f x), h2 : ∀ (x : ℕ), p x, h3 : ∀ (x : ℕ), p (f x), h4 : ∀ (x : ℕ), q (f x) ⊢ ∃ (x : ℕ), q x

#### Bryan Gin-ge Chen (Sep 24 2019 at 02:21):

Try using the `existsi`

tactic (I think it's deprecated in favor of `use`

now though).

#### Kevin Buzzard (Sep 24 2019 at 03:10):

can you post precisely what you are now trying to prove?

#### Kevin Buzzard (Sep 24 2019 at 03:10):

It would be interesting to see your proof.

#### Alexandre Rademaker (Sep 24 2019 at 09:47):

Hi @Kevin Buzzard , my current state is the following. I am just trying to complete this proof.

example (p q : ℕ → Prop) (f : ℕ → ℕ) : ((∀x:ℕ, p (f x)) → (∀x: ℕ, q (f x))) ∧ (∀ x: ℕ, p x) → ∃ x: ℕ, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : ℕ), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : ℕ), q (f x), from (h1 h3), end

#### Alexandre Rademaker (Sep 24 2019 at 09:51):

Hi @Bryan Gin-ge Chen , if I try `existsi (f a)`

it says that `a`

is unknow.

#### Chris Hughes (Sep 24 2019 at 09:53):

There's no variable called `a`

in your context. Try `existsi (f 0)`

#### Alexandre Rademaker (Sep 24 2019 at 10:09):

Wow! It worked!! So happy!! ;-) It looks like I have a proof. But why I can't use a generic term of type `nat`

instead of `0`

in the last step? It should be possible to prove `∀ (x : ℕ), q (f x) ⊢ ∃ (x : ℕ), q x`

for any nat, right?

example (p q : ℕ → Prop) (f : ℕ → ℕ) : ((∀x:ℕ, p (f x)) → (∀x: ℕ, q (f x))) ∧ (∀ x: ℕ, p x) → ∃ x: ℕ, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : ℕ), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : ℕ), q (f x), from (h1 h3), existsi (f 0), exact (h4 0) end

#### Chris Hughes (Sep 24 2019 at 10:14):

You could use any `nat`

other than `0`

for the proof. Using an arbitrary `nat`

when there isn't one in your context could cause problems if the type `nat`

was empty. Your example is actually false with `nat`

substituted for `empty`

in the statement.

#### Alexandre Rademaker (Sep 24 2019 at 10:19):

Sorry, I didn’t understand. The reason for my question is that it should be possible to replace the type `nat`

with a generic type `U : Type`

, right?

#### Chris Hughes (Sep 24 2019 at 10:34):

Only if `U`

is nonempty

#### Kevin Buzzard (Sep 24 2019 at 10:35):

....

#### Alexandre Rademaker (Sep 24 2019 at 10:39):

Yes, if U is nonempty, an usual assumption for domains in first order logic. In that case, how can I replace nat by U saying that U is nonempty?

#### Keeley Hoek (Sep 24 2019 at 10:42):

To minimally change your existing proof:

example {α : Type} [hne : nonempty α] (p q : α → Prop) (f : α → α) : ((∀x:α, p (f x)) → (∀x: α, q (f x))) ∧ (∀ x: α, p x) → ∃ x: α, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : α), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : α), q (f x), from (h1 h3), have a : α := classical.choice hne, existsi (f a), exact (h4 a), end

#### Keeley Hoek (Sep 24 2019 at 10:43):

If you would like a witness to the nonemptiness of the type `α`

to actually be provided, use `inhabited`

instead of `nonempty`

#### Alexandre Rademaker (Sep 24 2019 at 10:46):

Wow! Too many new things! I am curious why this discussion of nonempty types didn't appear in the chapter 9 of Logic and Proof!

Thank you @Keeley Hoek ! Now I have to understand why the `{ ...}`

, the use of `[...]`

in the declaration instead of `(...)`

and the `classical.choice`

operator.

#### Keeley Hoek (Sep 24 2019 at 10:47):

What I've done is just replaced each use of nat with an arbitrary type `α`

, but have required that a proof that `α`

is `nonempty`

is also provided.

#### Keeley Hoek (Sep 24 2019 at 10:48):

To obtain an actual element `a`

of `α`

based on the proof of nonemptiness `hne`

, we appeal to the axiom of choice.

#### Marc Huisinga (Sep 24 2019 at 10:50):

nonempty is also introduced here: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#choice

#### Keeley Hoek (Sep 24 2019 at 10:51):

The curly and square brackets aren't necessary. They would be instructions to lean for anyone trying to use your proof, if it was a `def`

, and not an `example`

. The curly braces instruct lean to always guess `α`

and never ask for it to be provided. The square brackets are trickier, and ask lean to perform so-called typeclass inference to obtain the proof of nonemptiness. You can read more about both of these in the book.

#### Keeley Hoek (Sep 24 2019 at 10:51):

So, they just make it easier to use. There are no implications for your actual proof.

#### Alexandre Rademaker (Sep 24 2019 at 10:52):

I didn't understand the difference between nonempty and inhabited! hne isn't a witness?

#### Keeley Hoek (Sep 24 2019 at 10:52):

No. It is a proof that it is nonempty. The witness has been forgotten.

#### Keeley Hoek (Sep 24 2019 at 10:53):

It's because `nonempty`

is defined to live in the universe `Prop`

, but `inhabited`

lives in `Type`

(roughly speaking).

#### Keeley Hoek (Sep 24 2019 at 10:53):

So `inhabited`

instances can be deconstructed, but `nonempty`

instances cannot be deconstructed once built.

#### Keeley Hoek (Sep 24 2019 at 10:53):

Otherwise, they have the same definition exactly.

#### Marc Huisinga (Sep 24 2019 at 10:54):

{...} and [...] are also explained here:

https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

#### Alexandre Rademaker (Sep 24 2019 at 10:55):

Thank you @Marc Huisinga for the links.

#### Alexandre Rademaker (Sep 24 2019 at 11:36):

Thank you @Keeley Hoek for the solution and detailed explanation.

#### Mario Carneiro (Sep 24 2019 at 17:57):

Since it wasn't mentioned: it is not necessary to use choice to extract a witness here, because the theorem being proved is itself a prop, so you can use `cases hne with a`

in place of `have a : α := classical.choice hne`

in Keeley's proof.

#### Floris van Doorn (Sep 24 2019 at 17:58):

You probably have to do `have := hne, cases this with a`

(or `unfreezeI, cases hne with a`

) for technical reasons.

#### Alexandre Rademaker (Sep 25 2019 at 00:29):

Thank you @Mario Carneiro and @Floris van Doorn , the final proof is below. I prefer explicit identifiers, that is why I used y. I am not sure if I understood the intuition behind this `have ... cases ... with ...`

! The `unfreezeI`

is probably from the mathlib, right? I didn't find it in my system.

example {α : Type} [hne : nonempty α] (p q : α → Prop) (f : α → α) : ((∀ x : α, p (f x)) → (∀ x : α, q (f x))) ∧ (∀ x : α, p x) → ∃ x : α, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : α), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : α), q (f x), from (h1 h3), have y := hne, cases y with a, existsi (f a), exact (h4 a), end

#### Mario Carneiro (Sep 25 2019 at 00:30):

you can also use `cases id hne with a`

#### Mario Carneiro (Sep 25 2019 at 00:32):

The technical reason is that `nonempty A`

is a class, which means that that argument is "frozen" in the local context in order to cache and speed up typeclass searches. There are several mathlib tactics ending in `*I`

that unfreeze these instances so that you can remove them from the context (which is what `cases hne`

wants to do)

#### Mario Carneiro (Sep 25 2019 at 00:33):

they are available via `import tactic.cache`

#### Mario Carneiro (Sep 25 2019 at 00:35):

If you don't have mathlib, you can also use `tactic.unfreeze_local_instances`

for which `unfreezeI`

is a synonym

#### Alexandre Rademaker (Sep 26 2019 at 02:03):

Hum, `case id hne with a`

is simpler than `have y := hne, cases y with a`

, but I am still trying to understand the rationality of this tactic `case`

. The docstring of `case`

if not very informative! To close this thread, I need to make one additional question. I started the proof using the type `nat`

, when we moved to the arbitrary `α`

type above, we had to say that it is nonempty and we used `hne`

(the proof of its nonemptiness) to obtain an arbitrary element. If we go back to the `nat`

, how could I use an arbitrary natural number instead of `0`

or any other magically available number already defined in the Lean environment? In the proof using `nat`

below, I didn't need to introduce `[hne : nonempty ℕ]`

, this type is probably already defined elsewhere as nonempty, right? That is, it works with any already defined number but I would like to have a more 'general' proof in `nat`

, saying that ANY number (like an `a`

) would work.

example (p q : ℕ → Prop) (f : ℕ → ℕ) : ((∀ x : ℕ, p (f x)) → (∀ x : ℕ, q (f x))) ∧ (∀ x : ℕ, p x) → ∃ x : ℕ, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : ℕ), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : ℕ), q (f x), from (h1 h3), existsi (f 10), exact (h4 10), end

Does it make sense?

#### Bryan Gin-ge Chen (Sep 26 2019 at 02:20):

You can use `apply_instance`

:

example (p q : ℕ → Prop) (f : ℕ → ℕ) : ((∀ x : ℕ, p (f x)) → (∀ x : ℕ, q (f x))) ∧ (∀ x : ℕ, p x) → ∃ x : ℕ, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : ℕ), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : ℕ), q (f x), from (h1 h3), have y : nonempty ℕ := by apply_instance, cases y with a, existsi (f a), exact (h4 a), end

(assuming I understood what you want)

#### Mario Carneiro (Sep 26 2019 at 02:21):

It doesn't really make sense. The proof requires you to use *some* natural number to do the cut, and if you want to quantify over different witnesses you have to change the theorem statement

#### Mario Carneiro (Sep 26 2019 at 02:22):

One way to express this is to add an argument `n`

to the theorem:

example (p q : ℕ → Prop) (f : ℕ → ℕ) (n : ℕ) : ((∀ x : ℕ, p (f x)) → (∀ x : ℕ, q (f x))) ∧ (∀ x : ℕ, p x) → ∃ x : ℕ, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : ℕ), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : ℕ), q (f x), from (h1 h3), existsi (f n), exact (h4 n), end

But no one would want to use this theorem because the argument `n`

is useless (has no bearing on the fact to be proven)

#### Mario Carneiro (Sep 26 2019 at 02:23):

This sort of thing is often done for functions, where we actually care about dependence of the definition on the argument even if the type is fixed, but for proofs we want to minimize assumptions because proofs are irrelevant

#### Alexandre Rademaker (Sep 26 2019 at 15:56):

Hi @Bryan Gin-ge Chen , nice I learned one more thing! The `apply_instance`

tactic seems to use the previous definition of `nat`

as non empty right? Trying it with the type `α`

didn't work.

example {α : Type} (p q : α → Prop) (f : α → α) : ((∀ x : α, p (f x)) → (∀ x : α, q (f x))) ∧ (∀ x : α, p x) → ∃ x : α, q x := begin intro h, cases h with h1 h2, have h3 : ∀ (x : α), p (f x), assume a, from h2 (f a), have h4 : ∀ (x : α), q (f x), from (h1 h3), have hne : nonempty α := by apply_instance, cases hne with a, existsi (f a), exact (h4 a), end

causes the error:

tactic.mk_instance failed to generate instance for nonempty α

In other words, the line `have hne : nonempty α := by apply_instance, cases hne with a,`

is not a replacement of `[hne : nonempty α]`

in the lemma declaration. Sorry for so many questions. I am just trying to understand what is going on.

#### Alexandre Rademaker (Sep 26 2019 at 15:57):

Yes, @Mario Carneiro I got your point. I am just trying to use the example to understand what is going on. But you are right about the example itself. It would not make sense to depend on an additional parameter.

#### Kevin Buzzard (Sep 26 2019 at 16:01):

If alpha is empty (which is fine in Lean) then the goal is false, right? Lean's type class inference system knows that nat is non-empty, but it won't know that alpha is non-empty unless you prove it first.

#### Kevin Buzzard (Sep 26 2019 at 16:02):

`[hne : nonempty α]`

is an assumption; `have hne : nonempty α := ...`

is an unjustified claim.

#### Kevin Buzzard (Sep 26 2019 at 16:03):

PS in case I misunderstood -- it's very hard to debug your code if you just post random error messages. Can you post complete minimal working examples which other people can just cut and paste?

#### Bryan Gin-ge Chen (Sep 26 2019 at 16:04):

In addition to what Kevin said, you can also see this chapter of TPiL for some more info about instances.

#### Alexandre Rademaker (Sep 26 2019 at 16:27):

Sorry @Kevin Buzzard , it edited my previous message. I thought it was clear from the rest of the thread what I am trying to do. Interesting, I thought that `apply_instance, cases hne with a`

is proving/justifying the `hne : nonempty α`

claim, but it would be introducing some circularity...

#### Kevin Buzzard (Sep 26 2019 at 16:30):

I am too lazy to refresh my memory of the thread by reading it all through again, and too forgetful to remember what its main points are :-)

#### Marc Huisinga (Sep 26 2019 at 16:31):

it can't prove that claim, because it isn't true in general

#### Marc Huisinga (Sep 26 2019 at 16:31):

not every α is nonempty

#### Kevin Buzzard (Sep 26 2019 at 16:34):

inductive empty_type . -- no constructors, so no terms. example : ¬ (nonempty empty_type) := begin intro h, cases h with h2, cases h2, end

#### Kevin Buzzard (Sep 26 2019 at 16:35):

The first `cases`

uses the fact that there is only one constructor for `nonempty X`

, which needs a term of type `X`

; this is `h2`

. And then `cases h2`

breaks up into one case per constructor; there are no constructors, so the proof is over.

#### Alexandre Rademaker (Sep 26 2019 at 16:43):

You mean "here is only ONE constructor for `nonempty X`

"? I found in `logic.lean`

:

class inductive nonempty (α : Sort u) : Prop | intro (val : α) : nonempty

Thank you for the example! I am learning a lot here.

#### Kevin Buzzard (Sep 26 2019 at 16:44):

Yes, sorry! I edited. The `cases`

tactic takes a term of type `I`

, with `I`

an inductive type, and then creates one goal per constructor.

#### Alexandre Rademaker (Sep 26 2019 at 16:52):

Thank you @Bryan Gin-ge Chen for the link. Yes, I need to finish to read the TPiL.

#### Alexandre Rademaker (Sep 28 2019 at 23:01):

I must admit, tactics is a complicate stuff! No clue how to prove using tactics the following two theorems:

constant U : Type constants p : U → Prop example (h : ¬ ∃ x : U, p x) : ∀ x : U, ¬ p x := assume y : U, assume h₂ : p y, h (exists.intro y h₂) open classical example (h : ¬ ∀ x : U, p x) : ∃ x : U, ¬ p x := by_contradiction (assume h₁ : ¬ ∃ x, ¬ p x, h (assume b : U, by_contradiction (assume h₂ : ¬ p b, h₁ (exists.intro b h₂))))

It is not clear how to deal with exists.intro and negation in the hypothesis...

#### Johan Commelin (Sep 28 2019 at 23:09):

There's `use`

, `rintro`

, `rcases`

, `push_neg`

, `contrapose!`

#### Johan Commelin (Sep 28 2019 at 23:09):

nice and powerful tactics (-;

#### Kevin Buzzard (Sep 28 2019 at 23:10):

import tactic.interactive -- mathlib, so I can use "use" variable U : Type variable p : U → Prop example (h : ¬ ∃ x : U, p x) : ∀ x : U, ¬ p x := begin intro y, intro h₂, apply h, use y, assumption, end

If you don't like `use`

, you can use `existsi`

in core.

#### Mario Carneiro (Sep 28 2019 at 23:10):

import tactic.interactive constant U : Type constants p : U → Prop example (h : ¬ ∃ x : U, p x) : ∀ x : U, ¬ p x := begin intros y h₂, apply h, existsi y, exact h₂ end example (h : ¬ ∀ x : U, p x) : ∃ x : U, ¬ p x := begin classical, by_contra h₁, apply h, intro b, by_contra h₂, apply h₁, existsi b, exact h₂ end

#### Mario Carneiro (Sep 28 2019 at 23:11):

I probably would not have used tactics for some of these, but this is a pure-tactic style

#### Mario Carneiro (Sep 28 2019 at 23:12):

for example the existsi, exact is easier to write as `refine ⟨b, h₂⟩`

#### Mario Carneiro (Sep 28 2019 at 23:12):

I use the `classical`

tactic (in mathlib) when lean complains about this and that not being decidable

#### Mario Carneiro (Sep 28 2019 at 23:15):

here's a more hybrid approach:

example (h : ¬ ∃ x : U, p x) : ∀ x : U, ¬ p x := λ y h₂, h ⟨y, h₂⟩ example (h : ¬ ∀ x : U, p x) : ∃ x : U, ¬ p x := begin classical, by_contra h₁, refine h (λ b, _), by_contra h₂, exact h₁ ⟨b, h₂⟩ end

#### Alexandre Rademaker (Sep 28 2019 at 23:45):

Thank you @Kevin Buzzard ! @Mario Carneiro , is there any alternative to the classical mathlib tactic? I am trying to avoid introduce mathlib before get things more clear.

#### Mario Carneiro (Sep 28 2019 at 23:46):

`classical`

is the same as `haveI := classical.prop_decidable`

#### Mario Carneiro (Sep 28 2019 at 23:46):

but `haveI`

is another mathlib tactic

#### Kevin Buzzard (Sep 28 2019 at 23:46):

What's `not not P -> P`

called in Lean? For some reason I can't find it with library_search

#### Mario Carneiro (Sep 28 2019 at 23:46):

you can use `local attribute [instance] classical.prop_decidable`

outside the proof instead

#### Mario Carneiro (Sep 28 2019 at 23:47):

`classical.by_contradiction`

#### Alexandre Rademaker (Sep 28 2019 at 23:47):

I like the compact notation of `⟨y, h₂⟩`

but it is confusing since the same par of symbols is used to the `and.intro`

.

#### Mario Carneiro (Sep 28 2019 at 23:48):

it works with any inductive type with one constructor

#### Kevin Buzzard (Sep 28 2019 at 23:48):

That's not confusing -- those are two instances of the same phenomenon. It's unifying :-)

#### Mario Carneiro (Sep 28 2019 at 23:48):

or any `structure`

#### Kevin Buzzard (Sep 28 2019 at 23:50):

example (h : ¬ ∀ x : U, p x) : ∃ x : U, ¬ p x := begin apply classical.by_contradiction, intro h₁, apply h, intro b, apply classical.by_contradiction, intro h₂, apply h₁, existsi b, assumption end

There's a mathlib-free proof of the second one in tactic mode.

#### Kevin Buzzard (Sep 28 2019 at 23:50):

(with thanks to Mario for `classical.by_contradiction`

)

#### Alexandre Rademaker (Sep 28 2019 at 23:51):

Hum, but the signatures returned by the check command are quite different. In the type theory level both are constructors, I see.

#check and.intro #check exists.intro

#### Mario Carneiro (Sep 28 2019 at 23:52):

This isn't notation overloading - the parser has special support for constructing tuple-like inductives

#### Mario Carneiro (Sep 28 2019 at 23:53):

You can also use the `{foo := ... , bar := ...}`

notation, although I've never used it with exists or and before

#### Alexandre Rademaker (Sep 28 2019 at 23:53):

`not not P -> P`

is the `by_contradiction`

, right?

#### Mario Carneiro (Sep 28 2019 at 23:53):

yes

#### Kevin Buzzard (Sep 28 2019 at 23:54):

structure foo := (bar : ℕ) (baz : bool) (erm : ℤ) def x : foo := ⟨7, tt, -5⟩

#### Mario Carneiro (Sep 28 2019 at 23:54):

oh, my mistake, apparently `{}`

structure notation only works with actual `structure`

s, so `exists`

doesn't permit it, although `and`

does

#### Kevin Buzzard (Sep 28 2019 at 23:56):

`exists`

is so horrible for beginners. `#print notation ∃`

gives garbage, and `#check exists`

fails -- Lean wants another term so just looks at the next token and gives a confusing error.

#### Kevin Buzzard (Sep 28 2019 at 23:57):

You're best off just finding the definitions in core (if you can figure out how to get to them)

#### Alexandre Rademaker (Sep 28 2019 at 23:58):

Now I am starting to make sense with negation and exists in tactics!! Tomorrow more exercises!! After months in the 'term-mode', it is taking time to flip my mind to the tactic-mode.

#### Mario Carneiro (Sep 28 2019 at 23:58):

Try `#check Exists`

#### Kevin Buzzard (Sep 28 2019 at 23:59):

Why is `Exists`

an inductive type with one constructor and not a structure?

Wooah, and what does

attribute [intro] Exists.intro

mean?

#### Mario Carneiro (Sep 28 2019 at 23:59):

I know that `[intro]`

(and `[intro!]`

) exist, but I'm not sure what they do

#### Alexandre Rademaker (Sep 29 2019 at 00:02):

@Mario Carneiro what does `local attribute [instance] classical.prop_decidable`

make?

#### Mario Carneiro (Sep 29 2019 at 00:03):

it causes all instances of the form `[decidable p]`

to be solvable

#### Mario Carneiro (Sep 29 2019 at 00:03):

using the law of excluded middle

#### Kevin Buzzard (Sep 29 2019 at 00:03):

It just adds the `instance`

tag to `classical.prop_decidable`

meaning that the type class inference system can see it.

#### Mario Carneiro (Sep 29 2019 at 00:06):

@Kevin Buzzard `[intro]`

is used as part of the `back_chaining`

tactic infrastructure

#### Kevin Buzzard (Sep 29 2019 at 00:07):

This was in core, right? So this is nothing to do with Scott's fancy tactics I guess. What is `back_chaining`

?

#### Mario Carneiro (Sep 29 2019 at 00:09):

That's a good question, I'm looking through tests and things to find out what it's for

#### Kevin Buzzard (Sep 29 2019 at 00:09):

well there you go, core has a file called `backward.lean`

. Not one I'd ever looked at before.

#### Mario Carneiro (Sep 29 2019 at 00:09):

/- Lean has a backward chaining tactic that can be configured using attributes. -/ open list tactic universe variable u lemma in_tail {α : Type u} {a : α} (b : α) {l : list α} : a ∈ l → a ∈ b::l := mem_cons_of_mem _ lemma in_head {α : Type u} (a : α) (l : list α) : a ∈ a::l := mem_cons_self _ _ lemma in_left {α : Type u} {a : α} {l : list α} (r : list α) : a ∈ l → a ∈ l ++ r := mem_append_left _ lemma in_right {α : Type u} {a : α} (l : list α) {r : list α} : a ∈ r → a ∈ l ++ r := mem_append_right _ /- It is trivial to define mk_mem_list using backward chaining -/ attribute [intro] in_tail in_head in_left in_right meta def mk_mem_list : tactic unit := solve1 (back_chaining) example (a b c : nat) : a ∈ [b, c] ++ [b, a, b] := by mk_mem_list set_option trace.tactic.back_chaining true example (a b c : nat) : a ∈ [b, c] ++ [b, a, b] := by mk_mem_list example (a b c : nat) : a ∈ [b, c] ++ [b, c, c] ++ [b, a, b] := by mk_mem_list example (a b c : nat) (l : list nat) : a ∈ l → a ∈ [b, c] ++ b::l := begin intros, mk_mem_list end example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] := begin intros, mk_mem_list end

#### Mario Carneiro (Sep 29 2019 at 00:09):

it looks a lot like `solve_by_elim`

#### Mario Carneiro (Sep 29 2019 at 00:12):

Interestingly it doesn't do definitional unfolding (the `a ∈ [b, c] ++ [b, a, b]`

example fails without the `in_left`

and `in_right`

examples), which is probably a good thing

#### Jesse Michael Han (Sep 29 2019 at 00:14):

it actually works in some cases where one expects `solve_by_elim`

to work, but doesn't

example (p q r s : Prop) (Hp : p) (H₁ : p → q) (H₂ : q → r) (H₃ : r → s) : s := by solve_by_elim -- fails example (p q r s : Prop) (Hp : p) (H₁ : p → q) (H₂ : q → r) (H₃ : r → s) : s := by tactic.back_chaining_using_hs -- works

#### Mario Carneiro (Sep 29 2019 at 00:15):

it has a lot of examples in the tests that look like that - lots of implication chains

Last updated: Dec 20 2023 at 11:08 UTC