Description
Describe the bug
This came up on Zulip:
at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> Empty) is an inconsistent type (as you're creating a fixpoint for negation)?
And later in the thread:
at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> False) is an inconsistent type (as you're creating a fixpoint for negation)?
I looked into this and indeed Lean generates a recursor without an induction hypothesis for Fix.rec:
unsafe inductive Fix (f : Type u → Type u) where
| fix : f (Fix f) → Fix f
#check Fix.rec
-- Fix.rec.{u_1, u} {f : Type u → Type u} {motive : Fix f → Sort u_1}
-- (fix : (a : f (Fix f)) → motive (Fix.fix a))
-- (t : Fix f) : motive t
So I guess the Fix that comes out of the unsafe inductive declaration is an accidentally consistent but non-inductive type.
And the the answer:
it's still not consistent, using f := (. -> Empty)
my point is that the argument as to why it isn't consistent is wrong (or at least not clear)
This should be investigated and fixed.