Zulip Chat Archive

Stream: new members

Topic: Use of "let" in tactic mode


view this post on Zulip 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?

view this post on Zulip 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⟩),

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 26 2020 at 21:08):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 26 2020 at 21:18):

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

view this post on Zulip Reid Barton (Nov 26 2020 at 21:18):

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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Reid Barton (Nov 26 2020 at 21:39):

Yes, it's in mathlib

view this post on Zulip 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 ?

view this post on Zulip Reid Barton (Nov 26 2020 at 21:43):

You need to import it, not open it

view this post on Zulip Reid Barton (Nov 26 2020 at 21:43):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 27 2020 at 00:01):

import tactic.basic


Last updated: May 10 2021 at 00:31 UTC