# Zulip Chat Archive

## 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