Zulip Chat Archive

Stream: general

Topic: Combining induction with cases in Lean

Kristina Sojakova (Mar 13 2025 at 11:47):

Dear all,

I am a new user to Lean and want to prove a lemma of the following form:

lemma Stmt.repeatUntil_correct_left_to_right {S B s t} :
(repeatUntil S B, s) ⟹ t →
(S; whileDo (fun s => ¬ (B s)) S, s) ⟹ t :=

showing that the repeatUntil construct can be encoded in terms of whileDo without changing its big-step semantics. Is there a form of induction that allows me to combine "cases" with induction? I want to perform induction on the first argument "(repeatUntil S B, s) ⟹ t", but this does not work outright since the indices are not variables. On the other hand, the cases tactic does not give me an inductive hypothesis. If I try to use dependent pattern matching, Lean fails to infer termination.

I could of course employ the standard trick and generalize the goal to something like "x ⟹ t \to (repeatUntil S B, s) = x \to (S; whileDo (fun s => ¬ (B s)) S, s) ⟹ t" but surely there must be something better.

Thanks in advance,

Kristina

Aaron Liu (Mar 13 2025 at 11:54):

Can you post a #mwe?

Kristina Sojakova (Mar 13 2025 at 13:02):

I would like something along the following example to work:

def State : Type := String → Nat

inductive Prog : Type where
  | seq         : Prog → Prog → Prog
  | whileDo     : (State → Bool) → Prog → Prog
  | repeatUntil : Prog → (State → Bool) → Prog

infixr:90 "; " => Prog.seq

inductive BigStep : Prog × State → State → Prop where
  | seq (S T s t u) (hS : BigStep (S, s) t)
      (hT : BigStep (T, t) u) :
    BigStep (S; T, s) u
  | while_true (B S s t u) (hcond : B s)
      (hbody : BigStep (S, s) t)
      (hrest : BigStep (Prog.whileDo B S, t) u) :
    BigStep (Prog.whileDo B S, s) u
  | while_false (B S s) (hcond : ¬ B s) :
    BigStep (Prog.whileDo B S, s) s
  | repeatUntil_true (S B s t) (hcond : B t)
      (hbody : BigStep (S, s) t) :
    BigStep (Prog.repeatUntil S B, s) t
  | repeatUntil_false (B S s t u) (hcond : ¬ B t)
      (hbody : BigStep (S, s) t)
      (hrepeat : BigStep (Prog.repeatUntil S B, t) u) :
    BigStep (Prog.repeatUntil S B, s) u

infix:110 " ⟹ " => BigStep

theorem Prog.repeatUntil_correct_left_to_right {S B s t} :
  (Prog.repeatUntil S B, s) ⟹ t →
  (S; whileDo (fun s => ¬ (B s)) S, s) ⟹ t :=
  by intro h
     cases h with
       | repeatUntil_true B S s t hcond hbody =>
         apply BigStep.seq (t := t)
         { exact hbody }
         { apply BigStep.while_false
           sorry }
       | repeatUntil_false S B s r t hcond hbody hrepeat =>
         apply Prog.repeatUntil_correct_left_to_right at hrepeat
         apply BigStep.seq (t := r)
         { exact hbody }
         { cases hrepeat with
             | seq _ _ _ q _ hS hwhile =>
               apply BigStep.while_true (t := q)
               { sorry }
               { sorry }
               { sorry } }