showing big_step is deterministic

Stream: lean4

[Daniel Bourgeois]

I'm attempting to translate the lean3 example files from Ch8 logical verification course to lean4.

To prove the deterministic theorem, induction on hl seems the way to go,
but deterministic1 gives induction hl fails.

deterministic2 uses match, but the inaccessible variables are preventing
progress.

Any suggestions?
MWE

abbrev state  : Type := String → Nat

def state.update (name : String) (val : Nat) (s : state) : state :=
  λ n ↦ ite (name = n) val (s n)

inductive stmt : Type
  | skip   : stmt
  | assign : String → (state → Nat) → stmt
  | seq    : stmt → stmt → stmt
  | ite    : (state → Prop) → stmt → stmt → stmt
  | while  : (state → Prop) → stmt → stmt

inductive big_step : stmt × state → state → Prop
| skip {s} :
  big_step (stmt.skip, s) s
| assign {x a s} :
  big_step (stmt.assign x a, s) (state.update x (a s) s)
| seq {S T s t u} (hS : big_step (S, s) t)
    (hT : big_step (T, t) u) :
  big_step (stmt.seq S T, s) u
| ite_true {b : state → Prop} {S T s t} (hcond : b s)
    (hbody : big_step (S, s) t) :
  big_step (stmt.ite b S T, s) t
| ite_false {b : state → Prop} {S T s t} (hcond : ¬ b s)
    (hbody : big_step (T, s) t) :
  big_step (stmt.ite b S T, s) t
| while_true {b : state → Prop} {S s t u} (hcond : b s)
    (hbody : big_step (S, s) t)
    (hrest : big_step (stmt.while b S, t) u) :
  big_step (stmt.while b S, s) u
| while_false {b : state → Prop} {S s} (hcond : ¬ b s) :
  big_step (stmt.while b S, s) s

def deterministic1 {S s l r} (hl : big_step (S, s) l) (hr : big_step (S, s) r) : l = r := by
  induction hl
  -- index in target's type is not a variable (consider using the `cases` tactic instead)

def deterministic2 {S s l r} (hl : big_step (S, s) l) (hr : big_step (S, s) r) : l = r := by
  match hl with
  | big_step.skip =>
    match hr with
    | big_step.skip => rfl
  | big_step.assign =>
    match hr with
    | big_step.assign => rfl
  | big_step.ite_true lcond lbody =>
    match hr with
    | big_step.ite_true rcond rbody => exact (deterministic2 lbody rbody)
    | big_step.ite_false rcond rbody => trivial
  | big_step.ite_false lcond lbody =>
    match hr with
    | big_step.ite_true rcond rbody => trivial
    | big_step.ite_false rcond rbody => exact (deterministic2 lbody rbody)
  | big_step.while_true lcond lbody lrest =>
    match hr with
    | big_step.while_true rcond rbody rrest =>
      --   lcond : b✝ s
      --   lbody : big_step (S✝, s) t✝¹
      --   lrest : big_step (stmt.while b✝ S✝, t✝¹) l
      --   rcond : b✝ s
      --   rbody : big_step (S✝, s) t✝
      --   rrest : big_step (stmt.while b✝ S✝, t✝) r
      -- Would like to:
      --  1. recurse on lbody, rbody to show t✝¹ = t✝
      --  2. replace t✝¹ with t✝
      --  3. recurse on lrest, rrest to show l = r

[James Gallicchio]

oh, I feel like this might be a regression of the induction tactic

[James Gallicchio]

cuz I think in Lean3 it would generalize (S,s) = s' such that the index is a variable. you can do this manually in Lean4 with the generalize tactic

[James Gallicchio]

RE: unreachable names, you can use next a b ... => ... to give names to the most recent unreachable variables

[Jannis Limperg]

The induction' tactic which we use for Lean 3 LoVe does generalisation automatically. Stock induction probably doesn't, or at least not correctly. It's actually nicer that Lean 4 induction refuses to operate in this situation instead of doing the likely-wrong thing.

[James Gallicchio]

(induction' is defined in Mathlib, in case you weren't importing Mathlib already)

[Daniel Bourgeois]

next tactic worked for the deterministic2 attempt, but it looks like using the match approach isn't appropriate because it doesn't show no termination

I'll take a look at the induciton' mathlib tactic :working_on_it:

[Mario Carneiro]

James Gallicchio said:

(induction' is defined in Mathlib, in case you weren't importing Mathlib already)

Actually I think that's the wrong induction'

[Mario Carneiro]

the mathlib4 induction' tactic is a replacement for lean 3 induction, and lean 3 induction' is still on the todo list (it might have been marked as "skip" because there aren't any uses of it in mathlib)