## 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.

#### Mike (Nov 17 2023 at 14:42):

I'm working my way through Theorem Proving in Lean4. In the Other Recursive Data Types section I'm trying to follow along in Visual Studio.

However, this code

import Mathlib

namespace Hidden
universe u
variable (α : Type u)

inductive List (α : Type u) where
| nil : List α
| cons : α → List α → List α

namespace List

def append (as bs : List α) : List α :=
match as with
| nil => bs
| cons a as => cons a (append as bs)

theorem nil_append (as : List α) : append nil as = as :=
rfl

theorem cons_append (a : α) (as bs : List α)
: append (cons a as) bs = cons a (append as bs) :=
rfl

end List


which is mostly copied from the tutorial gives a few syntax errors:

in

theorem nil_append (as : List α) : append nil as = as :=
rfl


the nil is underlined in red with the error message

application type mismatch
append nil
argument
nil
has type
List ?m.6804 : Type ?u.6803
but is expected to have type
Type ?u.6802 : Type (?u.6802 + 1)


and then in

theorem cons_append (a : α) (as bs : List α)
: append (cons a as) bs = cons a (append as bs) :=
rfl


cons a as
and
as in append as bs
give the following errors:

application type mismatch
append (cons a as)
argument
cons a as
has type
List α : Type u
but is expected to have type
Type ?u.508830 : Type (?u.508830 + 1)


and

application type mismatch
append as
argument
as
has type
List α : Type u
but is expected to have type
Type ?u.675344 : Type (?u.675344 + 1)


Anyone know what's going on here and how to fix the sytax errors?

#### Mauricio Collares (Nov 17 2023 at 14:50):

The variable is declared as explicit. You can change it to variable {α : Type u} and it will probably help.

#### Mauricio Collares (Nov 17 2023 at 14:53):

Note that if you're outside Mathlib and you don't declare the variable at all, it gets automatically declared as implicit. If you are inside Mathlib, you can do set_option autoImplicit true to revert to vanilla Lean behaviour (but be aware that typos can be very confusing if you don't pay attention to the syntax highlighting colours).

#### Mike (Nov 17 2023 at 15:20):

Thank you @Mauricio Collares That worked!!

#### Mike (Nov 17 2023 at 15:44):

In the next section, I'm getting a new syntax error in a definition:

inductive BinaryTree where
| leaf : BinaryTree
| node : BinaryTree → BinaryTree → BinaryTree


in the last line  | node : BinaryTree → BinaryTree → BinaryTree, the third BinaryTree is underlined in red with this error message:

function expected at
BinaryTree
term has type
Sort ?u.7194


Anyone have an idea of what's going on here?

#### Richard Copley (Nov 17 2023 at 15:48):

Click on the "Launch in Lean 4 playground" icon on your quoted Lean code. You will see that it contains no error.
But now try the same thing with this:

inductive BinaryTree where
| leaf : BinaryTree
| node : BinaryTree → BinaryTree → BinaryTree
sorry


There's a token whose indentation is such that it is being treated as an argument to 'BinarySearch', which requires no arguments.

#### Mike (Nov 17 2023 at 15:58):

Thanks @Richard Copley ! I have no idea what was happening. The error went away after a little while. I will have to be more careful about indentation.

Last updated: Dec 20 2023 at 11:08 UTC