CODEWITHSUNDEEP
coq
hamid k
hamid k

Reputation: 511

Destruct if condition in program fixpoint coq

I want to proof the factor function correctness in 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.

after unfold I expected see a if and destruct its condition , but now I see this : 

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)

How I can complete the proof?

Upvotes: 0

Views: 696

Answers (1)

larsr
larsr

Reputation: 5811

Program gives you terms that are difficult to work with, so you should prove a lemma that factor is equal to its body, and then rewrite with that, instead of unfolding. (I used match instead of if to get hold of the dvd proof term.)

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.

When you unfold and rewrite with Fix_eq you get such a horrible goal term to look at that it's best to fold it quickly! :-) It can be handled with reflexivity or auto anyway.

The second goal typically requires algebraic manipulation with omega or similar to show that the LHS equals RHS, but in this case it was sufficient with congruence.

How did I know to use Fix_eq? When I unfolded factor_func I saw it contained Wf.Fix_sub, so I searched for lemmas with Search (Wf.Fix_sub). and found a few.

Now you should continue your proof by rewriting with the lemma:

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.

Now your goal state is

  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)

which probably makes more sense.

Upvotes: 2

Related Questions