quartztz's Tactic of the Week · `constructor`

this is a forum post i wrote for the Foundations of Software course i am currently taking at EPFL. the goal is to make this a recurring segment, but promises are the first step to failure, so i won’t make any.

in this rubric, i present the lean tactics i’ve discovered this week that are useful, fun or weird. feel free to skip these !

Say, for the sake of argument, that you have the following inductive definition:

inductive prog where
| Done
| Add (n : Nat) (p : prog)
| Mul (n : Nat) (p : prog)
| SetTo (n : Nat) (p : prog)

for a small programming language where you have a current integer state, and you modify it with simple expressions to yield a final state. we can define “running” a program in this language as an inductive relation!

-- run : init state -> prog -> final state
inductive run : Nat -> prog ->  Nat -> Prop where
-- running Done on state s yields s
| done (s : Nat) :
    run (s) (.Done) (s)
-- running (Add n) on state s yields state s' = (s + n)
| add (s n : Nat) (p : prog) (s' : Nat) :
    run (s + n) p s' -> run s (.Add n p) s'
-- running (Mul n) on state s yields state s' = (s * n)
| mul (s n : Nat) (p : prog) (s' : Nat) :
    run (s * n) p s' -> run s (.Mul n p) s'
-- running (Mul n) on state s yields state s' = (s * n)
| setTo (s n : Nat) (p : prog) (s' : Nat) :
    run n p s' -> run s (.SetTo n p) s'

this looks unwieldy at first, but it makes a lot of sense! we set the interpretation of the semantics of our language. we can verify this works with some unit tests, using the usual lean machinery:

def program1 : prog :=
  .Add 4 .Done

-- let's prove that running program1 on state 0 yields 4!
theorem program1_yields_4 : run 0 program1 4 := by
  unfold program1
  apply run.add
  apply run.done

simple enough! inductive definitions make this simplification very straightforward, and for longer proofs, we can use the good old calc keyword, by defining the proper transitivity properties.

consider now, for your enjoyment.

def program2 : prog :=
  -- a very, very long program 
  .Add 11 (.Mul 7 (
    .SetTo 9 (.Mul 13 (
      .Add 6 (.Mul 12 (
        .SetTo 8 (.Mul 10 (
          .Add 5 (.Mul 16 .Done)))))))))

theorem program2_yields_100 : run 0 program2 100 := by
  -- fun!

in this particular case, it is pretty straightforward (though tedious) to prove this by writing every constructor in order. however, every statement is the same, from a higher level standpoint! there must be a better way to do this. say, for example:

theorem program2_yields_100 : run 0 program2 1360 := by
  repeat constructor

this works! the constructor statement applies the most sensible constructor in this case (in definition order), as long as it makes progress. in this case, it’s convenient, but on more complex cases, over more abstract inductive notations, this tactic can save a lot of time, and remove a lot of visual complexity from the proof. in conjunction with calc proofs, this can lead to very intuitive and readable proofs!