Zulip Chat Archive

Stream: general

Topic: sum.rec

Reid Barton (May 01 2018 at 15:52):

I'm having a surprisingly hard time working with sum.rec. Specifically, I'm having trouble convincing Lean to give me an ordinary, non-dependent function as the result. I pasted a transcript here: https://gist.github.com/rwbarton/b6cbf07bd07afd89f8c2b4feef8cec5f

Kenny Lau (May 01 2018 at 15:53):

the type of the second term depends on the type of the first term though

Kenny Lau (May 01 2018 at 15:53):

sorry, I thought you were talking about sigma. ignore what I said.

Reid Barton (May 01 2018 at 15:54):

I'm especially confused that surjective ((λ a, sum.rec f g a) : α ⊕ β → γ) produces an error that seems to be complaining that the argument needs to be a non-dependent function, though I can kind of imagine how this might not be considered a bug

Reid Barton (May 01 2018 at 15:56):

It'd be really convenient for me if there was also a non-dependent eliminator sum.rec' : (α → γ) → (β → γ) → α ⊕ β → γ

Reid Barton (May 01 2018 at 15:56):

I noticed someone else came across the same issue, too:

lemma continuous_sum_rec {f : α → γ} {g : β → γ}
  (hf : continuous f) (hg : continuous g) : @continuous (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=

Reid Barton (May 01 2018 at 15:58):

That whole result type should really just be continuous (sum.rec' f g).

Reid Barton (May 01 2018 at 16:00):

I assume the same issue arises for any other type with multiple constructors, too

Mario Carneiro (May 01 2018 at 17:45):

I think the problem is that sum.rec uses the eliminator strategy, meaning it relies heavily on the expected type to determine the motive, but surjective does not give a sufficiently specific expected type ?M1 -> ?M2. You can fix the issue by annotating the metavariables of surjective:

@surjective (α ⊕ β) γ (λ a, sum.rec f g a)

Mario Carneiro (May 01 2018 at 17:47):

The eliminator strategy makes T.rec more or less unusable when unapplied; apparently superfluous eta expansions here are important to trigger the right strategy

Kevin Buzzard (May 01 2018 at 18:08):

Could this also be fixed by writing a second recursor?

Kevin Buzzard (May 01 2018 at 18:08):

i.e. is this a problem that the interface could solve?

Kenny Lau (May 01 2018 at 18:08):

yes

Mario Carneiro (May 01 2018 at 18:09):

yes, but that would require changing lean (which generates all the inductive theorems)

Kenny Lau (May 01 2018 at 18:09):

I think I'm instead reading "yes but you would need to PR core"

Mario Carneiro (May 01 2018 at 18:10):

yes, that's what I mean

Kevin Buzzard (May 01 2018 at 18:12):

So you can't just write a new recursor, with a different name, which runs on top of unmodded Lean 3.4.1?

Mario Carneiro (May 01 2018 at 18:13):

You can, but you would have to do so for every inductive type

Kevin Buzzard (May 01 2018 at 18:13):

but you could solve his one specific problem with sum.rec.

Kevin Buzzard (May 01 2018 at 18:14):

I have to ask these stupid questions because I have no understanding of the status of these elab commands

Kevin Buzzard (May 01 2018 at 18:14):

all I know is that if you don't like one, you can sometimes add an @ and get another one

Mario Carneiro (May 01 2018 at 18:14):

Sure, or.elim already exists and sum.elim could be similar

Kevin Buzzard (May 01 2018 at 18:21):

example (a b c : Prop) : @or.elim a b c = @or.rec_on a b c := rfl

Kevin Buzzard (May 01 2018 at 18:21):

so the only way these function differ is by magic

Kevin Buzzard (May 01 2018 at 18:21):

as far as I am concerned

Kevin Buzzard (May 01 2018 at 18:22):

Aah do they have different tags?

Kevin Buzzard (May 01 2018 at 18:22):

Not only are they the same theorem

Kevin Buzzard (May 01 2018 at 18:23):

they are the same proof

Kevin Buzzard (May 01 2018 at 18:23):

but one is tagged [reducible]and is protected

Kevin Buzzard (May 01 2018 at 18:24):

[reducible] is all about how eagerly the elaborator unfolds the definition, or something...

Kevin Buzzard (May 01 2018 at 18:24):

protected I have no idea. Something about avoiding overloading?

Reid Barton (May 01 2018 at 18:26):

protected means if you wrote open or (which you probably wouldn't), then you still wouldn't get the name rec_on as a synonym for or.rec_on

Kevin Buzzard (May 01 2018 at 18:31):

one is a def and one is a theorem. Does this make any difference?

Kevin Buzzard (May 01 2018 at 18:36):

unknown identifier 'rec_on'

Kevin Buzzard (May 01 2018 at 18:36):

so nobody is allowed to have rec_on?

Kevin Buzzard (May 01 2018 at 18:45):

import set_theory.ordinal_notation
open nonote
#check rec_on
/-
rec_on :
  Π (o : nonote),
    ?M_1 0 →
    (Π (e : nonote) (n : ℕ+) (a : nonote) (h : below a e), ?M_1 e → ?M_1 a → ?M_1 (oadd e n a h)) → ?M_1 o
-/

Kevin Buzzard (May 01 2018 at 18:45):

Do I win five pounds?

Reid Barton (May 01 2018 at 18:47):

then that means that nonote.rec_on was not declared as protected

Kevin Buzzard (May 01 2018 at 19:04):

What is the complete list of unprotected rec_ons? And are these bugs?

Kenny Lau (May 01 2018 at 20:14):

/-- This is a recursor-like theorem for `nonote` suggesting an
  inductive definition, which can't actually be defined this
  way due to conflicting dependencies. -/
@[elab_as_eliminator] def rec_on {C : nonote → Sort*} (o : nonote)
  (H0 : C 0)
  (H1 : ∀ e n a h, C e → C a → C (oadd e n a h)) : C o :=
begin
  cases o with o h, induction o with e n a IHe IHa,
  { exact H0 },
  { exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _) }
end

(set_theory.ordinal_notation, line 857)

Kenny Lau (May 01 2018 at 20:14):

it isn't automatically generated

Kenny Lau (May 01 2018 at 20:15):

but indeed, @Mario Carneiro should have made it protected

Last updated: Dec 20 2023 at 11:08 UTC