Applying tactic `cases` on a non-variable

Stream: new members

[Gabriel Alfour]

In tactic mode, in my hypothesis, I have something of an application (like f x), and I'd like to do cases on it.
In Coq, when I do so, all instances of f x get pattern-matched over. In Lean4, nothing happens.

I have tried:

1. Doing something like let fx := f x, and then rewriting using rw [fx,\left fx] at hypothesis, but does not work either.
2. Doing something like let fx := fx, then let fx_eq : fx = f x := rfl and then cases fx, but it does not work either. Not even fx gets destructed.

What would be the Lean4 way of performing this step?

Code below if anyone is interested

inductive ast : Type
| Lam : String -> ast -> ast
| Var : String -> ast
| App : ast -> ast -> ast


-- rewriting
inductive rewrite_step_result : Type
| Finish
| Next : ast -> rewrite_step_result

open ast
open rewrite_step_result

def substitute (expr : ast) (var : String) (sub : ast) :=
  match expr with
  | Var var' => if var = var' then sub else Var var'
  | App f arg => App (substitute f var sub) (substitute arg var sub)
  | Lam var' body => if var = var' then Lam var' body else Lam var' (substitute body var sub)

def rewrite_step : ast -> rewrite_step_result
  | Var _var => Finish
  | Lam _var _body => Finish
  | App f arg => (
    match rewrite_step f with
    | Finish => (
      match rewrite_step arg with
      | Finish => (
        match f with
        | Lam var body => Next (substitute body var arg)
        | _ => Finish
      )
      | Next arg' => Next (App f arg')
    )
    | Next f' => Next (App f' arg)
  )

def is_normal (expr : ast) := rewrite_step expr = Finish

open Nat
def rewrite_n_steps (expr : ast) (n : Nat) :=
  match n with
  | zero => Next expr
  | succ n' => (
    match rewrite_step expr with
    | Finish => Finish
    | Next expr' => rewrite_n_steps expr' n'
  )

def terminates (expr : ast) := ∃ n , rewrite_n_steps expr n = Finish

def looper : ast :=
  App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (App (Var "x") (Var "x")))

theorem looper_loops : rewrite_n_steps looper 1 = Next looper :=
  by
  eq_refl

theorem looper_loops_forever : forall n , rewrite_n_steps looper n = Next looper :=
  by
  intro n
  induction n with
  | zero => eq_refl
  | succ _ ih =>
    exact ih

theorem non_terminating : ∃ (expr : ast) , ¬terminates expr :=
  by
  exists looper
  unfold terminates
  intro tl
  let ⟨ n , ih ⟩ := tl
  have ih' : (rewrite_n_steps looper n = Next looper) := looper_loops_forever n
  rw [ih] at ih'
  contradiction

namespace Typed

  inductive type : Type
  | Nat
  | Fun : type -> type -> type
  deriving DecidableEq

  inductive tast : Type
  | TVar : String -> tast
  | TApp : tast -> tast -> tast
  | TLam : String -> type -> tast -> tast

  open tast
  def remove_types : tast -> ast
  | TLam v _ty body => Lam v (remove_types body)
  | TVar v => Var v
  | TApp f arg => App (remove_types f) (remove_types arg)

  namespace Typecheck

    inductive result : Type
    | Fail
    | Succeed : type -> result

    def context : Type := List (String × type)

    open result
    open type
    def main (ctx : context) : tast -> result
    | TVar v => (
      match List.lookup v ctx with
      | none => Fail
      | some ty => Succeed ty
    )
    | TLam v ty body => (
      let ctx := List.cons (v , ty) ctx
      main ctx body
    )
    | TApp f arg => (
      match main ctx arg with
      | Fail => Fail
      | Succeed arg_ty => (
        match main ctx f with
        | Fail => Fail
        | Succeed f' => (
          match f' with
          | Fun in_ty out_ty => (
            if in_ty = arg_ty then Succeed out_ty
            else Fail
          )
          | _ => Fail
        )
      )
    )

  end Typecheck

  open Typecheck

  theorem stlc_terminate :
    ∀ (ctx : context) (tast : tast) (ty : type) ,
      main ctx tast = result.Succeed ty -> ∃ n ,
      rewrite_n_steps (remove_types tast) n = Finish :=
  by
    intros ctx tast ty success
    induction tast
    . exists 1
    . rename_i f arg f_ih arg_ih
      have f_ih_r := f_ih ?_
      . admit
      . unfold main at success
        -- Attempt 1
          -- cases (main ctx arg)
        -- Attempt 2
          -- let marg := main ctx arg
          -- rewrite [marg] at success
        -- Attempt 3
          -- let marg := main ctx arg
          -- have marg_eq : marg = main ctx arg := rfl
          -- rewrite [← marg_eq] at success arg_ih
          -- cases marg
        . sorry
    . sorry



end Typed


-- environment eval
-- inductive eval_step_result : Type

-- def eval_step

[Ruben Van de Velde]

Did I not see someone pointing out cases h : f x to you in another thread?

[Gabriel Alfour]

@Ruben Van de Velde I have tried many permutations that were pointed to me, I might have missed that one, let me check

[Gabriel Alfour]

@Ruben Van de Velde
still the same problem, f x in the hypotheses (main ctx arg in the code) does not get destructed
But I get an equality relation on it!!! Thanks
Is this the expected way to do so in Lean4? Looks a bit verbose (comparable to case_eq in Coq), but if it is, I can make-do with it!

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

abbrev colListofMat := List.map List.ofFn (List.ofFn M.transpose)

def findNonzCol : ℕ := (colListofMat M).findIdx (fun col => ¬ list_allZero col)

def findPivot : Matrix (Fin m) (Fin m) Rat :=
    if h:findNonzCol M = n then 1
    else by
        rcases lt_or_gt_of_ne h

Why is the last line giving this error:
tactic 'cases' failed, nested error: tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop

[Mitchell Lee]

Don't use tactic mode for anything other than proofs. You will get a lot of weird errors like this.

(The fundamental reason for this principle is as follows: when reading a tactic mode block, it is difficult to actually tell what term is being expressed. For proofs, this is fine because any two proofs of the same proposition are equal.)

[Vivek Rajesh Joshi]

Cool, thanks. I'll keep that in mind.

[Mitchell Lee]

Here is a detailed explanation of why this error actually occurs. Imagine that it were possible to use rcases for something other than a proof. Then, you could have something like this:

def f (x : Nat) : Nat := by
  rcases (Nat.le_or_le x 5 : x ≤ 5 ∨ 5 ≤ x)
  · exact 0
  · exact 1

But what would happen if x = 5? Then both conditions x ≤ 5 and 5 ≤ x would hold, so it's not clear whether f 5 should be 0 or 1.

(Note that there is a definition docs#Or.by_cases that you could use to "Construct a non-Prop by cases on an Or". But it only works if the left conjunct is decidable.)

[Kevin Buzzard]

Just to be clear -- Mitchell's example can be extended to a example where you prove False, if you allow cases to work when your goal isn't a true/false statement.