# Zulip Chat Archive

## Stream: new members

### Topic: unknown identifier 'mod_fn'

#### Mukesh Tiwari (Jun 22 2020 at 06:13):

Hi everyone, I am getting unknown identifier for the function definition. Any idea how to resolve, and may be a better way to write it?

```
def mod_fn (addr p : int) : int :=
ite (p <= 0)
0
(ite (0 <= addr)
(ite (addr < p)
addr
(mod_fn (addr - p) p))
(mod_fn (addr + p) p))
```

#### Johan Commelin (Jun 22 2020 at 06:14):

You are trying to define a function by recursion. But you can't do that without explaining to lean why this will terminate.

#### Johan Commelin (Jun 22 2020 at 06:15):

You might want to take a look at how this is defined in mathlib

#### Mukesh Tiwari (Jun 22 2020 at 06:50):

@Johan Commelin Thanks for your answer. I could not understand zmod in src/data/zmod/basic.lean. However, I looked at the gcd in data/int/gcd.lean and followed the similar strategy, but the typechecker is still not happy.

```
def mod_fn : int → int → int
| addr p :=
if h₁ : p <= 0 then
0
else
if h₂ : addr >= 0 then
if h₃ : addr < p then
addr
else
have addr - p < addr, from sorry,
mod_fn (addr - p) p
else
have addr + p < addr, from sorry,
mod_fn (addr + p) p
```

Do you think it's because of sorry ?

#### Johan Commelin (Jun 22 2020 at 06:56):

Well, why does this terminate?

#### Johan Commelin (Jun 22 2020 at 06:57):

If you are working with `nat`

s, then calling a function with an argument that is becoming smaller is sufficient proof that it's terminating.

#### Johan Commelin (Jun 22 2020 at 06:57):

So in that case `have i < n, from sorry`

will help.

#### Johan Commelin (Jun 22 2020 at 06:57):

But for `int`

this is of course not enough.

#### Johan Commelin (Jun 22 2020 at 06:58):

@Mukesh Tiwari You might want to try to define the function for `nat`

first.

#### Mukesh Tiwari (Jun 22 2020 at 07:37):

@Johan Commelin Now, I see you point. I have written the nat version and typechecker is happy about it.

```
def mod_nat : nat → nat → nat
| addr p :=
if h₁ : p = 0 then
0
else
if h₂ : addr < p then
addr
else
have addr - p < addr, by omega,
mod_nat (addr - p) p
```

So, the typechecker is not convinced that the integer definition would reach to a value between 0 and p, [0, p).

```
def mod_fn : int → int → int
| addr p :=
if h₁ : p <= 0 then
0
else
have h₄ : p > 0, by omega,
if h₂ : addr >= 0 then
if h₃ : addr < p then
addr
else
have addr >= p, by omega,
have (addr - p) < addr, by omega,
have (addr - p) >= 0, by omega,
mod_fn (addr - p) p
else
have h₅ : addr < 0, by omega,
have (addr + p) > addr, by omega,
have (addr + p) < p, by omega,
mod_fn (addr + p) p
```

Can you give me some more hint (a concrete input) that why this function would not terminate? Thank you very much for you help.

#### Johan Commelin (Jun 22 2020 at 07:42):

As you've discovered, "well founded recursion" on `nat`

is a lot easier than on `int`

. Because `<`

is not a well founded relation on `int`

.

To define the `int`

version, I would define something without recursion, by using the `nat`

version.

#### Johan Commelin (Jun 22 2020 at 07:43):

If you really want to use recursion for the `int`

version, you would have to add a complicated proof of termination. (I've never done something like that myself...)

#### Mukesh Tiwari (Jun 22 2020 at 08:43):

@Johan Commelin Now, I am trying to prove the following lemma for my mod_nat, but when I am unfold the definition,

I get this error: deep recursion was detected at 'expression replacer' (potential solution: increase stack space in your system)

```
lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < p
| addr p :=
if h₁ : p = 0 then
begin
intros, rw h₁ at a, exact (mul_lt_mul_right a).mp a,
end
else
if h₂ : addr < p then
begin
intros,
/- why I can not unfold the definitnon
deep recursion was detected at 'expression replacer'
(potential solution: increase stack space in your system)-/
unfold mod_nat, sorry
end
else
begin
intros,
have H₁ : addr >= p := by exact not_lt.mp h₂,
have H₂ : addr - p >= 0 := by exact bot_le,
specialize (mod_nat_proof (addr - p) p a),
unfold mod_nat, sorry
end
```

#### Johan Commelin (Jun 22 2020 at 09:11):

@Mukesh Tiwari Does `rw mod_nat`

work? If not, you can use `show`

to tell lean what you want the goal to look like.

#### Scott Morrison (Jun 22 2020 at 09:33):

I wouldn't advise this (usually best to avoid `unfold`

in favour of `rw`

and `simp`

whenever possible), but `unfold`

