Zulip Chat Archive

Stream: new members

Topic: Equivalent to Coq's remember tactic


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Dec 14 2020 at 09:10):

That worked, thank you!


Last updated: May 13 2021 at 21:12 UTC