## Stream: new members

### Topic: Equivalent to Coq's remember tactic

#### Horatiu Cheval (Dec 14 2020 at 08:39):

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 (Dec 14 2020 at 08:40):

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 (Dec 14 2020 at 08:42):

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 (Dec 14 2020 at 08:51):

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 (Dec 14 2020 at 09:10):

That worked, thank you!

Last updated: May 13 2021 at 21:12 UTC