Lean infering wrong induction hypothesis

Stream: new members

[Do Nhat Minh]

I'm proving the following theorem in Lean.

theorem progress {t T} (ht : has_type context.empty t T) :
  value t ∨ ∃t', t -+> t' :=
begin
  induction t,
    case tm.var: { exact false.elim (var_not_has_type_empty_context ht) },
    case tm.abs: { exact or.inl v_abs },
    case tm.app: t₁ t₂ ih₁ ih₂ {
      sorry,
    },
    case tm.tru: { exact or.inl v_tru },
    case tm.fls: { exact or.inl v_fls },
    case tm.tst: t₁ t₂ t₃ ih₁ ih₂ ih₃ {
      sorry,
    },
end

If I remove sorry in case tm.app, Lean tells me that ih₁ has type has_type context.empty t₁ T -> value t₁ ∨ ∃t', t₁ -+> t', which is wrong.

The definitions for ty, tm, value, and has_type can be found here.

Can anyone please give me a hint on how to proceed?

[Kenny Lau]

why is it wrong?

[Kenny Lau]

inductive tm : Type
| var : string -> tm
| app : tm -> tm -> tm
| abs : string -> ty -> tm -> tm
| tru : tm
| fls : tm
| tst : tm -> tm -> tm -> tm

in particular | app : tm -> tm -> tm, so case tm.app reads "t is now tm.app t1 t2 where t1 and t2 satisfy the proposition, and we prove that t also satisfies the proposition"

[Kenny Lau]

the proposition of course being has_type context.empty t T -> value t or exists t', t -+> t'

[Do Nhat Minh]

it should have type has_type context.empty t₁ (arrow T₁ T₂) -> value t₁ ∨ ∃t', t₁ -+> t'

[Do Nhat Minh]

how should I change the definition of tm to make that happen?

[Kenny Lau]

you should induct on ht instead

[Do Nhat Minh]

I'm translating the definition in Coq found here to Lean and I'm not doing a good job at it

[Do Nhat Minh]

induction on ht also gives me wrong hypotheses, such as a new context (named ht_context) for case has_type.t_var

[Do Nhat Minh]

(deleted)

[Kenny Lau]

theorem progress {t T} (ht : has_type context.empty t T) :
  value t ∨ ∃t', t -+> t' :=
begin
  revert ht, generalize he : context.empty = e, intro ht,
  induction ht,
  case has_type.t_var : e s t ht { rw ← he at ht, cases ht },
  case has_type.t_abs : { left, constructor },
  case has_type.t_app : e t₁ t₂ m₁ m₂ h₁ h₂ h₃ h₄ { sorry },
  case has_type.t_tru : { left, constructor },
  case has_type.t_fls : { left, constructor },
  case has_type.t_tst : { sorry }
end

[Do Nhat Minh]

Could you please explain what revert and generalize does?

[Marc Huisinga]

revert and generalize are also explained here: https://leanprover.github.io/theorem_proving_in_lean/tactics.html#basic-tactics

[Kenny Lau]

@Do Nhat Minh you can compare the state before and after those tactics

[Kenny Lau]

theorem progress {t T} (ht : has_type context.empty t T) :
  value t ∨ ∃t', t -+> t' :=
begin /-  state 1 -/
  revert ht,  /- state 2 -/ generalize he : context.empty = e,  /- state 3 -/ intro ht,
  induction ht,
  case has_type.t_var : e s t ht { rw ← he at ht, cases ht },
  case has_type.t_abs : { left, constructor },
  case has_type.t_app : e t₁ t₂ m₁ m₂ h₁ h₂ h₃ h₄ { sorry },
  case has_type.t_tru : { left, constructor },
  case has_type.t_fls : { left, constructor },
  case has_type.t_tst : { sorry }
end

[Kenny Lau]

state 1:

1 goal
t : tm,
T : ty,
ht : has_type context.empty t T
⊢ value t ∨ ∃ (t' : tm), t -+> t'

state 2:

1 goal
t : tm,
T : ty
⊢ has_type context.empty t T → (value t ∨ ∃ (t' : tm), t -+> t')

state 3:

1 goal
t : tm,
T : ty,
e : context,
he : context.empty = e
⊢ has_type e t T → (value t ∨ ∃ (t' : tm), t -+> t')

[Kenny Lau]

theorem progress {t T} (ht : has_type context.empty t T) :
  value t ∨ ∃t', t -+> t' :=
begin
  revert ht, generalize he : context.empty = e, intro ht,
  induction ht,
  case has_type.t_var : e s t ht { rw ← he at ht, cases ht },
  case has_type.t_abs : { left, constructor },
  case has_type.t_app : e t₁ t₂ m₁ m₂ h₁ h₂ h₃ h₄ {
    cases h₃ he with h₅ h₅, cases h₄ he with h₆ h₆,
    { cases h₅; cases h₁, right, existsi _, exact step.st_appabs h₆ },
    { cases h₆ with t' h₆, right, existsi _, exact step.st_app2 h₅ h₆ },
    { cases h₅ with t' h₅, right, existsi _, exact step.st_app1 h₅ }
  },
  case has_type.t_tru : { left, constructor },
  case has_type.t_fls : { left, constructor },
  case has_type.t_tst : e y t₁ t₂ t₃ h₁ h₂ h₃ h₄ h₅ h₆ { sorry }
end

[Do Nhat Minh]

Thanks, @Kenny Lau !

[Do Nhat Minh]

That helps!

[Do Nhat Minh]

Thanks for the pointer, @Marc Huisinga

[Do Nhat Minh]

I've read the whole book but the explanation for generalize is not clear to me

[Mario Carneiro]

If you want to prove P foo, it suffices to prove \forall x, P x. generalize : foo = x will do that. Similarly, it suffices to prove \forall x, foo = x -> P x, and generalize h : foo = x will do that (introducing x and h : foo = x).

[Do Nhat Minh]

That really helps! Thanks, @Mario Carneiro !