Using knowledge from pattern matching

Stream: new members

[Josh Clune]

Hello, sorry if a variant of this question has already been asked. I’m currently trying to use information that should be available from prior pattern matching in a proof. In particular, if I have one variable serve as part of the pattern for another, I want to be able to recover that fact.

So for example, in the code below, I need a proof that y < x in order for the recursion to be valid. I can easily show that y is less than nat.succ y (i.e. x in the second branch), but I don’t actually know how to use this fact to prove that y < x.

def recusion_test : ℕ → ℕ
  | x :=
    match x with
    | 0 := 0
    | (nat.succ y) :=
        have y < nat.succ y, from lt_add_one y,
        have y < x, from sorry,
        recusion_test y
    end

What should I replace sorry with to make this work?

[Horatiu Cheval]

Not answering your question (I don't know how to do it, or if it can be done), but maybe you could provide an example of where you need this? Perhaps there's a workaround there too.

[Eric Wieser]

I think the trick is usually match _, rfl : ∀ x', x' = x with ...

[Mario Carneiro]

or cases e : x

[Josh Clune]

Eric Wieser said:

I think the trick is usually match _, rfl : ∀ x', x' = x with ...

Sorry, I don't think I quite understand what you're getting at here. I'm not familiar with some of the syntax you're using or how it's supposed to work. Would you (or someone that knows what Eric is referring to) be willing to give an example of how I'm supposed to use this in context?

[Josh Clune]

Mario Carneiro said:

or cases e : x

Unless if I'm misunderstanding, or am unfamiliar with some other way of using cases, I thought cases was usable as a tactic. But as I'm trying to define a program here, it's unclear to me how it would be possible to use this tactic in place of the match construct. I tried to use nat.cases_on x in place of match x with ..., but that ran into the same issue of lean being unable to recognize the relationship between y and x. Is there some way to use cases in this context to achieve the effect I'm aiming for?

[Josh Clune]

Horatiu Cheval said:

Not answering your question (I don't know how to do it, or if it can be done), but maybe you could provide an example of where you need this? Perhaps there's a workaround there too.

In the context of the specific function I'm working on at present, I'm trying to define a recursive function that takes a fin n and cases on the val of that fin n (e.g. if x : fin n, then I'm trying to write a recursive function that starts with match subtype.val x with...). Since I can't case directly on the fin n, that's why I think the workaround for the example I posted doesn't work. But I'm also interested on how to do this more generally for the future (assuming there is one).