does have a `{single_pass := tt}`

configuration option that should at least let you see what is exploding.

#### Mukesh Tiwari (Jun 22 2020 at 09:46):

@Johan Commelin Thanks again. Now, given that h₁ : ¬p = 0, I want to evaluate the second branch of ite. How can I do that?

```
1 goal
mod_nat_proof : ∀ (addr p : ℕ), p > 0 → mod_nat addr p < p,
addr p : ℕ,
h₁ : ¬p = 0,
h₂ : addr < p,
a : p > 0
⊢ ite (p = 0) 0 (ite (addr < p) addr (mod_nat (addr - p) p)) < p
```

@Scott Morrison Thank you very much.

#### Johan Commelin (Jun 22 2020 at 09:49):

@Mukesh Tiwari `rw if_neg h\1`

#### Johan Commelin (Jun 22 2020 at 09:50):

`rwa [if_neg h₁, if_pos h₂]`

#### Patrick Massot (Jun 22 2020 at 09:53):

`simp [h₁, h₂]`

should help too

#### Mukesh Tiwari (Jun 22 2020 at 10:24):

Finally, I have finished the proof according to my definition of mod_nat, but it seems that typechecker is not happy about it.

```
lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < p
| addr p :=
if h₁ : p = 0 then
begin
intros, rw h₁ at a, exact (mul_lt_mul_right a).mp a,
end
else
if h₂ : addr < p then
begin
intros, rw mod_nat,
rwa [if_neg h₁, if_pos h₂]
end
else
begin
intro a,
have H₁ : addr >= p := by exact not_lt.mp h₂,
have H₂ : addr - p >= 0 := by exact bot_le,
have H₃ : addr - p < addr := by exact nat.sub_lt_of_pos_le p addr a H₁,
specialize (mod_nat_proof (addr - p) p a),
rw mod_nat, rwa [if_neg h₁, if_neg h₂],
end
```
```

failed to prove recursive application is decreasing, well founded relation

@has_well_founded.r (Σ' (addr : ℕ), ℕ)

(@psigma.has_well_founded ℕ (λ (addr : ℕ), ℕ) (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)

(λ (a : ℕ), @has_well_founded_of_has_sizeof ℕ nat.has_sizeof))

Possible solutions:

- Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.

- The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.

The nested exception contains the failure state for the decreasing tactic.

nested exception message:

failed

state:

mod_nat_proof : ∀ (_p : Σ' (addr : ℕ), ℕ), _p.snd > 0 → mod_nat _p.fst _p.snd < _p.snd,

addr p : ℕ,

h₁ : ¬p = 0,

h₂ : ¬addr < p,

a : p > 0

⊢ addr - p < addr

```
```

def mod_nat : nat → nat → nat

| addr p :=

if h₁ : p = 0 then

0

else

if h₂ : addr < p then

addr

else

have addr - p < addr, by omega,

mod_nat (addr - p) p

```
```

#### Kevin Buzzard (Jun 22 2020 at 10:30):

The error message says that Lean cannot literally see a proof of `addr - p < addr`

in your list of hypotheses, and suggests that you add it by proving it yourself using the `have`

command. If you're using mathlib you might be able to just insert `have h3 : addr - p < addr, by linarith`

at some appropriate point (or `by omega`

).

#### Scott Morrison (Jun 22 2020 at 10:32):

@Mukesh Tiwari already has this fact as `H₃`

.

#### Scott Morrison (Jun 22 2020 at 10:32):

Unfortunately, he needs to switch to a "term mode" have, before Lean can see it.

#### Kevin Buzzard (Jun 22 2020 at 10:32):

```
failed
state:
mod_nat_proof : ∀ (_p : Σ' (addr : ℕ), ℕ), _p.snd > 0 → mod_nat _p.fst _p.snd < _p.snd,
addr p : ℕ,
h₁ : ¬p = 0,
h₂ : ¬addr < p,
a : p > 0
⊢ addr - p < addr
```

Then it maybe needs to be moved?

#### Scott Morrison (Jun 22 2020 at 10:33):

That is, rather than using `specialize`

and a `have`

as a previous tactic, you'll need to write something like:

#### Scott Morrison (Jun 22 2020 at 10:34):

```
have foo := (have H₃ : addr - p < addr := by exact nat.sub_lt_of_pos_le p addr a H₁, (mod_nat_proof (addr - p) p a))
```

#### Scott Morrison (Jun 22 2020 at 10:34):

(there isn't a #mwe, so I can't test this for you)

#### Scott Morrison (Jun 22 2020 at 10:35):

I guess cleaner would be to still construct the value of H3 in tactic mode, just "make it available again" in term mode when you do the recursive call.

#### Scott Morrison (Jun 22 2020 at 10:35):

I'm terrible at the syntax for term mode have, so I won't try to get this right. But if you don't understand what I'm saying, or can't make it work, post a #mwe and I'll have a go.

#### Scott Morrison (Jun 22 2020 at 10:35):

You're basically just a syntactical change away from having it working now.

#### Mukesh Tiwari (Jun 22 2020 at 11:49):

Scott Morrison said:

I'm terrible at the syntax for term mode have, so I won't try to get this right. But if you don't understand what I'm saying, or can't make it work, post a #mwe and I'll have a go.

I have not tried it yet, but I have posted a gist https://gist.github.com/mukeshtiwari/4ed2d76a3994a62575865c8d1944b651, which should be compilable (typecheckable) in Lean.

#### Scott Morrison (Jun 23 2020 at 01:44):

Replace your final `begin ... end`

block with

```
begin
intro a,
have H₁ : addr >= p := by exact not_lt.mp h₂,
have H₂ : addr - p >= 0 := by exact bot_le,
have := have H₃ : addr - p < addr, from nat.sub_lt_of_pos_le p addr a H₁, mod_nat_proof (addr - p) p a,
rw mod_nat, rwa [if_neg h₁, if_neg h₂],
end
```

#### Scott Morrison (Jun 23 2020 at 01:45):

Unfortunately there's a difference between tactic mode `have`

and term mode `have`

here.

#### Scott Morrison (Jun 23 2020 at 01:45):

Lean's automatic reasoning about decreasing recursive calls only sees facts put to it in "term mode" have statements.

#### Scott Morrison (Jun 23 2020 at 01:46):

I'm not sure if this would be fixable by a language change. I wish it were.

#### Mukesh Tiwari (Jun 23 2020 at 03:48):

Scott Morrison said:

Unfortunately there's a difference between tactic mode

`have`

and term mode`have`

here.

Thanks for the answer, but how do you differentiate between those two? My understanding is: when you start begin .... end block, then every thing between begin and end is in tactic mode (am I right?). Since typechecker can only see the decreasing recursive call in "term" mode, I need to escape the tactic mode? Hopefully, enough practice would give insights about these kind of details.

#### Scott Morrison (Jun 23 2020 at 03:59):

Every time you write `:= ...`

, or `exact ...`

you're back in term mode.

#### Scott Morrison (Jun 23 2020 at 04:00):

So in the example I wrote for you above, in the ugly `have := have H3 : ..., from`

the first `have`

is a tactic-mode have, but the second is a term-mode have!

#### Scott Morrison (Jun 23 2020 at 04:00):

I'm sure there are more colloquial ways to write this...

#### Mario Carneiro (Jun 23 2020 at 04:01):

I usually do the `have`

's right at the start of the proof

#### Mario Carneiro (Jun 23 2020 at 04:02):

You can also use a lambda instead, I think (if you don't want to prove the decrease theorem immediately)

#### Mario Carneiro (Jun 23 2020 at 04:04):

I would demonstrate but I can't find an #mwe on the thread

#### Mario Carneiro (Jun 23 2020 at 04:05):

Oh, here's an MWE with Scott's version:

```
import tactic
def mod_nat : nat → nat → nat
| addr p :=
if h₁ : p = 0 then
0
else
if h₂ : addr < p then
addr
else
have addr - p < addr, by omega,
mod_nat (addr - p) p
lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < p
| addr p :=
if h₁ : p = 0 then
begin
intros, rw h₁ at a, exact (mul_lt_mul_right a).mp a,
end
else
if h₂ : addr < p then
begin
intros, rw mod_nat,
rwa [if_neg h₁, if_pos h₂]
end
else
begin
intro a,
have H₁ : addr >= p := by exact not_lt.mp h₂,
have H₂ : addr - p >= 0 := by exact bot_le,
have := have H₃ : addr - p < addr, from nat.sub_lt_of_pos_le p addr a H₁, mod_nat_proof (addr - p) p a,
rw mod_nat, rwa [if_neg h₁, if_neg h₂],
end
```

#### Mario Carneiro (Jun 23 2020 at 04:08):

Here is with a lambda:

```
begin
have IH := λ H₃ : addr - p < addr, mod_nat_proof (addr - p) p,
intro a,
have H₁ : addr >= p := by exact not_lt.mp h₂,
have H₂ : addr - p >= 0 := by exact bot_le,
have := IH (nat.sub_lt_of_pos_le p addr a H₁) a,
rw mod_nat, rwa [if_neg h₁, if_neg h₂],
end
```

#### Mario Carneiro (Jun 23 2020 at 04:15):

After compression I get this:

```
lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < p
| addr p := λ p0, begin
rw mod_nat, split_ifs with h₁ h₂; try {assumption},
apply λ a (H₃ : a < addr), mod_nat_proof a p p0,
exact nat.sub_lt_self (by linarith) p0,
end
```

Last updated: May 12 2021 at 23:13 UTC