tutorial about tactics?

Stream: new members

[Alexandre Rademaker]

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]

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

[Floris van Doorn]

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

[Jesse Michael Han]

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]

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

[Floris van Doorn]

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]

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

[Alexandre Rademaker]

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

[Kevin Buzzard]

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]

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

[Alexandre Rademaker]

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]

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]

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]

Thank you @Kevin Buzzard

[Alexandre Rademaker]

the head symbol of h is the conjunction.

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

yep, that's not the precedence you wrote

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Alexandre Rademaker]

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]

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

[Kevin Buzzard]

split your h with the split tactic so you can see what's going on a bit better.

[Kevin Buzzard]

We have an operator precedence issue.

[Mario Carneiro]

not split, that splits the goal

[Mario Carneiro]

cases h with h1 h2 should do

[Kevin Buzzard]

yeah, cases h

[Kevin Buzzard]

sorry

[Kevin Buzzard]

I'm rubbish at Lean

[Mario Carneiro]

maybe split at h should mean cases h

[Kevin Buzzard]

Your problem is that your h is of this type: (∀ (x : ℕ), (p (f x) → ∀ (x : ℕ), q (f x))) ∧ ∀ (x : ℕ), p x

[Kevin Buzzard]

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

[Alexandre Rademaker]

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]

that looks better

[Kevin Buzzard]

now what's the maths proof?

[Kevin Buzzard]

I'm on steadier ground there.

[Alexandre Rademaker]

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]

You can try working from the end, or haveing an intermediate state

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

Try using the existsi tactic (I think it's deprecated in favor of use now though).

[Kevin Buzzard]

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

[Kevin Buzzard]

It would be interesting to see your proof.

[Alexandre Rademaker]

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]

Hi @Bryan Gin-ge Chen , if I try existsi (f a) it says that a is unknow.

[Chris Hughes]

There's no variable called a in your context. Try existsi (f 0)

[Alexandre Rademaker]

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]

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]

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]

Only if U is nonempty

[Kevin Buzzard]

....

[Alexandre Rademaker]

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]

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]

If you would like a witness to the nonemptiness of the type α to actually be provided, use inhabited instead of nonempty

[Alexandre Rademaker]

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]

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]

To obtain an actual element a of α based on the proof of nonemptiness hne, we appeal to the axiom of choice.

[Marc Huisinga]

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

[Keeley Hoek]

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]

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

[Alexandre Rademaker]

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

[Keeley Hoek]

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

[Keeley Hoek]

It's because nonempty is defined to live in the universe Prop, but inhabited lives in Type (roughly speaking).

[Keeley Hoek]

So inhabited instances can be deconstructed, but nonempty instances cannot be deconstructed once built.

[Keeley Hoek]

Otherwise, they have the same definition exactly.

[Marc Huisinga]

{...} 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]

Thank you @Marc Huisinga for the links.

[Alexandre Rademaker]

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

[Mario Carneiro]

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]

You probably have to do have := hne, cases this with a (or unfreezeI, cases hne with a) for technical reasons.

[Alexandre Rademaker]

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]

you can also use cases id hne with a

[Mario Carneiro]

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]

they are available via import tactic.cache

[Mario Carneiro]

If you don't have mathlib, you can also use tactic.unfreeze_local_instances for which unfreezeI is a synonym

[Alexandre Rademaker]

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]

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]

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]

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]

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]

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]

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]

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]

[hne : nonempty α] is an assumption; have hne : nonempty α := ... is an unjustified claim.

[Kevin Buzzard]

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]

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

[Alexandre Rademaker]

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]

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]

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

[Marc Huisinga]

not every α is nonempty

[Kevin Buzzard]

inductive empty_type . -- no constructors, so no terms.

example : ¬ (nonempty empty_type) :=
begin
  intro h,
  cases h with h2,
  cases h2,
end

[Kevin Buzzard]

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]

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]

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]

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

[Alexandre Rademaker]

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]

There's use, rintro, rcases, push_neg, contrapose!

[Johan Commelin]

nice and powerful tactics (-;

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I use the classical tactic (in mathlib) when lean complains about this and that not being decidable

[Mario Carneiro]

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]

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]

classical is the same as haveI := classical.prop_decidable

[Mario Carneiro]

but haveI is another mathlib tactic

[Kevin Buzzard]

What's not not P -> P called in Lean? For some reason I can't find it with library_search

[Mario Carneiro]

you can use local attribute [instance] classical.prop_decidable outside the proof instead

[Mario Carneiro]

classical.by_contradiction

[Alexandre Rademaker]

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]

it works with any inductive type with one constructor

[Kevin Buzzard]

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

[Mario Carneiro]

or any structure

[Kevin Buzzard]

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]

(with thanks to Mario for classical.by_contradiction)

[Alexandre Rademaker]

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]

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

[Mario Carneiro]

You can also use the {foo := ... , bar := ...} notation, although I've never used it with exists or and before

[Alexandre Rademaker]

not not P -> P is the by_contradiction, right?

[Mario Carneiro]

yes

[Kevin Buzzard]

structure foo :=
(bar : ℕ)
(baz : bool)
(erm : ℤ)

def x : foo := ⟨7, tt, -5⟩

[Mario Carneiro]

oh, my mistake, apparently {} structure notation only works with actual structures, so exists doesn't permit it, although and does

[Kevin Buzzard]

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]

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

[Alexandre Rademaker]

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]

Try #check Exists

[Kevin Buzzard]

Why is Exists an inductive type with one constructor and not a structure?

Wooah, and what does

attribute [intro] Exists.intro

mean?

[Mario Carneiro]

I know that [intro] (and [intro!]) exist, but I'm not sure what they do

[Alexandre Rademaker]

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

[Mario Carneiro]

it causes all instances of the form [decidable p] to be solvable

[Mario Carneiro]

using the law of excluded middle

[Kevin Buzzard]

It just adds the instance tag to classical.prop_decidable meaning that the type class inference system can see it.

[Mario Carneiro]

@Kevin Buzzard [intro] is used as part of the back_chaining tactic infrastructure

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

well there you go, core has a file called backward.lean. Not one I'd ever looked at before.

[Mario Carneiro]

/- 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]

it looks a lot like solve_by_elim

[Mario Carneiro]

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]

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]

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