Inferring the behavior of an unknown type's recursor

Stream: new members

[Pedro Minicz]

Is it possible to infer the behavior of an unknown type's recursor given enough information?

universe u

section

parameters {N : Type} {z : N} {s : N → N}
parameters (hz : ∀ x, s x ≠ z) (hs : ∀ x y, s x = s y → x = y)
parameter N.rec : Π {P : N → Sort u}, P z → (Π x, P x → P (s x)) → Π x, P x
variables {P : N → Sort u} {base : P z} {step : Π x, P x → P (s x)}

example : N.rec base step z = base := sorry
example (x : N) : N.rec base step (s x) = step x (N.rec base step x) := sorry

end

The only real difference that I see between N.rec and nat.rec is that N.rec is not universe polymorphic (it depends on the universe u and u is fixed in this context). But if finitely many universes are needed, the following can be done:

parameter N.rec1 : Π {P : N → Sort (u + 1}, P z → (Π x, P x → P (s x)) → Π x, P x
parameter N.rec2 : Π {P : N → Sort (u + 2}, P z → (Π x, P x → P (s x)) → Π x, P x
parameter N.rec3 : Π {P : N → Sort (u + 3}, P z → (Π x, P x → P (s x)) → Π x, P x
-- ...

If full universe polymorphism is required, would it be possible to prove the following?

axioms {N : Type} {z : N} {s : N → N}
axioms (hz : ∀ x, s x ≠ z) (hs : ∀ x y, s x = s y → x = y)
axiom N.rec : Π {P : N → Sort*}, P z → (Π x, P x → P (s x)) → Π x, P x
variables {P : N → Sort*} {base : P z} {step : Π x, P x → P (s x)}

example : N.rec base step z = base := sorry
example (x : N) : N.rec base step (s x) = step x (N.rec base step x) := sorry

[Anne Baanen]

I don't think you can prove this in Lean, since N.rec could e.g. swap the result for z and s z if it detects P z = P (s z).

[Anne Baanen]

However, since N.rec is polymorphic, you should be able to prove a metatheorem (in the vein of Wadler's "theorems for free") showing that it has to behave like recursion on natural numbers, conditional on the assumption that the definition of N consists only of Lean terms.

[Patrick Johnson]

The first example is false:

Proof

import tactic

universe u

section

parameters {N : Type} {z : N} {s : N → N}
parameters (hz : ∀ x, s x ≠ z) (hs : ∀ x y, s x = s y → x = y)
parameter N.rec : Π {P : N → Sort u}, P z → (Π x, P x → P (s x)) → Π x, P x
variables {P : N → Sort u} {base : P z} {step : Π x, P x → P (s x)}

lemma lem : N.rec base step z = base := sorry

end

example : false :=
begin
  classical,
  have := @lem ℕ 0 nat.succ (λ (f : ℕ → Type), λ z s n,
    if h : f n = Prop then by { rw h, exact true }
    else n.rec_on z s) (λ _, Prop) false (λ _ _, false),
  simp * at *,
end

The second example (the one that uses axioms) is unprovable I think.

The only real difference that I see between N.rec and nat.rec is that N.rec is not universe polymorphic (it depends on the universe u and u is fixed in this context)

I think that's not the real problem (you could always lift the type up/down to fit the expected universe, while preserving type cardinality). The real problem is that nat.rec has implicit reduction rules (kernel is aware that nat.rec base step 0 = base and nat.rec base step n.succ = step n (nat.rec base step n))