Julin S (Feb 24 2023 at 03:02): Julin S (Feb 24 2023 at 03:02):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?
Paolo Giarrusso (Feb 24 2023 at 05:39):Your assumption H implies that n >= 10
Paolo Giarrusso (Feb 24 2023 at 05:43):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)
Paolo Giarrusso (Feb 24 2023 at 05:44):Search Zlt_bool. should find lemmas to reason about your assumption and convert it to 10 <= n.
Laurent Théry (Feb 24 2023 at 07:03):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.
Julin S (Feb 25 2023 at 05:16):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 (Feb 25 2023 at 05:18):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
Julin S (Feb 25 2023 at 05:19):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?
Julin S (Feb 25 2023 at 05:33):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.
Paolo Giarrusso (Feb 25 2023 at 12:38):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 / 10n / 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.
Paolo Giarrusso (Feb 25 2023 at 12:42):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.
Laurent Théry (Feb 25 2023 at 12:56):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: Apr 19 2024 at 15:02 UTC