How to reduce repeated proofs in cases

Stream: general

[xiao]

I am modeling simply-typed lambda-calculus, but I see some repeated tactics. Here's a minimal example.

Let's first define types Ty and terms Tm.

inductive Ty: Type where
  | Nat | Bool


inductive Tm: Type where
  | zero: Tm
  | succ: Tm -> Tm
  | add: Tm -> Tm -> Tm
  | true: Tm
  | false: Tm
  | ite: Tm -> Tm -> Tm -> Tm

with the obvious computation and typing rules

inductive Tm.step: Tm -> Tm -> Prop where
  | zeroAdd {m2: Tm}: (Tm.add .zero m2).step m2
  | succAdd {m1 m2: Tm}: (Tm.add m1.succ m2).step (m1.add m2).succ
  | succ {m m': Tm}: m.step m' -> m.succ.step m'.succ
  | add1 {m1 m1' m2: Tm}: m1.step m1' -> (m1.add m2).step (m1'.add m2)
  | add2 {m1 m2 m2': Tm}: m2.step m2' -> (m1.add m2).step (m1.add m2')
  | ifTrue {t f: Tm}:
    (Tm.ite .true t f).step t
  | ifFalse {t f: Tm}:
    (Tm.ite .false t f).step f
  | if1 {c c' t f: Tm}:
    c.step c' ->
    (Tm.ite c t f).step (Tm.ite c' t f)
  | if2 {c t t' f: Tm}:
    t.step t' ->
    (Tm.ite c t f).step (Tm.ite c t' f)
  | if3 {c t f f': Tm}:
    f.step f' ->
    (Tm.ite c t f).step (Tm.ite c t f')


inductive Tm.has_type: Tm -> Ty -> Prop where
  | zero: Tm.zero.has_type .Nat
  | succ {m: Tm}:
    m.has_type .Nat ->
    m.succ.has_type .Nat
  | add {m1 m2: Tm}:
    m1.has_type .Nat ->
    m2.has_type .Nat ->
    (m1.add m2).has_type .Nat
  | true: Tm.true.has_type .Bool
  | false: Tm.false.has_type .Bool
  | ite {c t f: Tm} {T: Ty}:
    c.has_type .Bool ->
    t.has_type T ->
    f.has_type T ->
    (Tm.ite c t f).has_type T

I want to prove that the types are preserved after each computation step.

theorem Ty.preserve {m m': Tm} {T: Ty}:
  m.has_type T ->
  m.step m' ->
  m'.has_type T
:= by
  intro Ht Hstep
  induction m generalizing m' T with
  | zero | true | false =>
    cases Hstep
  | succ n IH =>
    cases Ht
    cases Hstep with
    | succ =>
      constructor <;>
        solve_by_elim
  | add m1 m2 IH1 IH2 =>
    cases Ht
    cases Hstep with
    | zeroAdd =>
      solve_by_elim
    | succAdd =>
      next Ht =>
      cases Ht
      -- solve_by_elim
      apply Tm.has_type.succ
      apply Tm.has_type.add
      . assumption
      . assumption
    | add1 | add2 =>
      constructor <;>
        solve_by_elim
  | ite m1 m2 m3 IH1 IH2 IH3 =>
    cases Ht
    cases Hstep with
    | ifTrue =>
      solve_by_elim
    | ifFalse =>
      solve_by_elim
    | if1 | if2 | if3 =>
      constructor <;>
        solve_by_elim

You may have observed that those computation rules (Tm.step) are split into two cases:

1. The real computation rules like zeroAdd, succAdd, ifTrue, ifFalse;
2. And the compatibility rules that make the equivalence closure of Tm.step a congruence relation, i.e. succ, add1, add2, if1, if2, if3.

When I proved Ty.preserve, I did the induction on m, and in each case of the induction, I took the inversion of step. Then, for each possible case of step, I did the corresponding proof. Of course, those cases of step split into two situations:

1. They are some real computation rules;
2. They are some compatibility rules.

The core of the proof is to satisfy those computation rules, while for the compatibility rules, the theorem follows naturally from the constructors and other (inductive) hypotheses. So, they are proved by constructor <;> solve_by_elim.

My question is how I can reduce those repeated constructor <;> solve_by_elim. I only want to focus on the computational rules. In my real case, the repeated tactics are relatively long. I hope not to repeat them.
You can find my code here.

[Robin Arnez]

Why not simply do induction on Hstep?

[xiao]

I think you are correct for this case. I can certainly do induction on Hstep. But, is there any general answer on that? I am not sure whether I will encounter the same case while I cannot do the induction on the inner one.

[Robin Arnez]

I mean, you can also just

theorem Ty.preserve {m m' : Tm} {T : Ty} (Ht : m.has_type T) (Hstep : m.step m') :
    m'.has_type T := by
  induction m generalizing m' T <;> grind [cases Tm.step, Tm.has_type]

[Robin Arnez]

Or well

theorem Ty.preserve {m m' : Tm} {T : Ty} (Ht : m.has_type T) (Hstep : m.step m') :
    m'.has_type T := by
  induction Hstep generalizing T <;> grind [Tm.has_type]

[xiao]

Well, still thank you. I am not seeking for a shorter solution for this specific example, but in general, how to reduce the replication. Here's the real case. Maybe the replication is inevitable.

[Robin Arnez]

Hmm I'm still not quite sure what you are looking for, is it something like this?

cases x with first | constructor <;> solve_by_elim | solve_by_elim | skip with
...

That way, all the cases that can be solved by constructor <;> solve_by_elim or solve_by_elim can be omitted

[xiao]

I think first | constructor <;> solve_by_elim | skip is something I want. Thank you.

In case | add and | ite, I don't want to | zeroAdd, | succAdd, ifTrue, ifFalse to be solved, because they are the computation parts so I want to hand write a proof, while for the other branches, I want them to be solved automatically by some common tactics.

For example, something like

induction m generalizing m' T with (
    cases Ht <;>
      cases <Hstep> <;>
        constructor <;>
          solve_by_elim
  )
  | add m1 m2 IH1 IH2 =>
    cases Hstep with
    | zeroAdd =>
      solve_by_elim
    | succAdd =>
      next Ht =>
      cases Ht
      -- solve_by_elim
      apply Tm.has_type.succ
      apply Tm.has_type.add
      . assumption
      . assumption
  | ite m1 m2 m3 IH1 IH2 IH3 =>
    cases Ht
    cases Hstep with
    | ifTrue =>
      solve_by_elim
    | ifFalse =>
      solve_by_elim

I want to preserve the cases for zeroAdd, succAdd, ifTrue, ifFalse because they are the computation parts, while I don't want to focus on add1, add2, if1, if2, if3 because they are just the compatibility rules.

Even if there exists some shorter proof for

next Ht =>
      cases Ht
      -- solve_by_elim
      apply Tm.has_type.succ
      apply Tm.has_type.add
      . assumption
      . assumption

I still want to write this silly proof in order to show the computation process for a pedagogical purpose.

[Robert Maxton]

Another trick you can try: refine ?h names the placeholder it creates h, so you can access it later with case h and even (sometimes) reuse it in other terms by re-mentioning ?h (though for some reason you can only do this before you close the goal it's attached to, so you need to either reorder your proof accordingly or do have h := ?h to 'save' it to a local variable. Similarly, refine (fun x => ⟨?f, ?g⟩) ?x creates three goals x, f, g where an opaque variable referencing x appears in the contexts of f and g

[xiao]

I see. Thank you!