Zulip Chat Archive

Stream: general

Topic: match hypothesis


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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 08:47):

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

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

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

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:15):

@Kevin Buzzard is this the answer to your question?

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 09:15):

right

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 09:15):

so you are defining an auxiliary f' using pattern matching

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 09:15):

and then you can define f using f'

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:16):

wait, I think I have another answer

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 09:16):

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

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:17):

this is the answer you seek

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:18):

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 09:18):

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

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 09:31):

So, what are you trying to do?

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:32):

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

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

view this post on Zulip Keeley Hoek (Sep 13 2018 at 09:44):

Minimum working example

view this post on Zulip Alexander Bentkamp (Sep 13 2018 at 09:45):

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 10:42):

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

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

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

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 23:09):

interesting!

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 23:19):

wow

view this post on Zulip Kenny Lau (Sep 13 2018 at 23:19):

this is amazing

view this post on Zulip Kenny Lau (Sep 13 2018 at 23:19):

I learn something new every day

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