Use of "let" in tactic mode

Stream: new members

[Lars Ericson]

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]

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]

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

[Reid Barton]

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]

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

[Lars Ericson]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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

Yes, it's in mathlib

[Lars Ericson]

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]

You need to import it, not open it

[Reid Barton]

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

[Lars Ericson]

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

import tactic.basic