How to reduce `rec`

Stream: new members

[Alex Meiburg]

Tips on how I can try to simply down a goal like

option.rec 1 non_id.val
((λ (a : M), dite (a = 1) (λ (h : a = 1), none) (λ (h : ¬a = 1), some {val := a, not_one := h})) a) = 1

when I have h : a=1 in local context? I want to beta-reduce that lambda

[Ruben Van de Velde]

Does split_ifs do something?

[Alex Meiburg]

No, it says "no if-then-else expressions to split". I'm guessing because it's inside the lambda.

[Alex Meiburg]

This boils down to something of the form

option.rec X Y ((λ (a : M), f a) a) = 1

and I'm not clear on why the ((λ (a : M), f a) a) isn't turning itself into f a

[Ruben Van de Velde]

Do you have a #mwe?

[Alex Meiburg]

universe u

noncomputable def f {M : Type u} [has_one M] : M → option M := begin
  intro a, by_cases a=1, exact none, exact some a,
end

def g {M : Type u} [has_one M] : option M → M
| none := 1
| (some a) := a

example {M : Type u} [h1 : has_one M] : ∀ (a : M) (h : a = 1), g (f a) = h1.one := begin
  intros a h,
  simp [f],
  sorry,
end

[Alex Meiburg]

Think that pretty much captures it

[Alex Meiburg]

To process option.rec X Y ((λ (a : M), f a) a) = 1 I tried conv mode. First to_lhs and then congr. But the congr only gave me two goals, the X and the Y, and didn't leave me with a goal for the third argument to option.rec (the ((λ (a : M), f a) a)).

[Ruben Van de Velde]

import tactic.split_ifs
universe u

noncomputable def f {M : Type u} [has_one M] : M → option M := begin
  intro a, by_cases a=1, exact none, exact some a,
end

def g {M : Type u} [has_one M] : option M → M
| none := 1
| (some a) := a

example {M : Type u} [h1 : has_one M] : ∀ (a : M) (h : a = 1), g (f a) = h1.one := begin
  intros a h,
  simp [f],
  split_ifs,
  refl,
end

[Ruben Van de Velde]

Or

universe u

noncomputable def f {M : Type u} [has_one M] : M → option M := begin
  intro a, by_cases a=1, exact none, exact some a,
end

def g {M : Type u} [has_one M] : option M → M
| none := 1
| (some a) := a

example {M : Type u} [h1 : has_one M] : ∀ (a : M) (h : a = 1), g (f a) = h1.one := begin
  intros a h,
  simp [f, h, g],
end

[Alex Meiburg]

Ah, right, those do work on my "mwe". I guess that means it's not a very good mwe. :c
Well I would like to directly set up a goal of the form option.rec X Y ((λ (a : M), f a) a) = 1 for a "true" mwe, but then I get an error that

invalid 'option.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  ?m_1

[Alex Meiburg]

Lemme try to set it up better... sorry, and thank you for the help...

[Yakov Pechersky]

Don't make defs using tactics (to first order). The f def can be "fun a, if a = 1 then none else some a".

[Alex Meiburg]

Good to know @Yakov Pechersky , why? Don't tactics get 'compiled down' to a proof term anyway?

[Alex Meiburg]

@Ruben Van de Velde , okay here is an actual functional mwe that gives the same error that I'm actually getting: https://gist.github.com/Timeroot/8fd43e5b58a4f910ad05b098383c788f

[Alex Meiburg]

I have option.rec ... on the left. Given a rec on the left side of the equation, I expected to be able to reduce this to a separate goal for each of the inductive types. But I don't know how to do that.

Alternately, it's option.rec 0 X Y, and 0 is definitionally equal to none, I expect to be able to just reduce that to X. But I don't know how to get option.rec to "evaluate".

Alternately, given that given that Y is of the form (\lambda a, foo a) a, it would be good to beta-reduce that lambda, but I can't get that to happen either.

[Alex Meiburg]

split and split_ifs don't do anything, and I can't seem to force it to turn the 0 into none (but as I understand, I shouldn't have to if it's equivalent underneath?)

[Alex J. Best]

Tactics produce proof terms, but not necessarily very minimal ones so often there is a lot of extra junk in the term generated that makes proving things about a def harder. For lemmas it doesn't matter what the term is however so using tactics isnt ever really a problem there

[Alex Meiburg]

I see, makes sense