Zulip Chat Archive

Stream: new members

Topic: unknown identifier 'mod_fn'


view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 22 2020 at 06:15):

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

view this post on Zulip 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 ?

view this post on Zulip Johan Commelin (Jun 22 2020 at 06:56):

Well, why does this terminate?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 22 2020 at 06:57):

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

view this post on Zulip Johan Commelin (Jun 22 2020 at 06:57):

But for int this is of course not enough.

view this post on Zulip Johan Commelin (Jun 22 2020 at 06:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 22 2020 at 09:49):

@Mukesh Tiwari rw if_neg h\1

view this post on Zulip Johan Commelin (Jun 22 2020 at 09:50):

rwa [if_neg h₁, if_pos h₂]

view this post on Zulip Patrick Massot (Jun 22 2020 at 09:53):

simp [h₁, h₂] should help too

view this post on Zulip 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


view this post on Zulip 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).

view this post on Zulip Scott Morrison (Jun 22 2020 at 10:32):

@Mukesh Tiwari already has this fact as H₃.

view this post on Zulip Scott Morrison (Jun 22 2020 at 10:32):

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

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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))

view this post on Zulip Scott Morrison (Jun 22 2020 at 10:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 22 2020 at 10:35):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jun 23 2020 at 01:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 23 2020 at 03:59):

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

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Jun 23 2020 at 04:00):

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

view this post on Zulip Mario Carneiro (Jun 23 2020 at 04:01):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jun 23 2020 at 04:04):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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