How to use induction without Fixpoint definition in Coq?

Question

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.

Answer 1

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.