Use proof of if expression = true in then part coq

Question

Forall 1 <= a and 2 <= b exists k that (b^k) divide a but (b^(k+1)) do not divide a ; And I want to calculate k in coq:

Require Import ZArith Znumtheory.

Local Open Scope Z_scope.


Require Coq.Program.Tactics.
Require Coq.Program.Wf.

Lemma divgt0 ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) (dvd : (b|a) ) : 0<a/b.
Proof.
  apply Zdivide_Zdiv_lt_pos.
  auto.
  auto.
  auto.
Qed.

Program Fixpoint factor ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) {measure (Z.abs_nat a)} := 
  if Zdivide_dec b a 
  then factor (a/b) b (divgt0 a b agt0 bgt1 (Zdivide_dec b a))  bgt1 
  else 0.
Next Obligation.

How I can use proof of (b|a) in then part of the if?

Answer 1

Program remembers that kind of information. If you leave an underscore in place of the needed proof, the system can figure it out on its own.

Program Fixpoint factor ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) {measure (Z.abs_nat a)} := 
  if Zdivide_dec b a 
  then factor (a/b) b (divgt0 a b agt0 bgt1 _)  bgt1 
  else 0.                                (* ^ here *)
Next Obligation.

At this point all you need to do is to prove that your measure decreases, which is not hard.