Zulip Chat Archive

Stream: lean4

Topic: Induction issue?


view this post on Zulip François G. Dorais (Apr 03 2021 at 17:27):

This stopped working since the March 29 nightly, where the induction can't find the Decidable P instance anymore.

def casesTFOn {motive : Prop  Sort _} (P) [inst : Decidable P] : (T : motive True)  (F : motive False)  motive P :=
  λ ht hf => match inst with
  | isTrue H => eqTrue H  ht
  | isFalse H => eqFalse H  hf

example (P) [Decidable P] : ¬¬P  P := by
  induction P using casesTFOn
/-
error: unsolved goals
case inst
P : Prop
⊢ Decidable P
-/
  admit
  admit

Looking around, commit 41539a77 is a likely cause of this change in behavior. Is this an intensional change or a bug?

view this post on Zulip Leonardo de Moura (Apr 03 2021 at 17:43):

I will take a look, thanks for identifying the commit that introduced the problem.


Last updated: May 18 2021 at 23:14 UTC