在部分coq中使用if expression = true的证明 [英] Use proof of if expression = true in then part coq

问题描述

Forall 1< = a和2< = b存在k（b ^ k）除a但（b ^（k + 1））不除a的k;我想计算coq中的k：

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.

如何在if的一部分中使用（b | a）的证明？

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

推荐答案

程序会记住此类信息。如果您将下划线代替所需的证明，则系统可以自行解决。

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.

这篇关于在部分coq中使用if expression = true的证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！