unknown identifier 'mod_fn'

Stream: new members

[Mukesh Tiwari]

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]

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]

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

[Mukesh Tiwari]

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

Well, why does this terminate?

[Johan Commelin]

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]

So in that case have i < n, from sorry will help.

[Johan Commelin]

But for int this is of course not enough.

[Johan Commelin]

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

[Mukesh Tiwari]

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

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]

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]

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

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

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]

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

@Mukesh Tiwari rw if_neg h\1

[Johan Commelin]

rwa [if_neg h₁, if_pos h₂]

[Patrick Massot]

simp [h₁, h₂] should help too

[Mukesh Tiwari]

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]

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]

@Mukesh Tiwari already has this fact as H₃.

[Scott Morrison]

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

[Kevin Buzzard]

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]

That is, rather than using specialize and a have as a previous tactic, you'll need to write something like:

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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

[Mukesh Tiwari]

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]

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]

Unfortunately there's a difference between tactic mode have and term mode have here.

[Scott Morrison]

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

[Scott Morrison]

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

[Mukesh Tiwari]

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]

Every time you write := ..., or exact ... you're back in term mode.

[Scott Morrison]

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]

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

[Mario Carneiro]

I usually do the have's right at the start of the proof

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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