## Stream: new members

### Topic: Application type mismatch

#### Vincent Beffara (Nov 22 2019 at 13:12):

Hi,

Still trying to figure out how lean works ... so I have a function defined under the condition that some predicate holds on the argument, something like

def good (x : whatever) : Prop := something
def f (x : whatever) (h : good x) := blah


and I would like to rewrite the argument x in f x h, but I get the error [check] application type mismatch at ... stating, if I understand the message correctly, that after rewriting the x to some y, then we would get f y h with h : good x instead of good y. Certainly doing the same rewrite inside of h would make it fit, but if I understand it right, rw only acts at one location at a time.

What is the right way to do this rewrite? Is that what simp only is for? Is that kind of issue the reason why 1/0=0?

#### Vincent Beffara (Nov 22 2019 at 13:13):

OK, more explicit example:

def good (n : ℕ) : Prop := 3 ∣ n
def f (n : ℕ) (h : good n) := n
lemma toto {n : ℕ} : n = n + 1 - 1 := by { norm_num }
example {n : ℕ} (h : good n) : 3 ∣ f n h :=
begin
rw (@toto n),
sorry
end


#### Johan Commelin (Nov 22 2019 at 13:24):

Is that kind of issue the reason why 1/0=0?

Yes, this is certainly one of the reasons

#### Rob Lewis (Nov 22 2019 at 13:24):

This example will work if you revert h before the rewrite. Then both occurrences of n will get rewritten at the same time. But in general, this will be frustrating, and yes it is the reason why 1/0=0.

#### Rob Lewis (Nov 22 2019 at 13:24):

In mathlib we generally prefer to "totalize" f, that is, to give it a default value when good n doesn't hold. Something like

#### Johan Commelin (Nov 22 2019 at 13:24):

@Vincent Beffara It turns out that it is often easier to define your function in such a way that it garbage whenever the input is garbage, instead of defining a partial function

#### Rob Lewis (Nov 22 2019 at 13:24):

@[derive decidable] def good (n : ℕ) : Prop := 3 ∣ n

def f (n : ℕ) : ℕ := if h : good n then n else default _

lemma f_val {n : ℕ} (h : good n) : f n = n := by simp [f, h]

lemma toto {n : ℕ} : n = n + 1 - 1 := by { norm_num }
example {n : ℕ} (h : good n) : 3 ∣ f n :=
begin
rw [(@toto n)] at h ⊢,
sorry
end


#### Johan Commelin (Nov 22 2019 at 13:26):

You only need to check good x on theorems that need it, but not on the function itself.
If you can make the "output garbage" somewhat useful even if the input is garbage, that's even better, because it will allow you to drop some checks of good x. That's the reason why 1/0 = 0 and not 1/0 = 37 even though Kevin would have liked that.

#### Kevin Buzzard (Nov 22 2019 at 13:28):

Here's another trick which is sometimes helpful:

import tactic.norm_num

def good (n : ℕ) : Prop := 3 ∣ n
def f (n : ℕ) (h : good n) := n
lemma toto {n : ℕ} : n = n + 1 - 1 := by { norm_num }
example {n : ℕ} (h : good n) : 3 ∣ f n h :=
begin
have : 3 ∣ f (n + 1 - 1) h, sorry,
convert this,
end


#### Kevin Buzzard (Nov 22 2019 at 13:29):

toto is true by rfl but had this not been the case, the goal would have changed to n = n + 1 - 1. Possibly.

#### Vincent Beffara (Nov 22 2019 at 16:16):

This example will work if you revert h before the rewrite. Then both occurrences of n will get rewritten at the same time. But in general, this will be frustrating, and yes it is the reason why 1/0=0.

Ah, that is nice to know. So how can I tell whether rw will rewrite the first occurrence of n or all of them at once?

And a related question, if the h is not part of my environment but a field in some structure somewhere (and the n is in another field of the same structure), does all that mean that I will have to deconstruct the whole structure before I can apply rw then?

#### Kevin Buzzard (Nov 22 2019 at 16:17):

You only need to check good x on theorems that need it, but not on the function itself.
If you can make the "output garbage" somewhat useful even if the input is garbage, that's even better, because it will allow you to drop some checks of good x. That's the reason why 1/0 = 0 and not 1/0 = 37 even though Kevin would have liked that.

It's morally dishonest to prove theorems about junk.

#### Kevin Buzzard (Nov 22 2019 at 16:18):

You can target which ns rw will rewrite, it's somewhat arcane but it's possible.

#### Vincent Beffara (Nov 22 2019 at 16:19):

Is it arcane even if I want to target "all the ns even those hidden in assumptions that show up as _"?

#### Kevin Buzzard (Nov 22 2019 at 16:20):

I just usually proceed by trial and error :-/ I try rw, erw, simp only and then I ask here :D

#### Vincent Beffara (Nov 22 2019 at 16:21):

Feels a bit brittle to navigate through the expression and tag all the occurrences one by one ...

#### Patrick Massot (Nov 22 2019 at 16:36):

The slightly confusing rule is: rw rewrites every occurrence but it has to be the exact same rewriting. For instance, if your goal contains ((a+b)+ (c+d)) + (a + b), rw add_comm will perform only one rewrite, although there are five additions, because it will see the outermost addition (second to last one in left to right order), specialize the add_comm lemma to add_comm ((a+b)+(c+d)) (a+b) and perform all rewrite using that specialized lemma. On the other hand rw add_comm a b will perform two rewriting, because that specific lemma matches two subterms in the goal.

Last updated: May 17 2021 at 23:14 UTC