match pattern not rfl-ing

Stream: lean4

[Dmitry Ivankov]

Hi, very new to lean and got stuck proving pattern match relation to scrutinee.

def f (x : Bool)
  | y =>
    have eq : x = y := by rfl
    True

doesn't work

tactic 'rfl' failed, equality lhs
  x
is not definitionally equal to rhs
  y
x x✝ : Bool
y : Bool := x✝
⊢ x = y

in the end I want to prove

def g (x : List α)
  | [] => True
  | y@(a :: bs) =>
    have eq : x = y := by rfl -- this currently fails
    have lt : bs.length < x.length := by simp[eq]
    True

[Dmitry Ivankov]

Extra debugging

def g (x : List α) := match x with
  | [] => True
  | y@(a :: bs) =>
    have : y = (a::bs) := by simp_all -- this one is ok
    have : x = y := by simp_all -- this one fails
--    have : x = (a::bs) := by rfl
--    have : bs.length.succ = (a::bs).length := by apply List.length_cons
--    have lt : bs.length < x.length := by simp
    True

fails with

unsolved goals
α : Type ?u.55
x y : List α
a : α
bs : List α
this : y = a :: bs
⊢ x = a :: bs

other commented-out have-s also fail

this works

def g (x : List α) := match x with
  | y =>
    have : x = y := by rfl
    True

and this fails

def g (x : List α) := match x with
  | [] => True
  | y =>
    have : x = y := by rfl
    True

[Adam Topaz]

Can you explain what you're trying to accomplish here?

[Reid Barton]

In particular, it's confusing that there is no type declared for any of your functions

[Adam Topaz]

The issue in the original code is that lean has no way of telling what you're trying to define

[Dmitry Ivankov]

overall context is trying to prove termination for code like following

def prob (l : List Nat) := go 0 l where
  gozeroes (acc : Nat) (l : List Nat) := match l with
   | [] => acc
   | l@(x :: rst) =>
     match x with
      | 0 => gozeroes acc.succ rst
      | _ => go acc l
  go (acc : Nat) (l : List Nat) := match l with
   | [] => acc
   | q@(x::rst) =>
    match x with
      | 0 =>  -- skip one zero and process zeroes
        have : q = 0 :: rst := by simp_all
        --all below fails
        --have : q = x :: rst := by rfl
        --have : q = l := by rfl
        --have : l = (0 :: rst) := by simp_all
        --have : l = (x :: rst) := by simp_all
        --have : rst.length < l.length := by ...
        gozeroes acc rst
      | _ => go acc rst
  termination_by go _ l => l.length
                 gozeroes _ l => l.length + 1 -- gozeroes recursed into go without reduction

was confused by not being able to give hints to termination checker
but actually termination_by can be tweaked to work without extra hints and following resolves my overall goal

def prob (l : List Nat) := go 0 l where
  gozeroes (acc : Nat) (l : List Nat) := match l with
   | [] => acc
   | l@(x :: rst) => -- removing shadowing of l with l@ makes termination checker fail
     match x with
      | 0 => gozeroes acc.succ rst
      | _ => go acc l
  go (acc : Nat) (l : List Nat) := match l with
   | [] => acc
   | q@(x::rst) =>
    match x with
      | 0 =>  -- skip one zero and process zeroes
        gozeroes acc rst
      | _ => go acc rst
  termination_by go _ l => 2 * l.length
                 gozeroes _ l => 2 * l.length + 1

but I'm still unsure why have-s can't establish scrutinee <-> matched relations

[Dmitry Ivankov]

Cleaned up version

-- count number of zeroes except for the first zeros in each consecutive run of zeroes
def prob (l : List Nat) : Nat := go 0 l where
  gozeroes (acc : Nat) (l : List Nat) : Nat := match l with
   | [] => acc
   | x :: rst =>
     match x with
      | 0 => gozeroes acc.succ rst
      | _ =>
        have : l = x :: rst := sorry -- equality holds but how to prove it?
        go acc l
  go (acc : Nat) (l : List Nat) : Nat := match l with
   | [] => acc
   | x::rst =>
    match x with
      | 0 =>  -- skip one zero and process zeroes
        gozeroes acc rst
      | _ => go acc rst
  termination_by go _ l => 2 * l.length
                 gozeroes _ l => 2 * l.length + 1

termination checker is happy but I don't see a way to fix "sorry", and without that line termination checker isn't happy. Workaround is to alias (x::rst) as l in gozeroes (also can remove l argument and "match l" wrapping), then termination checker is happy again