neither computable nor noncomputable

Stream: general

[Scott Morrison]

It seems @Fox Thomson may have run into a bug in Lean, which I've posted as https://github.com/leanprover-community/lean/issues/451:

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

noncomputable def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives a warning definition 'N' was incorrectly marked as noncomputable, while

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives an error rec_fn_macro only allowed in meta definitions.

[Scott Morrison]

This is minimised from #3855, if it's helpful to see the original context, defining the combinatorial game "nim".

[Mario Carneiro]

the error suggests that it wants to be meta, not noncomputable

[Mario Carneiro]

Interestingly, you can get it to compile if you use noncomputable theory and also mark the def noncomputable

[Mario Carneiro]

None of the auxiliary definitions here should be noncomputable, but there are lots of noncomputable subterms in irrelevant positions, specifically O₁.out

[Mario Carneiro]

If you stick this before the definition it works just fine:

import set_theory.ordinal

def ordinal.out (o : ordinal) : Well_order :=
⟨o.out.α, λ x y, o.out.r x y, o.out.wo⟩

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

def N : ordinal → G
| O₁ := ⟨O₁.out.α,
  λ O₂, have hwf : ordinal.typein O₁.out.r O₂ < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂)⟩
using_well_founded {dec_tac := tactic.assumption}

ordinal.out "launders" quotient.out through a bunch of irrelevant types to make it computable

[Scott Morrison]

@Fox Thomson, do you want to try using Mario's ordinal.out?

[Fox Thomson]

@Mario Carneiro I tried adding this to my definition and it works if I 'prove' hwf by sorry but my current proof of hwf uses ordinal.type_out which I think is causing problems, how could I translate this to use your definition of ordinal.out?

def nim : ordinal → pgame
| O₁ := ⟨ O₁.out.α, O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁,
    from begin nth_rewrite_rhs 0 ←ordinal.type_out O₁, exact ordinal.typein_lt_type _ _ end,
    nim (ordinal.typein O₁.out.r O₂),
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁,
    from begin nth_rewrite_rhs 0 ←ordinal.type_out O₁, exact ordinal.typein_lt_type _ _ end,
    nim (ordinal.typein O₁.out.r O₂)⟩
using_well_founded {dec_tac := tactic.assumption}

[Mario Carneiro]

Same trick:

theorem ordinal.type_out' : ∀ (o : ordinal), ordinal.type (ordinal.out o).r = o := ordinal.type_out

use this instead of ordinal.type_out

[Mario Carneiro]

@Fox Thomson