A Question about Inductively Defined Propositions in Lean4

Question.lean

/-
# Question on Inductively Defined Propositions

I've hit a brick wall while learning Theorem Proving/Dependent Types, and that
brick wall is Inductively Defined Predicates.  There's *something* about them
that I'm not fully grokking, and I don't understand what I don't understand
well enough to articulate what I'm not getting.

I've finally found a (relatively) small example that illustrates the issue I'm
having in a way that someone can hopefully "fill in the blanks" as a jumping
off point for a deeper dive.

This example comes from the first chapter ([`Equiv`][1]) of
[Programming Language Foundations][2], the second book in the
[Software Foundations][3] series.  It's based on the [`Imp`][4] language, a
simple imperative programming language with numbers, booleans, variables, and
basic control structures, as presented in the first book in the series,
[Logical Foundations][5].  The `Imp` language is included here for context
along with an example theorem about the language that demonstrates the gap in
my knowledge.

The core of the problem is that I keep getting stuck when using Inductively
Defined Propositions.  I can typically work out the proofs informally, but I'm
struggling to actually manipulate the propositional values in Lean to build a
formal proof term.  And I'm struggling to find any tutorials (not just any
*good* tutorial, but any tutorial *at all*) on how to work with these terms
outside of the books I'm working from, which aren't helping.  They're only
barely touched on in Theorem Proving in Lean, so that's not been helpful for
this problem (though, TPIL was *super* helpful in learning how to translate
from Coq -> Lean and how to do term/calculational style proofs.)

