程序定点代码中的析构IF条件 [英] Destruct if condition in program fixpoint coq

问题描述

我想证明Use proof of if expression = true in then part 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 1+factor (a/b) b (divgt0 a b agt0 bgt1 _)  bgt1 
  else 0.
Next Obligation.
  assert ( 0 < a / b < a ).
  apply Zdivide_Zdiv_lt_pos.
  auto.
  auto.
  auto.
  apply Zabs_nat_lt.
  omega.
Qed.

Lemma factor_div ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) : (b ^ (factor a b agt0 bgt1) | a).
Proof.
  unfold factor.

展开后，我预计会看到一个if并破坏它的条件，但现在我看到了这个：

1 subgoal
a, b : Z
agt0 : 0 < a
bgt1 : 1 < b
______________________________________(1/1)
(b
 ^ factor_func
     (existT (fun a0 : Z => {b0 : Z & {_ : 0 < a0 & 1 < b0}}) a
        (existT (fun b0 : Z => {_ : 0 < a & 1 < b0}) b
           (existT (fun _ : 0 < a => 1 < b) agt0 bgt1))) | a)

如何填写证明？

推荐答案

Program给出了难以使用的术语，因此您应该证明一个factor等于其正文的引理，然后用它重写，而不是展开。(我使用match而不是if来获取dvd证明术语。)

Lemma factor_lemma a b agt0 bgt1:
  factor a b agt0 bgt1 =
  match Zdivide_dec b a with
  | left dvd => 1+factor (a/b) b (divgt0 a b agt0 bgt1 dvd)  bgt1
  | right notdvd =>  0 end.
Proof.
  unfold factor at 1.
  unfold factor_func; rewrite Program.Wf.Fix_eq; fold factor_func.
  - reflexivity.
  - intros.
    destruct Zdivide_dec; auto.
    congruence.
Qed.

当您使用Fix_eq展开和重写时，您会看到一个如此糟糕的目标术语，因此最好尽快将其折叠！：-)无论如何都可以使用reflexivity或auto来处理它。

第二个目标通常需要使用omega或类似的代数操作来证明LHS等于RHS，但在这种情况下，使用congruence就足够了。

我怎么知道要使用Fix_eq？当我打开factor_func时，我看到它包含Wf.Fix_sub，所以我搜索了带有Search (Wf.Fix_sub).的词条，并找到了几个。

现在您应该使用引理重写您的证明：

Lemma factor_div ( a b : Z ) ( agt0 : 0 < a ) ( bgt1 : 1 < b ) : (b ^ (factor a b agt0 bgt1) | a).
Proof.
  rewrite factor_lemma.
  destruct Zdivide_dec.

  2:   now rewrite Z.pow_0_r;apply Z.divide_1_l.

现在您的目标状态为

  a, b : Z
  agt0 : 0 < a
  bgt1 : 1 < b
  d : (b | a)
  ============================
  (b ^ (1 + factor (a / b) b (divgt0 a b agt0 bgt1 d) bgt1) | a)

这可能更有意义。

这篇关于程序定点代码中的析构IF条件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！