## Stream: new members

### Topic: Use of "let" in tactic mode

#### Lars Ericson (Nov 26 2020 at 21:03):

The text gives this example of using let:

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩


I am trying to adapt this to tactic mode. This works:

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
exact (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
end


However, this does not work:

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
exact h2,
end


I get this error:

invalid match/convoy expression, expected type is not known
state:
α : Type u_1,
p q : α → Prop,
h : ∃ (x : α), p x ∧ q x
⊢ ∃ (x : α), q x ∧ p x


My prior experience has been that this:

example foo :=
begin
have h := bar,
exact h,
end


is equivalent to this:

example foo :=
begin
exact bar,
end


Why does the equivalence not hold in the above case?

#### Logan Murphy (Nov 26 2020 at 21:06):

Looking at your tactic state, i think you just need to switch

 have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),


to

 have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hpw, hqw⟩),


#### Logan Murphy (Nov 26 2020 at 21:07):

i.e. right now p and q don't match up exactly with the goal, they are swapped

#### Reid Barton (Nov 26 2020 at 21:08):

The error message sort of tells you the reason. If your goal is foo and you write exact bar, then Lean knows that bar is supposed to have type foo and it can use this to make sense of bar. If you write have h := bar, then Lean doesn't know what you are intending to do with h and it has to make sense of bar in isolation, and usually this is harder.

#### Reid Barton (Nov 26 2020 at 21:08):

If you write have h : foo := bar then Lean has the same information again.

#### Lars Ericson (Nov 26 2020 at 21:12):

Thank you @Reid Barton :

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
have h2 : ∃ x, q x ∧ p x := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
exact h2,
end


#### Reid Barton (Nov 26 2020 at 21:18):

This is a very unnatural way to write the proof of course

#### Reid Barton (Nov 26 2020 at 21:18):

The (mathlib) tactic equivalent to let with a pattern is obtain

#### Reid Barton (Nov 26 2020 at 21:20):

import tactic.basic

example (a : Type) (p q : a -> Prop) (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
obtain ⟨w, hpw, hqw⟩ := h,
exact ⟨w, hqw, hpw⟩,
end


#### Lars Ericson (Nov 26 2020 at 21:38):

@Reid Barton if I try to use obtain ⟨w, hpw, hqw⟩ := h to unpack h : ∃ (x : α), p x ∧ r where the current goal state is:

27:6: goal
α : Type u_1,
p : α → Prop,
r : Prop,
h : ∃ (x : α), p x ∧ r
⊢ r


in this example:

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end


a lot of errors result:

Display GoalDisplay Messages
27:4: error:
unknown identifier 'obtain'
27:12: error:
unknown identifier 'w'
27:15: error:
unknown identifier 'hpw'
27:20: error:
unknown identifier 'hqw'
27:25: error:
invalid 'begin-end' expression, ',' expected
27:4: error:
don't know how to synthesize placeholder
context:
α : Type u_1,
p : α → Prop,
r : Prop
⊢ Type ?


#### Reid Barton (Nov 26 2020 at 21:39):

Yes, it's in mathlib

#### Lars Ericson (Nov 26 2020 at 21:42):

I see tactic.interactive.obtain but I get the same error even if I open it:

open tactic.interactive

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end


If I try to use the full name of obtain:

open tactic.interactive

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
tactic.interactive.obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end


then I get this:

Display GoalDisplay Messages
29:31: error:
unknown identifier 'w'
29:34: error:
unknown identifier 'hpw'
29:39: error:
unknown identifier 'hqw'
29:44: error:
invalid 'begin-end' expression, ',' expected
29:4: error:
unknown identifier 'tactic.interactive'
29:22: error:
invalid field notation, type is not of the form (C ...) where C is a constant
⁇
has type
?m_1
29:4: error:
don't know how to synthesize placeholder
context:
α : Type u_1,
p : α → Prop,
r : Prop
⊢ Type ?


#### Reid Barton (Nov 26 2020 at 21:43):

You need to import it, not open it

#### Reid Barton (Nov 26 2020 at 21:43):

Er, import some module which exports it (basically all of mathlib)

#### Lars Ericson (Nov 26 2020 at 23:17):

@Reid Barton , switching import for open didn't obtain obtain. It's OK, I did it without it. It turns out I can instantiate an existential with cases:

open classical

variables (α : Type*) (p q : α → Prop)
variable r : Prop

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor,
exact px,
},
{
cases h with x pxr,
exact pxr.right,
}
},
{
intro h,
cases h with h1 h2,
cases h1 with x px,
have hpxr := and.intro px h2,
constructor,
exact hpxr,
},
end


#### Reid Barton (Nov 27 2020 at 00:01):

import tactic.basic

Last updated: May 10 2021 at 00:31 UTC