match hypothesis

Stream: general

[Alexander Bentkamp]

Hi,

I hope you can help me with the following issue:

I have this defintion containing a proof obligation:

  def clip_tensor_index2 : Π {ds₁ : list ℕ} (ds₂ : list ℕ), tensor_index (zipdims ds₂ ds₁) → option (tensor_index ds₂)
  | ds₁ ds₂ ⟨is, h⟩ := match clip_tensor_index_list ds₂ is with
  | none := none
  | some js := some ⟨ js , clip_tensor_index_list_correct ds₂ is js sorry⟩
  end

Where I put sorry, I need to prove that clip_tensor_index_list ds₂ is = some js, which should be obvious since I matched clip_tensor_index_list ds₂ is with some js. How can I do this?

@Rob Lewis helped me out with this solution using tactics:

  def clip_tensor_index2 : Π {ds₁ : list ℕ} (ds₂ : list ℕ), tensor_index (zipdims ds₂ ds₁) → option (tensor_index ds₂)
  | ds₁ ds₂ ⟨is, h⟩ :=
  begin
    cases h1 : clip_tensor_index_list ds₂ is with js,
    exact none,
    exact some ⟨ js , clip_tensor_index_list_correct ds₂ is js h1 ⟩
  end

This works, but I am curious if I could avoid using tactics inside a definition.

[Kevin Buzzard]

If the thing you're matching on (clip_tensor_index_list ds₂ is) is an inductive type T then you could use T.rec (it looks like option.rec in your case)

[Alexander Bentkamp]

Yes, clip_tensor_index_list ds₂ is is of type option. However, with option.rec, I still have the same issue. Where you see the sorry below, I need to provide a proof of clip_tensor_index_list ds₂ is = some js. How can I get it?

  def clip_tensor_index2 : Π {ds₁ : list ℕ} (ds₂ : list ℕ), tensor_index (zipdims ds₂ ds₁) → option (tensor_index ds₂)
  | ds₁ ds₂ ⟨is, h⟩ :=
  option.rec none (λjs, some ⟨ js , clip_tensor_index_list_correct ds₂ is js sorry ⟩) (clip_tensor_index_list ds₂ is)

[Kevin Buzzard]

I see: I was too quick. This has come up before and I can't remember the answer :-(

[Kevin Buzzard]

Of course you could look at the proof term generated by the tactic version and see how Lean did it ;-)

[Kevin Buzzard]

MWE:

