Application type mismatch

Stream: new members

[Vincent Beffara]

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]

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]

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

Yes, this is certainly one of the reasons

[Rob Lewis]

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]

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]

@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]

@[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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

See https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

[Vincent Beffara]

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

[Kevin Buzzard]

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

[Vincent Beffara]

See https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

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

[Patrick Massot]

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]

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]

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

[Mauricio Collares]

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]

Thank you @Mauricio Collares That worked!!

[Mike]

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]

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]

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.