Hypothesis in `match`

Stream: lean4

[Horatiu Cheval]

Consider the snippet below. I want to define the function foo through a dependent if-then-else, and to do pattern matching on one of the branches. But the hypothesis hgiven by if is in some patterns absurd, i.e. I am on the true branch but I know that the function is always false one some pattern, so foo is trivially defined through exfalso there. The problem is that the hypothesis from if remains stated in the local context in terms of the general variable t, instead of by replacing t with its form in the current pattern. Can this be done?

inductive Term
| var : Nat → Term
| app : Term → Term → Term

open Term

def bar : Term → Bool := sorry -- let's say this is some function which returns `false` on `var (i + 1)`

def foo (t : Term) : Term :=
  if h : bar t then match t with
    -- here `t` should be `i + 1`,but how do I get that `bar t = bar (i + 1)`?
    -- I know `h : bar t`, but `bar $ var (i + 1)` is false, si I want to apply False elimination
    | var (i + 1) => _
    /-
    context:
    t : Term
    h : bar t = true
    i : Nat
    ⊢ Term
    -/
    | _ => sorry
  else sorry

[Alexander Bentkamp]

You can also match on h:

def foo (t : Term) : Term :=
  if h : bar t then match t, h with
    | var (i + 1), h' => _
    /-
    t : Term
    h : bar t = true
    i : Nat
    h' : bar (var (i + 1)) = true
    -/
    | _, _ => sorry
  else sorry

[Sebastian Ullrich]

Or, equivalently, match (generalizing := true) t with

[Sebastian Ullrich]

Added to the match docstring.

[Horatiu Cheval]

Great, thank you both!

[Andrés Goens]

I have a similar issue to this where match (generalizing := true) doesn't seem to substitute the variables matched on. This is an #MWE:

import Std
abbrev State := Std.HashMap Nat Nat
inductive IsVal : State → Nat → Option Nat → Prop
  | mk : IsVal s n (s.find? n)

instance (s : State) (n : Nat) (n? : Option Nat) : Decidable (IsVal s n n?) :=
  let v := s.find? n
  match (generalizing := true) v, n? with
    | none, none => isTrue (by
    /- Information lost that v = none:
       Goals (1)
       s : State
       n : Nat
       n? : Option Nat
       v : Option Nat := Std.HashMap.find? s n
       ⊢ IsVal s n none
    -/

Is there any way to keep the information that s.find? n = none in that case?

[Arthur Paulino]

(deleted)

[Arthur Paulino]

As a workaround you can do two consecutive matches and deal with the inner cases separately

[Kyle Miller]

I think you're not really able to do generalization on let bindings. This works for the first case:

instance (s : State) (n : Nat) (n? : Option Nat) : Decidable (IsVal s n n?) :=
  match h : s.find? n, n? with
    | none, none => isTrue <| by
      rw [← h]
      constructor
    | _, _ => sorry

[Kyle Miller]

Here's probably an easier way to go about defining this instance though:

theorem IsVal_iff (s : State) (n : Nat) (n? : Option Nat) :
    IsVal s n n? ↔ n? = s.find? n := by
  constructor
  · intro h
    cases h
    constructor
  · intro h
    subst_vars
    constructor

instance (s : State) (n : Nat) (n? : Option Nat) : Decidable (IsVal s n n?) :=
  if h : n? = s.find? n then
    isTrue <| by rwa [IsVal_iff]
  else
    isFalse <| by rwa [IsVal_iff]

[Andrés Goens]

oh that's interesting, I didn't know you could do match h : ... with like in an if, that's exactly what I was looking for. Thanks! (the example was a simpler version just to show the issue)