Hi. I was trying to understand how to use `Function`

to convince coq that recursive functions are well-formed.

So I was looking at this example from here:

```
Function log10 (n:Z) {measure Z.abs_nat n} : nat :=
if Zlt_bool n 10 then 0
else 1 + log10 (n/10).
Proof.
intros n H.
```

I guess what this is trying to convince coq that log10 will terminate by saying that `Z.abs_nat n`

will keep getting smaller till reaching a base case.

I got the proof obligation goal at this point as:

```
1 subgoal (ID 84)
n : Z
H : (n <? 10)%Z = false
============================
Z.abs_nat (n / 10) < Z.abs_nat n
```

How can we go about proving this?

(I'm not familiar with proofs on ℤ).

I was thinking something like this:

Since `n<10`

, we can say `n/10 = 0`

.

Then we can get

```
0 < Z.abs-nat n
```

But that can't be true, right?

I mean, what if n is 0?

Any idea what I'm missing here?

Your assumption H implies that n >= 10

Because it literally says that testing if n < 10 returned false. Indeed, if you look at your function, you'll see log10 only calls itself recursively when Zlt_bool n 10 returned false (Zlt_bool n 10 and (n <? 10)%Z seem to be different syntaxes for the same term)

`Search Zlt_bool.`

should find lemmas to reason about your assumption and convert it to 10 <= n.

```
Require Import ZArith Lia.
Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
Goal forall n, (n <? 10)%Z = false -> Z.abs_nat (n / 10) < Z.abs_nat n.
lia.
Qed.
```

Paolo Giarrusso said:

Your assumption H implies that n >= 10

Oh... Sorry. I got that completely wrong.

Laurent Théry said:

`Require Import ZArith Lia. Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. Goal forall n, (n <? 10)%Z = false -> Z.abs_nat (n / 10) < Z.abs_nat n. lia. Qed.`

This didn't work for my. My coq version is 8.12

Is it too old for this?

Julin S said:

Laurent Théry said:

`Require Import ZArith Lia. Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. Goal forall n, (n <? 10)%Z = false -> Z.abs_nat (n / 10) < Z.abs_nat n. lia. Qed.`

This didn't work for my. My coq version is 8.12

Is it too old for this?

I guess it was too old. It worked on coq 8.15

Is using `lia`

like this the only way of doing this? To understand how this proof can progress, is there a more 'manual' way of proving this?

Paolo Giarrusso said:

Your assumption H implies that n >= 10

I could use ` rewrite Z.ltb_ge`

to get `n >= 10`

. Now the goal looks like:

```
n : Z
H : (10 <= n)%Z
============================
Z.abs_nat (n / 10) < Z.abs_nat n
```

How can I proceed from here?

Should I induct on `n`

? Couldn't proceed far with that.

The other tool is learning to use Search (after enabling `Printing Coercions`

, and toggling `Unset Printing Notations`

); and that's necessary for goals that can't be solved with lia (and relatives like nia). For instance, you could try the following strategy (I'm not at a computer):

`Z.abs_nat m = m`

for both of these numbers; use`Search Z.abs_nat`

to find some lemma; use`lia`

to prove that`0 <= n / 10`

and`0 <= n / 10`

- then I'd try to show
`n / 10 < n`

by rewriting to`n / 10 < n / 1`

and using 1 / 10: I'd search for a monotonicity lemma for division.

In general, expected lemmas might be missing and unexpected lemmas might be available, so one might want to change strategy after browsing Search result, or prove new helper lemmas.

Also beware of the N/Z/Nat distinction: many notations are overloaded; lemmas available on the three are similar but not always identical. Some conversions between these types might be coercions (depending on libraries you use), and coercions aren't printed but must still be reasoned about.

Here is a step by step proof

```
Require Import ZArith.
Goal forall n, (n <? 10)%Z = false -> Z.abs_nat (n / 10) < Z.abs_nat n.
intros n Hn.
Search (Z.abs_nat _ < Z.abs_nat _).
apply Zabs_nat_lt; split.
Search (0 <= _ / _)%Z.
- apply Z.div_pos.
Search (_ <= _)%Z "trans".
apply (Z.le_trans 0 10 n).
+ now trivial.
+ Search ((_ <? _)%Z = false).
now apply Z.ltb_ge.
+ now trivial.
- Search (_ / _ < _)%Z.
apply Z.div_lt.
Search (_ < _)%Z "trans".
apply (Z.lt_le_trans 0 10 n).
+ now trivial.
+ now apply Z.ltb_ge.
+ now trivial.
Qed.
```

```
```

Last updated: Jun 14 2024 at 18:01 UTC