How to rewrite match case

Stream: new members

[MrQubo]

Screenshot_20250124_124222.png

inductive Lam : ∀ (_ : Nat) (_ : Prop), Type
| bvar : ∀ {n}, (m : Nat) → (_ : m < n := by omega) → (p : Prop := True) → Lam n p
| fvar : ∀ {n}, String → Lam n False
| app : ∀ {n p q r}, Lam n p → Lam n q → (_ : r → p ∧ q := by simp_all) → Lam n r
| lam : ∀ {n p r}, Lam n.succ p → (_ : r → p := by simp_all) → Lam n r
deriving Repr
open Lam

def forgetClosed {n p} (t : Lam n p) : Lam n False :=
  match ht : t with
  | bvar m h p => bvar m h False
  | fvar name => by
    <here>
  | app f arg _ => app f arg
  | lam body _ => lam body

How can I rewrite t to Lam n False? I.e., how can I name anonymous hypothesis p = False, or how can I use this anonymous hypothesis in rewrite.

[Ruben Van de Velde]

Maybe rename_i hp

[Aaron Liu]

What are you trying to accomplish? The goal state at <here> is

n : Nat
p : Prop
t : Lam n p
name : String
h✝ : p = False
ht : HEq t (fvar name)
⊢ Lam n False

What do you want to try to turn this into?

[MrQubo]

I want to do rw [h✝] at t; exact t basically.

[Aaron Liu]

This works:

  | fvar name => ‹p = False› ▸ t

[MrQubo]

Ruben Van de Velde said:

Maybe rename_i hp

I've read that the names of inaccessible names aren't guaranteed to be preserved across lean version. Is order of inaccessible names guaranteed though?

[Edward van de Meent]

i think it's decently consistent?

[MrQubo]

Aaron Liu said:

This works:

  | fvar name => ‹p = False› ▸ t

Thanks! I think I understand what \f<> does, but how can I find what \t does?

[Edward van de Meent]

perhaps easier:

def forgetClosed {n p} : Lam n p → Lam n False
  | bvar m h p => bvar m h False
  | fvar name => fvar name
  | app f arg _ => app f arg
  | lam body _ => lam body

[MrQubo]

Edward van de Meent said:

perhaps easier:

def forgetClosed {n p} : Lam n p → Lam n False
  | bvar m h p => bvar m h False
  | fvar name => fvar name
  | app f arg _ => app f arg
  | lam body _ => lam body

Oh, wait, it does work. I thought I've tried it and it didn't.

[Edward van de Meent]

also a possibility:

def forgetClosed {n p} (t : Lam n p) : Lam n False :=
  match t with
  | bvar m h p => bvar m h False
  | t'@(fvar name) => t'
  | app f arg _ => app f arg
  | lam body _ => lam body

[MrQubo]

MrQubo said:

Aaron Liu said:

This works:

  | fvar name => ‹p = False› ▸ t

Thanks! I think I understand what \f<> does, but how can I find what \t does?

Hm, okay, found it. In neovim I had to put (‹p = False› ▸ t) in parentheses, and then run vim.lsp.buf.hover() with my cursor on ▸.