eliminating complex existensial

Stream: general

[Bernd Losert]

Why doesn't match ... with work here?

constants p q r : Prop
constant h : exists (a b c : α), p ∧ q ∧ r

def foo : exists a b c, p ∧ q ∧ r :=
  match h with ⟨a, b, c, prfp, prfq, prfr⟩ :=
    ⟨a, b, c, prfp, prfq, prfr⟩
  end

[Eric Wieser]

What's the error?

[Bernd Losert]

Ah, I forgot to write exists (a b c : α) in foo.

[Bernd Losert]

That was a toy example. In the real code, I'm getting:

invalid constructor ⟨...⟩, 'or' must have only one constructor

[Bernd Losert]

Oops. Actually, it's this error:

error: invalid constructor ⟨...⟩, expected type is not an inductive type
  ?m_1

[Huỳnh Trần Khanh]

oh oops... is the problem resolved now or do you still need our help?

[Bernd Losert]

Yes, I still need some help. What does that last error mean?

[Huỳnh Trần Khanh]

ah that error simply means lean can't infer the type

[Bernd Losert]

By the way, this is the code that produces the error:

      (assume h, match h with ⟨x, l, hm, hf, hc⟩ :=
        or.inr ⟨x, l, hm, hf, hc⟩
      end)

Now, it should an error since hm is not entirely correct, but it seems that the error I'm getting is more fundamental.

[Eric Wieser]

Can you make a #mwe? That last post is useless without knowing what the type of your goal state is

[Eric Wieser]

Which is to say, the humans on Zulip are also unable to infer the type

[Bernd Losert]

The mwe I came up with worked. Let me play around some more. The goal was to produce this:

l₁ ≤ pure y ∨ ∃ (x : α) (l : filter α), l₁ ≤ map f l ∧ y = f x ∧ conv l x

[Eric Wieser]

Are you aware of tactic#extract_goal, which can be used as a starting point to create a mwe?

[Huỳnh Trần Khanh]

oh ouch this poor human being can't help you... can you just make a complete lean file with imports and stuff to demonstrate the problem and post it here OR you can just paste the file you're working on if it's short enough

[Bernd Losert]

Eric Wieser said:

Are you aware of tactic#extract_goal, which can be used as a starting point to create a mwe?

Interesting. Didn't know about that.

[Bernd Losert]

Here's the full file:

import order.filter.ultrafilter
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

universes u v w
variables {α β : Type*}

class convergence_space (α : Type u) :=
(conv : filter α → α → Prop)
(pure_conv : ∀ {x : α}, conv (pure x) x)
(le_conv : ∀ {x : α} {l l' : filter α}, l ≤ l' → conv l' x → conv l x) -- l ≤ l' means l' ⊆ l
(sup_conv : ∀ {x : α} {l l' : filter α}, conv l x → conv l' x → conv (l ⊔ l') x) -- l ⊔ l' means l ∩ l'

open convergence_space

def lim [convergence_space α] (l : filter α) : set α := set_of (conv l)

structure continuous [convergence_space α] [convergence_space β] (f : α → β) : Prop :=
(filter_conv : ∀ {x : α} {l : filter α}, conv l x → conv (map f l) (f x))

class hausdorff_space [convergence_space α] : Prop :=
(hausdorff_prop : ∀ (l : filter α) [ne_bot l], subsingleton (lim l))

def induced (f : α → β) (t : convergence_space β) : convergence_space α := {
  conv := λ l x, conv (map f l) (f x),
  pure_conv := begin
    intro,
    simp [filter.map_pure],
    apply pure_conv
  end,
  le_conv := begin
    intros x l l' h₀ h₁,
    have h₂ : map f l ≤ map f l',
      apply map_mono h₀,
    apply le_conv h₂ h₁
  end,
  sup_conv := begin
    intros x l l' h₀ h₁,
    simp [map_sup],
    apply sup_conv h₀ h₁,
  end
}

def coinduced (f : α → β) (t : convergence_space α) : convergence_space β := {
  conv := λ l' y, l' ≤ pure y ∨ (∃ x l, l' ≤ map f l ∧ y = f x ∧ conv l x),
  pure_conv := begin
    intro,
    simp [and.left]
  end,
  le_conv := begin
    intros y l₁ l₂ h₀ h₁,
    apply or.elim h₁
      (assume h, or.inl (trans h₀ h))
      (assume h, match h with ⟨x, l, hm, hf, hc⟩ :=
        or.inr ⟨x, l, trans h₀ hm, hf, hc⟩ -- THIS IS WHERE IT FAILS
      end)
  end,
  sup_conv := sorry
}

[Eric Wieser]

Replace apply with exact

[Bernd Losert]

Haha. It works. Nice.

[Bernd Losert]

So what's the difference between exact, apply and refine? I was using refine before, then switched to apply. And now I am switching to exact.

[Eric Wieser]

exact tells the elaborator "parse this expression with the knowledge that it must match the goal". apply doesn't know whether the expression is intended to exactly or partially match the goal, which can confuse the elaborator.

[Eric Wieser]

refine is like exact but won't error if there are _s it can't fill. You should use exact instead of refine if it's the last line of your (sub)proof

[Eric Wieser]

apply foo x is like refine foo x _ _ which tries to guess how many _s are needed. It's this guessing that can misfire and causes your problem

[Bernd Losert]

OK, so I will stick with exact as much as I can then.

[Bernd Losert]

Thanks guys.

[Reid Barton]

More specifically, exact foo knows the expected type of foo (namely the goal) and can use this to elaborate foo, while apply foo doesn't know the expected type of foo because it will be foo _ ... _ that matches the goal; so apply needs to first elaborate foo without expected type information to work out the correct number of _s, and here it has no way to know what the anonymous constructor ⟨x, l, trans h₀ hm, hf, hc⟩ refers to.

[Reid Barton]

We rarely use match or apply eliminators directly in tactics, a more tactic-style proof would be

  le_conv := begin
    intros y l₁ l₂ h₀ h₁,
    rcases h₁ with h | ⟨x, l, hm, hf, hc⟩,
    { exact or.inl (trans h₀ h) },
    { exact or.inr ⟨x, l, trans h₀ hm, hf, hc⟩ }
  end,

or variants using tactic#rintro or tactic#obtain

[Eric Wieser]

Reid Barton said:

so apply needs to first elaborate foo without expected type information to work out the correct number of _s

Is there a reason apply doesn't just try elaborating foo, foo _, foo _ _, ... until it finds one that matches, as opposed to elaborating foo with incomplete information?