Apply theorem to subexpression

Stream: general

[David Richey]

In a previous thread, I was suggested the following way to prove this theorem, which works perfectly:

import data.pfun
theorem foo {α β : Type*} {f : α →. β} {x y} : f x = part.some y ↔ ∃ev, f.fn x ev = y :=
begin
  exact part.eq_some_iff,
end

however, I really want f x = part.some y ↔ ∃ev, y = f.fn x ev (notice that this is y = ... instead of ... = y). Upon making this change, I can no longer use exact part.eq_some_iff. I think I could use something like eq.symm to first change it to the form eq_some_iff expects, but I cannot figure out how.

Does anyone have any suggestions?

[David Richey]

Also, to be honest, I do not really understand why part.eq_some_iff is applicable in the first place either... It says o = part.some a ↔ a ∈ o which doesn't look exactly like what I'm trying to prove. Is there multiple steps going on somehow?

[Eric Wieser]

Regarding your last question, It's just unfolding the definition of docs#part.has_mem

[David Richey]

Thanks, I guess it is also implicitly using pfun.fn_apply? I thought exact would only apply if the goal were exactly the same. How can I know what it is really doing under the hood?

[Eric Rodriguez]

exact is the same up to definitional equality, if you know what that means

[David Richey]

ah, I see now. It is not using pfun.fn_apply but pfun.fn. So two defs, makes sense in the context of definitional equality

[David Richey]

thanks for your help with that second question! I derailed us from the original question though, oops. I think it is probably quite simple, but I just can't seem to write the right thing

[Yakov Pechersky]

Your original question might involve docs#eq_comm

[David Richey]

I agree, I'm just not sure how to tell it which subexpression to apply the rewrite to. For example, if I do rewrite eq_comm, I get

⊢ part.some y = f x ↔ ∃ (ev : f.dom x), y = f.fn x ev

but now I have part.some y = f x on the left which is just as bad

[David Richey]

oh, actually, it only did the first occurrence, not both occurrences

[Yakov Pechersky]

"simp_rw @eq_comm _ y" might work

[David Richey]

that does indeed work. I also found conv, and I'm working to understand how I can use it in this case. Is there a way to navigate into an existential in conv mode?

[Eric Wieser]

conv in (∃ x, _) { sorry } perhaps

[David Richey]

hmmm doesn't seem to work unfortunately

theorem foo {α β : Type*} {f : α →. β} {x y} : f x = part.some y ↔ ∃ev, y = f.fn x ev :=
begin
  conv in (∃ev, _) {
    rewrite eq_comm,
  },
  exact part.eq_some_iff,
end

gives find converter failed, pattern was not found

[David Richey]

that gave me the idea to try conv in (y = _), but then doing rewrite eq_comm in that gives

exact tactic failed, type mismatch, given expression has type
  (λ (_a : Prop), y = f.fn x h = _a) (f.fn x h = y)
but is expected to have type
  y = f.fn x h ↔ f.fn x h = y

and I'm not quite sure what that's saying

[Julian Berman]

This seems to do it:

import data.pfun
theorem foo {α β : Type*} {f : α →. β} {x y} : f x = part.some y ↔ ∃ev, y = f.fn x ev :=
begin
  conv_rhs {
    congr,
    funext,
    rw eq_comm,
  },
  exact part.eq_some_iff,
end

I can't say I know what I'm doing in conv mode though I just looked up some previous example here from Zulip and copied it. simp_rw seems easier to use I think.

[Julian Berman]

(You can do it with the conv in thing Eric showed as well, the trick was using congr and funext to again jump inside the binder I think)

[Mario Carneiro]

If I can #xy your question, why do you want this theorem? You should just be able to use the original one by applying .symm whenever you need the equality

[Mario Carneiro]

Anyway you can prove this version too using defeq tricks

theorem foo {α β : Type*} {f : α →. β} {x y} : f x = part.some y ↔ ∃ev, y = f.fn x ev :=
part.eq_some_iff.trans $ exists_congr $ λ _, eq_comm

[David Richey]

thank you for the suggestions! @Mario Carneiro I ultimately wanted this theorem to do a rewrite from y to f.fn x ev. I can of course just rewrite in the other direction (which is what I ended up doing), but I'm also just taking my time and exploring rabbit holes as I come across them :)

This is what I actually ended up with (absolutely open to comments if you have any!)

import data.pfun

inductive iarith
| var : string -> iarith

inductive iarith_big_steps : iarith → (string →. int) → int → Prop
| abs_var {σ v h} : iarith_big_steps (iarith.var v) σ (σ.fn v h)

theorem store_bound_imp_var_bound {σ : string →. int} {v n} (h : σ v = part.some n) : iarith_big_steps (iarith.var v) σ n :=
begin
  have exists_ev : ∃ev, σ.fn v ev = n, by exact part.eq_some_iff.mp h,
  cases exists_ev with _ apply_is_n,
  rewrite ←apply_is_n,
  apply iarith_big_steps.abs_var,
end

[Mario Carneiro]

indeed, I would write that as

theorem store_bound_imp_var_bound {σ : string →. int} {v n} (h : σ v = part.some n) : iarith_big_steps (iarith.var v) σ n :=
begin
  rcases part.eq_some_iff.1 h with ⟨a, rfl⟩,
  apply iarith_big_steps.abs_var,
end

[David Richey]

haha I will have to look into rcases!

[Mario Carneiro]

or even better

theorem store_bound_imp_var_bound {σ : string →. int} {v n} (h : n ∈ σ v) : iarith_big_steps (iarith.var v) σ n :=
begin
  rcases h with ⟨a, rfl⟩,
  apply iarith_big_steps.abs_var,
end

[Mario Carneiro]

you might also consider writing the inductive type this way instead of using fn / get

inductive iarith_big_steps : iarith → (string →. int) → int → Prop
| abs_var {σ : string →. int} {v n} : n ∈ σ v → iarith_big_steps (iarith.var v) σ n

[David Richey]

reading the docs for rcases, picking out the relevant parts...

An rcases pattern has the following grammar:

• A name like x, which names the active hypothesis as x.
• The keyword rfl, which expects the hypothesis to be h : a = b, and calls subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).
• A tuple pattern ⟨p1, p2, p3⟩, which matches a constructor with many arguments, or a series of nested conjunctions or existentials. For example if the active hypothesis is a ∧ b ∧ c, then the conjunction will be destructured, and p1 will be matched against a, p2 against b and so on.

So would it be correct to say that rcases part.eq_some_iff.1 h with ⟨_, rfl⟩ is shorthand for cases part.eq_some_iff.1 h with _ h1, subst h1?

(by the way, I couldn't get your second rcases example to compile)

[Mario Carneiro]

you probably missed that I changed the signature of the theorem in the second example

[David Richey]

I did indeed

[Mario Carneiro]

and yes your desugaring example is correct

[David Richey]

and here what is the "constructor with many arguments" that the tuple pattern is matching?

[Mario Carneiro]

exists

[Mario Carneiro]

src#Exists

[David Richey]

thank you very much, Mario, you've been a really great help :)