[1](https://softwarefoundations.cis.upenn.edu/plf-current/Equiv.html)
[2](https://softwarefoundations.cis.upenn.edu/plf-current/index.html)
[3](https://softwarefoundations.cis.upenn.edu/)
[4](https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html)
[5](https://softwarefoundations.cis.upenn.edu/lf-current/toc.html)
-/

/-
## The `Imp` Language

This is my implementation of the `Imp` language from Logical Foundations.  It's
copy/pasted here for context and so the file is standalone.
-/

/-
### Maps

These are functional maps that back the state store.
-/

def TotalMap (α: Type): Type := String → α
def TotalMap.empty {α: Type} (default: α): TotalMap α := fun _ => default
def TotalMap.update {α: Type} (m: TotalMap α) (k: String) (v: α): TotalMap α :=
  fun k₁ => if k == k₁ then v else m k₁

/-
### States

The store for runtime variable bindings.
-/

def State: Type := TotalMap Nat
def State.empty: State := TotalMap.empty 0

/-
### Arithmetic Expressions

Arithmetic expressions.  These are `aexp` in the book.  Evaluation is defined
as a function and there is a Prop for equivalence.
-/

inductive Arith: Type where
  | num (n: Nat): Arith
  | ident (id: String): Arith
  | plus (e₁ e₂: Arith): Arith
  | minus (e₁ e₂: Arith): Arith
  | mult (e₁ e₂: Arith): Arith

def Arith.eval (state: State): Arith → Nat
  | num n => n
  | ident id => state id
  | plus e₁ e₂ => (e₁.eval state) + (e₂.eval state)
  | minus e₁ e₂ => (e₁.eval state) - (e₂.eval state)
  | mult e₁ e₂ => (e₁.eval state) * (e₂.eval state)

def Arith.equiv (a₁ a₂: Arith): Prop := ∀ s: State, a₁.eval s = a₂.eval s

/-
### Logical Expressions

Logical expressions.  These are `bexp` (Boolean Expressions) in the book.
Evaluation is defined as a function and there is a Prop for equivalence.
-/

inductive Logic: Type where
  | true: Logic
  | false: Logic
  | eq (e₁ e₂: Arith): Logic
  | neq (e₁ e₂: Arith): Logic
  | le (e₁ e₂: Arith): Logic
  | gt (e₁ e₂: Arith): Logic
  | not (e: Logic): Logic
  | and (e₁ e₂: Logic): Logic

def Logic.eval (state: State): Logic → Bool
  | true => Bool.true
  | false => Bool.false
  | eq e₁ e₂ => (e₁.eval state) == (e₂.eval state)
  | neq e₁ e₂ => (e₁.eval state) != (e₂.eval state)
  | le e₁ e₂ => (e₁.eval state) ≤ (e₂.eval state)
  | gt e₁ e₂ => (e₁.eval state) > (e₂.eval state)
  | not e => !(e.eval state)
  | and e₁ e₂ => (e₁.eval state) && (e₂.eval state)

def Logic.equiv (l₁ l₂: Logic): Prop := ∀ s: State, l₁.eval s = l₂.eval s

/-
### Commands

Top-level Imperative commands.  These are `com` in the book.  Evaluation is
defined as a relation since `Imp` programs can be non-terminating.  There is
also a Prop for equivalence.
-/

inductive Command: Type where
  | skip: Command
  | assign (id: String) (e: Arith): Command
  | seq (c₁ c₂: Command): Command
  | if (b: Logic) (c₁ c₂: Command): Command
  | while (b: Logic) (c: Command): Command

inductive CommandEval: Command → State → State → Prop where
  | skip (s: State): CommandEval .skip s s
  | assign (s: State) (e: Arith) (n: Nat) (id: String) (h: e.eval s = n): CommandEval (.assign id e) s (s.update id n)
  | seq (c₁ c₂: Command) (s₁ s₂ s₃: State) (h₁: CommandEval c₁ s₁ s₂) (h₂: CommandEval c₂ s₂ s₃): CommandEval (.seq c₁ c₂) s₁ s₃
  | ifTrue (s₁ s₂: State) (c: Logic) (t f: Command) (h₁: c.eval s₁ = .true) (h₂: CommandEval t s₁ s₂): CommandEval (.if c t f) s₁ s₂
  | ifFalse (s₁ s₂: State) (c: Logic) (t f: Command) (h₁: c.eval s₁ = .false) (h₂: CommandEval f s₁ s₂): CommandEval (.if c t f) s₁ s₂
  | whileTrue (s₁ s₂ s₃: State) (c: Logic) (b: Command) (h₁: c.eval s₁ = .true) (h₂: CommandEval b s₁ s₂) (h₃: CommandEval (.while c b) s₂ s₃): CommandEval (.while c b) s₁ s₃
  | whileFalse (c: Logic) (s: State) (b: Command) (h₁: c.eval s = .false): CommandEval (.while c b) s s

def Command.equiv (c₁ c₂: Command): Prop := ∀ s₁ s₂: State, CommandEval c₁ s₁ s₂ ↔ CommandEval c₂ s₁ s₂

/-
## The Problematic Theorem

This is the theorem `skip_left` from the book: the sequence of commands
`skip; c` is equivalent to the command `c`.

I've given it two ways: as a Term-style proof and as a Tactic-style proof.  I'm
stuck at the same point on both, so I don't believe it's an issue of not
understanding one style or the other.

FWIW, I've done large portions of the Natural Number Game, the Set Theory Game,
and many of the Logical Foundations proofs in Term/Calculational, Tactic, and
"Blended" styles.  I really like that Lean lets me jump in and out of tactic
mode as is convenient.  I find the term-style proofs much easier to follow
even if they are more verbose since they're more like functional pattern
matching I'm familiar with.  Tactic-style proofs can be really, really opaque.
-/

/-
### Term-Style Proof

The Reverse Modus Ponens direction makes complete sense to me, as does the idea
of building the two proofs and packing them into the struct with `⟨..., ...⟩`.
It's just building up terms like you would do with a sum type in any functional
language, except that some of the terms are dependent types/hypotheses.

What I'm confused about is going the other way.  It's the core of what I "don't
get" about inductive predicates.  I'm stuck in this same or a similar spot on a
lot of the `IndProp` proofs in Logical Foundations.  The ones I did get, I got
by fiddling instead of by understanding.
-/

example (c: Command): (Command.seq .skip c).equiv c :=
  fun s₁ s₂ =>
    have mp: CommandEval (Command.seq .skip c) s₁ s₂ → CommandEval c s₁ s₂
      | .seq .skip c s₁ s₂ s₃ h₁ h₂ =>
        have h₃: s₁ = s₂ :=
          /-
          [Question #1] This must be true, since the first command is a skip.
          How do I communicate that to Lean?

          More generally, do I use the information embedded in the
          premise/hypothesis to advance through the proof when the hypothesis
          is an inductively defined predicate?
          -/
          sorry
        by
          /-
          [Question #2] How do I do this rewrite purely term-style?  I have
          done plenty of calculational proofs with lots of `congr`,
          `congrArg`, and `congrFun` so I know it can get messy.  But I
          think it would be illustrative to see this worked out in all its
          gory details as it would be more examples of how to use inductive
          predicates in the way I don't get.
          -/
          rw [← h₃] at h₂
          exact h₂
    have mpr: CommandEval c s₁ s₂ → CommandEval (Command.seq .skip c) s₁ s₂
      | .skip _                        => .seq _ _ _ _ _ (.skip _) (.skip _)
      | .assign _ _ _ _ h              => .seq _ _ _ _ _ (.skip _) (.assign _ _ _ _ h)
      | .seq _ _ _ s₂ _ h₁ h₂          => .seq _ _ _ _ _ (.skip _) (.seq _ _ _ s₂ _ h₁ h₂)
      | .ifTrue _ _ _ _ _ h₁ h₂        => .seq _ _ _ _ _ (.skip _) (.ifTrue _ _ _ _ _ h₁ h₂)
      | .ifFalse _ _ _ _ _ h₁ h₂       => .seq _ _ _ _ _ (.skip _) (.ifFalse _ _ _ _ _ h₁ h₂)
      | .whileTrue _ s₂ _ _ _ h₁ h₂ h₃ => .seq _ _ _ _ _ (.skip _) (.whileTrue _ s₂ _ _ _ h₁ h₂ h₃)
      | .whileFalse _ _ _ h₁           => .seq _ _ _ _ _ (.skip _) (.whileFalse _ _ _ h₁)
    ⟨mp, mpr⟩

/-
### Tactic-Style Proof

I've gone code-golfing on the MPR half as much as I could, but I still have
some (minor, secondary) questions about why the two cases did't get handled by
the `try`.

But more important is [Question #3]: The `inversion` tactic.  In the book, this
is the Coq proof they give:

```
Theorem skip_left : ∀ c, cequiv <{ skip; c }> c.
Proof.
  intros c st st'.
  split; intros H.
  - (* -> *)
    inversion H. subst.
    inversion H2. subst.
    assumption.
  - (* <- *)
    apply E_Seq with st.
    + apply E_Skip.
    + assumption.
Qed.
```
They use this `inversion` tactic all over the place to make their proofs
shorter, but I can't find an equivalent in Lean.  Is there one?

I've started working on a Coq -> Lean Tactic CheatSheet (included in this
Gist), and this is one of the tactics that I don't know how to translate.
A quick review of that would be appreciated as well.

Relatedly, I've noticed that the Induction Principle generated by Lean
is different from the one that Coq generates.  The variant that Lean
generates is mentioned as the "alternative" induction principle in the
`IndPrinciples` chapter of Logical Foundations.  I'm guessing that this
is related to why the proofs look so radically different, but I don't
know.
-/

example (c: Command): (Command.seq .skip c).equiv c := by
  unfold Command.equiv
  intro s₁ s₂
  apply Iff.intro
  · intro h
    cases h with
      | seq c₁ c₂ s₁ s₂ s₃ h₁ h₂ =>
        /-
        [Question #1] Same as above.  Is there a tactic-specific way of solving
        this?
        -/
        sorry
  · intro h
    cases h
    <;> try (apply CommandEval.seq
             · apply CommandEval.skip
             . constructor
               repeat assumption)
    case ifFalse =>
      apply CommandEval.seq
      · apply CommandEval.skip
        /-
        [Question #4] Why doesn't the `constructor` tactic work here like in
        all the other cases?
        -/
      . apply CommandEval.ifFalse
        repeat assumption
    case whileFalse =>
      apply CommandEval.seq
      · apply CommandEval.skip
        /-
        [Question #4] Again.  They're both cases where `c.eval s = false`.
        Does that have something to do with it?
        -/
      · apply CommandEval.whileFalse
        repeat assumption

TacticsCheatSheet.md

Coq <-> Lean4 Tactics Cheat Sheet

This is a list of Coq tactics and their (rough) equivalent in Lean4. It's important to note that these are often not quite equivalent.

Tactics

Coq	Lean	Notes
intros	intro	Lean4 also supports pattern matching
reflexivity	rfl
apply	apply
apply ... in	???	How do I do an apply to a hypothesis in the context?
apply ... with	apply	Supports explicit positional args (apply foo 1 2 3) or named args (apply foo (x := 1) (z := 3))
simpl	simp	Also has variants simp [... theorems ...], simp only [... theorems ...], simp_all, and other more specialized varieties. Theorems can be added to the simplifier using the @[simp], @[local simp] (restricted to the current file), and @[scoped simp] (restricted to the current scope and all sub-scopes) annotations. Any theorem added to the simplifier should "make progress" when read left to right. So x + 0 = x is a good candidate, but x + y = y + x is not.
simpl in h	simp at h
rewrite	rw (or rewrite)	Automatically calls try rfl
rewrite ... in h	rw ... at h
symmetry	symm	Requires import Mathlib.Tactic.Relation.Symm and only works on Symmetric relations
symmetry at h	symm at h	Same notes as symm
transitivity	trans	Requires import Mathlib.Tactic.Relation.Trans and only works on Transitive relations, also supports trans at h
unfold	unfold (related: @[reducible]/abbrev)	The @[reducible] annotation on a definition allows tactics to auto-unfold the a definition (@[reducible] def foo := ...). The abbrev is an abbreviation (typically for a type) which is reducible (abbrev Sum: Type := List Parts). See this StackExchange post for more details.
unfold ... in h	unfold ... at h
destruct ... as, destruct ... eqn	cases ...
induction ... as ...	induction ... with
injection	???	???
discriminate	???	???
assert (H: e) or assert (e) as H	have h: ... := ...	have is very similar to a local let binding. The name is optional, and defaults to the name this.
generalize dependent	generalize or revert	???. Not sure which...
f_equal	funext	???. Maybe?
	contradiction	Handles a lot of cases, some of which are covered by the Coq injection and discriminate tactics (I think...).
left, right	???
inversion	???	Really want to figure this one out
lia	linarith	Requires import Mathlib.tactic.linarith
clear	clear
rename ... into ...	rename ... => ...
assumption	assumption
constructor	constructor
auto	???
eapply	eapply
congruence	congr
intuition	???

Tacticals

| Coq | Lean | Notes | | try | try | | | ; | <;> | | | repeat | repeat | | | subst | subst | |

Other

Some Coq tactics allow referencing the goal as goal. Lean doesn't seem to have the same functionality.