Equivalent to Coq's remember tactic

Stream: new members

[Horatiu Cheval]

Does Lean have something like Coq's remeber tactic or a way to retain information lost when doing induction? For context, I'm trying to prove a deduction theorem for a logical system, normally done by induction on derivations. A minimal example would be:

inductive formula
| atomic : formula
| implication : formula → formula → formula

inductive derivable : list formula → formula → Prop
| ax : ∀ {Γ : list formula} {A B : formula}, derivable Γ (formula.implication A A)
| mp : ∀ {Γ : list formula} {A B : formula}, derivable Γ A → derivable Γ (formula.implication A B) → derivable Γ B
| premise : ∀ {Γ : list formula} {A : formula}, A ∈ Γ → derivable Γ A

theorem deduction_theorem : ∀ {Γ : list formula} {p q : formula}, derivable (p :: Γ) q → derivable Γ (formula.implication p q) :=
begin
  intros Γ p q deriv,
  induction deriv,
  case premise: Γ' q' mem_q'_Γ'{
    -- Γ: list formula
    -- p q: formula
    -- Γ': list formula
    -- q': formula
    -- mem_q'_Γ': q' ∈ Γ'
    -- ⊢ derivable Γ (p.implication q')
    -- We need to retain the information that Γ' = p :: Γ
    sorry
  }
end

I am stuck at the premise case, because Lean replaces p :: Γ with a new term Γ', with no relation between them. In Coq I would use remeber to add the hypothesis Γ' = p :: Γ in order to solve this. Is there a way to do that in Lean?

[Mario Carneiro]

For cases, you can use cases e : term to add the assumption e : term = constructor ... in the subcases, but for induction you have to use generalize e : term = x first followed by induction x

[Mario Carneiro]

it is also often useful to use induction x; cases e in the latter case to immediately case on the equality, which may eliminate some of the inductive cases

[Mario Carneiro]

import tactic.basic

inductive formula
| atomic : formula
| implication : formula → formula → formula

inductive derivable : list formula → formula → Prop
| ax : ∀ {Γ : list formula} {A : formula}, derivable Γ (formula.implication A A)
| mp : ∀ {Γ : list formula} {A B : formula}, derivable Γ A → derivable Γ (formula.implication A B) → derivable Γ B
| premise : ∀ {Γ : list formula} {A : formula}, A ∈ Γ → derivable Γ A

theorem deduction_theorem : ∀ {Γ : list formula} {p q : formula}, derivable (p :: Γ) q → derivable Γ (formula.implication p q) :=
begin
  intros Γ p q deriv,
  generalize_hyp e : p :: Γ = Γ₁ at deriv,
  induction deriv,
  case premise: Γ' q' mem_q'_Γ' {
    cases e,
    obtain rfl | mem := mem_q'_Γ',
    { constructor },
    { sorry } }
end

[Horatiu Cheval]

That worked, thank you!