Induction on hypotheses

Stream: mathlib4

[Tanner Duve]

Is there a way to perform induction on a hypothesis? Cases is useful but I'd like to be able to generate induction hypotheses when I case on a hypothesis.

[Newell Jensen]

Do you have an #mwe?

[Mario Carneiro]

induction H

[Tanner Duve]

I have a file full of definitions which this snippet depends on, but I am doing an implementation of the STLC, and am currently trying to prove the progress theorem. Here is the goal extracted from where I am stuck:

theorem extracted_1 (t : tm) (T : ty) (HT : empty |- t ∈ T) : value t ∨ ∃ t', t==>t' := sorry

This just says, given a term t, a type T, and evidence HT that t is of type T in the empty context, show that either t is a value or there is a t' which t steps to (by my operational semantics) I would like to do an induction on the typing derivation HT of the term t, but "induction HT" gives me "tactic 'induction' failed, major premise type is not an inductive type", same with induction' HT.

[Yury G. Kudryashov]

How long are the definitions of all the types needed for the example?

[Yury G. Kudryashov]

If they are not that long, then you can copy+paste them here.

[Yury G. Kudryashov]

We can't help unless we know what does empty |- t ∈ T mean.

[Tanner Duve]

Here is my inductive relation for my typing rules + the prerequisite map definitions

---- Typing

------ Total and Partial Maps

def total_map (A : Type) := String → A

def empty_map {A : Type} (v : A) : total_map A :=
  fun _ => v

def t_update {A : Type} (m : String → A) (x : String) (v : A) : String → A :=
  fun x' => if x = x' then v else m x'

notation x " !-> " v " ; " m => t_update m x v

def partial_map (α : Type) := total_map (Option α)

def empty {α : Type} : partial_map α :=
  empty_map none

def update {A : Type} (m : partial_map A) (x : String) (v : A) : partial_map A :=
  x !-> some v ; m

notation x " |-> " v " ; " m => update m x v
---- We let a "context" be a partial map for types
def context := partial_map ty
---- has_type Γ t T (equivalently, Γ |- t ∈ T) means that in the typing context Γ, the term t has type T
inductive has_type : context -> tm -> ty -> Prop :=
  | T_Var : ∀ Γ x T,
    Γ x = some T →
    has_type Γ (tm.tm_var x) T
  | T_Abs : ∀ x T1 T2 t1 Γ,
    has_type (x |-> T2; Γ) t1 T1 →
    has_type Γ (<{λx : T2, t1}>) (T2->T1)
  | T_App : ∀ Γ t1 t2,
    has_type Γ t1 (T2 -> T1) ->
    has_type Γ t2 T2 ->
    has_type Γ (t1 ∘ t2) T1 -- t1 ∘ t2 means apply t1 to t2
  | T_True : ∀ Γ,
    has_type Γ true Bool
  | T_False : ∀ Γ,
    has_type Γ false Bool
  | T_If : ∀ Γ t1 t2 t3 T1,
    has_type Γ t1 Bool →
    has_type Γ t2 T1 →
    has_type Γ t3 T1 →
    has_type Γ <{if t1 then t2 else t3}> T1

notation Γ:99 " |- " t1:99 " ∈ " T2:99 => has_type Γ t1 T2

[Tanner Duve]

and, in doing a proof, I have a hypothesis HT which just states that t has type T in the empty context (ie. empty |- t \in T), and I'd like to do induction on HT, but get the errors I mentioned above.

[Yury G. Kudryashov]

I copy+pasted your code and it doesn't work. Please fix it.

[Raghuram]

It appears that there are inductive types ty for types and tm for terms whose definitions are missing. I imagine they look something like this:

inductive ty
| fun : ty → ty → ty
| Bool

infixr:35 "->" => ty.fun

open ty (Bool)

inductive tm
| tm_var (var_name : String)
| lam (param_name : String) (param_type : ty) (body : tm)
| apply : tm → tm → tm
| true | false
| ite : tm → tm → tm → tm

macro "<{λ" x:ident " : " t:term ", " body:term "}>" : term =>
  `(term| tm.lam $(Lean.Quote.quote x.getId.toString) $t $body)
infixl: 50 "∘" => tm.apply
macro "<{if" cond:term " then " true:term " else " false:term "}>" : term =>
  `(term| tm.ite $cond $true $false)

open tm (true false)

This makes the given code work if placed before the definition of context.

[Raghuram]

Tanner Duve said:

I have a file full of definitions which this snippet depends on, but I am doing an implementation of the STLC, and am currently trying to prove the progress theorem. Here is the goal extracted from where I am stuck:

theorem extracted_1 (t : tm) (T : ty) (HT : empty |- t ∈ T) : value t ∨ ∃ t', t==>t' := sorry

This just says, given a term t, a type T, and evidence HT that t is of type T in the empty context, show that either t is a value or there is a t' which t steps to (by my operational semantics) I would like to do an induction on the typing derivation HT of the term t, but "induction HT" gives me "tactic 'induction' failed, major premise type is not an inductive type", same with induction' HT.

With the above definitions of ty and tm and your definitions for has_type, I can't reproduce your error. Instead I get a different error upon running induction HT:

theorem extracted_1 (t : tm) (T : ty) (HT : empty |- t ∈ T) :
  /- Definitions of value and ==> not given
    value t ∨ ∃ t', t==>t' -/
  False := by
  -- "index in target's type is not a variable (consider using the `cases` tactic instead)"
  -- i.e., empty is not a variable
  -- induction HT
  sorry

This error actually makes sense, because the context is an index and can change across the constructors. A standard way of dealing with this is to turn the context into a variable with a hypothesis that it's equal to the empty context, as follows:

  theorem (t : tm) (T : ty) (HT : empty |- t ∈ T) : False := by
  generalize context_empty : context = empty at HT
  induction HT
  all_goals sorry -- remove after proving

I feel like there should be an option in induction to does this directly, but I don't know/remember it if so.