## Stream: general

### Topic: match hypothesis

#### Alexander Bentkamp (Sep 12 2018 at 12:46):

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 (Sep 12 2018 at 13:25):

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 (Sep 13 2018 at 08:28):

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 (Sep 13 2018 at 08:40):

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

#### Kevin Buzzard (Sep 13 2018 at 08:41):

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

#### Kevin Buzzard (Sep 13 2018 at 08:46):

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 (Sep 13 2018 at 08:47):

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

#### Rob Lewis (Sep 13 2018 at 08:51):

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 (Sep 13 2018 at 08:52):

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

#### Kenny Lau (Sep 13 2018 at 09:15):

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


right

#### Kevin Buzzard (Sep 13 2018 at 09:15):

so you are defining an auxiliary f' using pattern matching

#### Kevin Buzzard (Sep 13 2018 at 09:15):

and then you can define f using f'

#### Kenny Lau (Sep 13 2018 at 09:16):

wait, I think I have another answer

#### Kevin Buzzard (Sep 13 2018 at 09:16):

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 (Sep 13 2018 at 09:16):

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

#### Kenny Lau (Sep 13 2018 at 09:17):

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


#### Kenny Lau (Sep 13 2018 at 09:17):

this is the answer you seek

#### Kenny Lau (Sep 13 2018 at 09:18):

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


#### Kevin Buzzard (Sep 13 2018 at 09:18):

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

#### Patrick Massot (Sep 13 2018 at 09:31):

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 (Sep 13 2018 at 09:31):

So, what are you trying to do?

#### Kenny Lau (Sep 13 2018 at 09:32):

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

#### Alexander Bentkamp (Sep 13 2018 at 09:44):

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 (Sep 13 2018 at 09:44):

Minimum working example

#### Alexander Bentkamp (Sep 13 2018 at 09:45):

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

#### Kevin Buzzard (Sep 13 2018 at 09:54):

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 (Sep 13 2018 at 09:55):

@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 (Sep 13 2018 at 09:56):

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

#### Alexander Bentkamp (Sep 13 2018 at 10:01):

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 (Sep 13 2018 at 10:10):

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 (Sep 13 2018 at 10:41):

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 (Sep 13 2018 at 10:42):

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

#### Kevin Buzzard (Sep 13 2018 at 10:42):

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

#### Rob Lewis (Sep 13 2018 at 10:45):

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 (Sep 13 2018 at 11:22):

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 (Sep 13 2018 at 22:44):

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

interesting!

#### Mario Carneiro (Sep 13 2018 at 23:15):

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


wow

this is amazing

#### Kenny Lau (Sep 13 2018 at 23:19):

I learn something new every day

#### Alexander Bentkamp (Sep 14 2018 at 09:33):

cool! I went for Johannes's solution now.

Last updated: May 08 2021 at 10:12 UTC