在 coq 的 then 部分中使用 if expression = true 的证明

对于所有 1

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.

如何在 if 的 then 部分使用 (b|a) 的证明？

Program记得这类信息。如果您在所需的证明处留下下划线，系统可以自行计算出来。

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.

此时你需要做的就是证明你的测量值减小了，这并不难。