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


#### 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
if h₁ : p <= 0 then
0
else
if h₂ : addr >= 0 then
if h₃ : addr < p then
else
else


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 nats, 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
if h₁ : p = 0 then
0
else
if h₂ : addr < p then
else


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
if h₁ : p <= 0 then
0
else
have h₄ : p > 0, by omega,
if h₂ : addr >= 0 then
if h₃ : addr < p then
else
have addr >= p, by omega,
have (addr - p) >= 0, by omega,
else
have h₅ : addr < 0, by omega,
have (addr + p) < p, by omega,


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
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,
h₁ : ¬p = 0,
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
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,
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,
h₁ : ¬p = 0,
a : p > 0




def mod_nat : nat → nat → nat
if h₁ : p = 0 then
0
else
if h₂ : addr < p then
else




#### 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,
h₁ : ¬p = 0,
a : p > 0


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,
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
if h₁ : p = 0 then
0
else
if h₂ : addr < p then
else

lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < 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,
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
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