7
$\begingroup$

I want to verify a program written in C. I am using Jessie to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions.

Unfortunately Jessie generates no fixpoint definitions and unfortunately I must use these generated definitions to verify a program.

For example the power function:

Require Export ZArith.
Open Scope Z_scope.

  (*Generated by Jessie from my C program*) 
Definition pow : Z->Z->Z.
Admitted.

Definition eq_int_bool : Z -> Z -> bool.
Admitted.

Lemma eq_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((eq_int_bool x y) = true <-> x = y))).
Admitted.

Lemma _jc_axiom_sum : 
    forall (b:Z),
    forall (e:Z), (pow b e) = 
    if (eq_int_bool e 0) then (1)
    else (b * pow b (e-1)).
Admitted.

How can I use the inductive tactics provided in Coq, if I want to prove some features? What can I do in this situation to prove the features? Is it even possible to perform some “complicated” proofs with this sort of definition? In my Coq proofs I can use all I want, including fixpoint definitions.

$\endgroup$
  • $\begingroup$ If you want to use facts without proving them, may I suggest that you use Hypothesis and Variable instead of stating things and then admitting them. Or is this what Jessie did? Who is Jessie? $\endgroup$ – Andrej Bauer Apr 18 '12 at 19:12
7
$\begingroup$

You have an equational specification of the power function. You can prove that it's equivalent to some recursively defined function, in that it has the same values whenever the two functions are passed equal arguments. This is called extensional equality of the two functions.

There is a Zpower function in the standard library, defined recursively:

Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
  match n with
    | xH => f x
    | xO n' => iter_pos n' A f (iter_pos n' A f x)
    | xI n' => f (iter_pos n' A f (iter_pos n' A f x))
  end.
Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
Definition Zpower (x y:Z) :=
    match y with
      | Zpos p => Zpower_pos x p
      | Z0 => 1
      | Zneg p => 0
    end.

Here's a quick-and-dirty proof that your function is equal to Zpower for nonnegative exponents.

Lemma neq_int_bool : forall x y, eq_int_bool x y = false <-> x <> y.
Proof.
  intros.
  pose (A := eq_int_bool_axiom x y); clearbody A.
  split; intros.
  intro E; apply <- A in E. assert (false = true); solve [eauto with bool].
  case_eq (eq_int_bool x y); intro E.
  apply -> A in E. elimtype False. solve [auto with bool].
  reflexivity.
Qed.

Lemma pow_x_0 : forall b, pow b 0 = 1.
Proof.
  intros; rewrite _jc_axiom_sum.
  replace (eq_int_bool 0 0) with true. reflexivity.
  symmetry. apply <- eq_int_bool_axiom. reflexivity.
Qed.

Lemma pow_nat_is_power :
  forall b n, pow b (Z_of_nat n) = Zpower b (Z_of_nat n).
Proof.
  induction n; simpl.
  apply pow_x_0.
  rewrite _jc_axiom_sum.
  replace (eq_int_bool (Zpos (P_of_succ_nat n)) 0) with false.
  replace (Zpos (P_of_succ_nat n) - 1) with (Z_of_nat n).
  rewrite IHn; clear IHn.
  rewrite Zpower_pos_nat. rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
  replace (S n) with (1 + n)%nat. 2: solve [auto with arith].
  rewrite Zpower_nat_is_exp.
  unfold Zpower_nat at 1; simpl.
  replace (b * 1) with b. 2: solve [auto with zarith]. f_equal.
  destruct n; simpl.
  reflexivity.
  rewrite Zpower_pos_nat. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. reflexivity.
  rewrite Zpos_P_of_succ_nat. solve [auto with zarith].
  symmetry. apply <- neq_int_bool. intro; discriminate.
Qed.

What about negative exponents? Your function is underspecified; you may want to try to coerce a more precise specification out of Jessie. One possibility is that pow b e = 0 whenever e < 0, which would make pow extensionally equal to Zpower. But it's also possible that pow 1 e = 1 whenever e < 0.

You can also prove properties of the function independently of the function's definition. For example, you can use induction on the arguments to prove interesting properties like

Lemma pow_plus :
  forall b n1 n2,
    pow b (Z_of_nat n1 + Z_of_nat n2) =
    pow b (Z_of_nat n1) * pow b (Z_of_nat n2).
Proof.
  induction n2.
  (*same techniques as above*)
Qed.
$\endgroup$
  • $\begingroup$ Thank you very much ! It is very good and helpful answer. What do you think is better to do showing the extensional equality of definitions and then prove the properties or proving generated definitions directly? $\endgroup$ – Anton Sep 12 '11 at 11:54
  • $\begingroup$ Coq's theory is very constructive, so it's usually easier to prove things about an inductive definition than about an equational specification. As illustrated here, some things are obvious with an inductive definition, such as the fact that there exists exactly one matching function (the equational specification guarantees neither existence nor unicity). $\endgroup$ – Gilles Sep 12 '11 at 12:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.