## 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):

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

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 haveing 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

....

#### 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.

#### 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?

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 structures, 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: May 08 2021 at 03:17 UTC