definition f (b : bool) : {x : bool // x = tt} :=
begin
  cases h : b with x y,
  { -- h : b = ff
    exact ⟨tt,rfl⟩,
  },
  { -- h : b = tt and I will now use h
    exact ⟨b,h⟩
  }
end

[Kevin Buzzard]

and #print f tells me that Lean used bool.cases_on

[Rob Lewis]

Like I told you yesterday, I'm sure there's a way to make match handle this, but I can't remember. Here's a workaround in term mode, by giving a motive to the recursor explicitly. I suspect that the tactic version is doing basically this under the hood.

definition f (b : bool) : {x : bool // x = tt} :=
@bool.rec_on (λ b', b = b' → {x : bool // x = tt}) b (λ _, ⟨tt, rfl⟩) (λ h, ⟨b, h⟩) rfl

[Kevin Buzzard]

right, that's what the term looks like in my bool example. The trick is a cleverly-chosen motive.

[Kenny Lau]

definition f' : Π b₁ b₂ : bool, b₁ = b₂ → {x : bool // x = tt}
| b tt H := ⟨b, H⟩
| b ff H := ⟨tt, rfl⟩

[Kenny Lau]

@Kevin Buzzard is this the answer to your question?

[Kevin Buzzard]

right

[Kevin Buzzard]

so you are defining an auxiliary f' using pattern matching

[Kevin Buzzard]

and then you can define f using f'

[Kenny Lau]

wait, I think I have another answer

[Kevin Buzzard]

I had a look at that tail / vector example in TPIL and they also used an auxiliary function, but then they did something cleverer and got the equation compiler to do it

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#dependent-pattern-matching

[Kenny Lau]

definition f' : nat → nat
| 0 := _
| k@(n+1) := let K := k in _
/-
f' : ℕ → ℕ,
n : ℕ,
K : ℕ := n + 1
⊢ ℕ
-/

[Kenny Lau]

this is the answer you seek

[Kenny Lau]

definition f' : bool → {x : bool // x = tt}
| b@tt := ⟨b, rfl⟩
| ff := ⟨tt, rfl⟩

[Kevin Buzzard]

excellent, thanks Kenny. @Alexander Bentkamp hopefully this is enough hints :-)

[Patrick Massot]

I have no idea what you are talking about, and yet it seems interesting. What the point of that definition of f'? Clearly example : f' = (λ x, ⟨tt, rfl⟩) := by ext x ; cases x; refl

[Patrick Massot]

So, what are you trying to do?

[Kenny Lau]

honestly, nobody knows what we're trying to do unless OP provides an MWE

[Alexander Bentkamp]

Hi, thanks for all the answers. I am trying to apply what you wrote to my situation, but I am still having trouble.

What's an MWE?

[Keeley Hoek]

Minimum working example

[Alexander Bentkamp]

Oh, ok. I'll try to come up with something.

[Kevin Buzzard]

Patrick my definition is too minimal. The OP just wants to define a function on option A by matching, and when defining its value at x := some y he needs the proof that x = some y to define the value.

[Kevin Buzzard]

@Alexander Bentkamp the reason your original post didn't get much attention is because we can't just cut and paste your code into a blank lean session, so someone had to figure out what you were actually asking.

[Alexander Bentkamp]

Oh, I feel like my post is getting a lot of attention :)
I almost finished the MWE...

[Alexander Bentkamp]

Here it is:

    def clip : list ℕ → option (list ℕ) := sorry

    def p : list ℕ → list ℕ → bool := sorry

    lemma clip_correct (is js : list ℕ) (h : clip is = some js) : p is js := sorry

    def lookup (is : list ℕ) : option { js : list ℕ // p is js} :=
    match (clip is) with
    | none := none
    | some js := some ⟨ js, clip_correct is js _ ⟩
    end

The last underscore would need a proof that clip is = some js.

[Alexander Bentkamp]

If I follow @Kevin Buzzard 's advise, i.e. I use tactic mode to generate a working definition and use #print to view it, then I get this:

def lookup : Π (is : list ℕ), option {js // ↥(p is js)} :=
λ (is : list ℕ),
  (λ (_x : option (list ℕ)) (h1 : clip is = _x),
     option.cases_on _x (λ (h1 : clip is = none), none) (λ (js : list ℕ) (h1 : clip is = some js), some ⟨js, _⟩)
       h1)
    (clip is)
    _

But if I copy paste this into the editor, I get

invalid 'option.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known

What type needs to be known?

[Kenny Lau]

def clip : list ℕ → option (list ℕ) := sorry

def p : list ℕ → list ℕ → bool := sorry

lemma clip_correct (is js : list ℕ) (h : clip is = some js) : p is js := sorry

def lookup_aux : Π (is : list ℕ) (cis : option (list ℕ)), clip is = cis → option { js : list ℕ // p is js}
| is none H := none
| is (some js) H := some ⟨js, clip_correct _ _ H⟩

def lookup (is : list ℕ) : option { js : list ℕ // p is js} :=
lookup_aux _ _ rfl

[Kevin Buzzard]

my guess is that it's the type of of the lambda which you're evaluating at clip is

[Kevin Buzzard]

So Kenny's solution is via the auxiliary function trick which is mentioned in TPIL

[Rob Lewis]

The elaborator isn't able to infer the motive for cases_on. If you don't want to use an aux declaration, you can give the motive manually, but personally I think the tactic version is cleaner than all of these.

def lookup' (is : list ℕ) : option { js : list ℕ // p is js} :=
@option.cases_on _ (λ i, clip is = i → option { js : list ℕ // p is js}) (clip is)
  (λ _, none)
  (λ js h, some ⟨js, clip_correct is js h⟩)
  rfl

def lookup'' (is : list ℕ) : option { js : list ℕ // p is js} :=
have ∀ {i}, clip is = i → option { js : list ℕ // p is js}, from λ i,
match i with
| none := λ _, none
| some js := λ h, some ⟨ js, clip_correct is js h ⟩
end,
this rfl

[Alexander Bentkamp]

Ok, I guess you are right. I'll stick to the tactic version. Anyway, good to know how the other options look like. Thanks!

[Johannes Hölzl]

@Alexander Bentkamp for this concrete example you can use the following solution:

def lookup (is : list ℕ) : option { js : list ℕ // p is js} :=
match clip is, clip_correct is with
| none, h := none
| some js, h := some ⟨ js, h _ rfl ⟩
end

The trick is to put the clip_correct into the parameters to match, with enough instantiations that clip is is found in it. But Rob is right, for more complicated things tactics will be easier.

[Kenny Lau]

interesting!

[Mario Carneiro]

By the way, Rob's last match example can also be written using the (rarely used) "return" argument of match (i.e. match stuff : type with syntax):

def lookup (is : list ℕ) : option { js : list ℕ // p is js} :=
match _, rfl : ∀ i, clip is = i → option { js : list ℕ // p is js} with
| none,    _ := none
| some js, h := some ⟨ js, clip_correct is js h ⟩
end

[Kenny Lau]

wow

[Kenny Lau]

this is amazing

[Kenny Lau]

I learn something new every day

[Alexander Bentkamp]

cool! I went for Johannes's solution now.