Controling induction hypothesis

Stream: general

[Paweł Balawender]

Hey! I got stuck on proving a property by structural induction and am convinced that the problem is in the way I applied the induction tactic in Lean 4. I boiled down the following MWE:

import Lean
import Qq
open Lean Elab Tactic Term Meta Syntax PrettyPrinter Qq

inductive Formula where
| var : Name -> Formula
| imp : Formula -> Formula -> Formula
deriving Repr, DecidableEq

notation:60 a " ==> " b => Formula.imp a b

inductive Derivable : (List Formula) -> Formula -> Prop where
| axK {Γ} {phi psi} : Derivable Γ $ phi ==> psi ==> phi
-- "multiplicative" version of modus ponens
| mult_mp {Γ1 Γ2} {phi psi} :
  Derivable Γ2 (phi ==> psi) ->
  Derivable Γ1 phi ->
  Derivable (Γ1 ++ Γ2) psi

theorem weakening {Γ} {φ ψ} : Derivable Γ ψ -> Derivable (φ :: Γ) ψ := by
  generalize Sub1 : φ :: Γ = Sub1_
  generalize Sub2 : ψ = Sub2_
  intro h
  induction h
  case _ phi psi =>
    apply Derivable.axK
  case _ a b c d imp base imp_ih base_ih =>
    -- the induction hypothesis for some reason is unusable...
    -- imp_ih : φ :: b = Sub1_ → ...
    -- base_ih : φ :: a = Sub1_ → ...
    -- but: Sub1 : φ :: (a ++ b) = Sub1_
    sorry

And have questions to you:
a) Can you somehow do without these ugly generalize?
b) Do we have some kind of compilation of popular pitfalls when using induction? (Maybe it would be a nice addition to the new channel :) (#general > Documenting lean pitfalls: feedback requested )

c) Originally, I did my induction using induction h with, but just couldn't get the pattern matching right for some reason. I don't submit a MWE here (because in a MWE I wasn't able to reproduce), but basically my cases after induction were labeled as mp.Constructor instead of Constructor I'd expect and nothing really worked to fix it instead of switching to induction h cases => syntax. Does it spark any light in your head if it's a known problem? If not, I will work on creating the MWE, but it's not that easily reproducible in my case

theorem deduction {Γ} : Derivable (var φ :: Γ) [Logic|ψ] <-> Derivable Γ [Logic|φ -> ψ] := by
  apply Iff.intro
  {
    -- trick to bypass "index in target's type is not a variable" at `induction h`
    generalize Sub1 : var φ :: Γ = Sub1_
    generalize Sub2 : var ψ = Sub2_
    intro h
    induction h with
    -- APPROACH 1:
    -- | mp.axK =>
    --   -- invalid alternative name 'mp.axK', expected 'assumption', 'axK', 'axS' or 'mult_mp'
    -- APPROACH 2:
    -- | axK =>
      -- unexpected token 'axK'; expected '_' or identifier
    -- APPROACH 3:
    -- | _ =>
      -- invalid occurrence of wildcard alternative, it must be the last alternative

[Kyle Miller]

The generalize didn't seem to be necessary. There also didn't seem to be any issue with using induction h with. In your full code, you don't define axK to be notation somewhere, do you?

import Lean
import Qq
open Lean Elab Tactic Term Meta Syntax PrettyPrinter Qq

inductive Formula where
| var : Name -> Formula
| imp : Formula -> Formula -> Formula
deriving Repr, DecidableEq

notation:60 a " ==> " b => Formula.imp a b

inductive Derivable : (List Formula) -> Formula -> Prop where
| axK {Γ} {phi psi} : Derivable Γ $ phi ==> psi ==> phi
-- "multiplicative" version of modus ponens
| mult_mp {Γ1 Γ2} {phi psi} :
  Derivable Γ2 (phi ==> psi) ->
  Derivable Γ1 phi ->
  Derivable (Γ1 ++ Γ2) psi

theorem weakening {Γ} {φ ψ} (h : Derivable Γ ψ) : Derivable (φ :: Γ) ψ := by
  induction h with
  | axK =>
    apply Derivable.axK
  | mult_mp imp base imp_ih base_ih =>
    rw [← List.cons_append]
    exact Derivable.mult_mp imp base_ih

[Kyle Miller]

The reverse direction needs generalization though:

theorem weakening' {Γ} {φ ψ} (h : Derivable (φ :: Γ) ψ) : Derivable Γ ψ := by
  generalize hΓ' : φ :: Γ = Γ' at h
  induction h generalizing φ Γ with
  | axK =>
    apply Derivable.axK
  | mult_mp imp base imp_ih base_ih =>
    rw [List.cons_eq_append_iff] at hΓ'
    obtain ⟨rfl, rfl⟩ | ⟨Γ2', rfl, rfl⟩ := hΓ'
    · have := Derivable.mult_mp (imp_ih rfl) base
      rwa [List.nil_append] at this
    · exact Derivable.mult_mp imp (base_ih rfl)

[Paweł Balawender]

Kyle Miller said:

theorem weakening' {Γ} {φ ψ} (h : Derivable (φ :: Γ) ψ) : Derivable Γ ψ := by
  generalize hΓ' : φ :: Γ = Γ' at h
  induction h generalizing φ Γ with
  | axK =>
    apply Derivable.axK
  | mult_mp imp base imp_ih base_ih =>
    rw [List.cons_eq_append_iff] at hΓ'
    obtain ⟨rfl, rfl⟩ | ⟨Γ2', rfl, rfl⟩ := hΓ'
    · have := Derivable.mult_mp (imp_ih rfl) base
      rwa [List.nil_append] at this
    · exact Derivable.mult_mp imp (base_ih rfl)

Thank you @Kyle Miller ! I appreciate you helping me. It's actually funny that you proved the other direction, as it shouldn't really be provable :) But it's just an artifact of the MWE-ization that the logic trivialized.

The issue with induction h with really was about me using axK in notation! I didn't immediately conclude that it's the problem, as I used it as constructor in other parts of the code without any problems. But inside pattern matching, the custom syntax was a problem!

I was able to use your solution to the <- direction to finish the proof of deduction theorem for Hilbert-style calculus. What you wrote is really sorcerous to me! (edit: okay, I just misunderstood $\forall \phi, \phi=X \rightarrow sth$ as $(\forall \phi, \phi=X) \rightarrow sth$, which didn't make any sense. now it's clear) Thank you! (complete code of what I wanted to achieve: live.lean-org