<p>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 <em>extensional equality</em> of the two functions.</p>

<p>There is a <code>Zpower</code> function in the standard library, defined recursively:</p>

<pre><code>Fixpoint iter_pos (n:positive) (A:Type) (f:A -&gt; A) (x:A) {struct n} : A :=
  match n with
    | xH =&gt; f x
    | xO n' =&gt; iter_pos n' A f (iter_pos n' A f x)
    | xI n' =&gt; 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 =&gt; z * x) 1.
Definition Zpower (x y:Z) :=
    match y with
      | Zpos p =&gt; Zpower_pos x p
      | Z0 =&gt; 1
      | Zneg p =&gt; 0
    end.
</code></pre>

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

<pre><code>Lemma neq_int_bool : forall x y, eq_int_bool x y = false &lt;-&gt; x &lt;&gt; y.
Proof.
  intros.
  pose (A := eq_int_bool_axiom x y); clearbody A.
  split; intros.
  intro E; apply &lt;- A in E. assert (false = true); solve [eauto with bool].
  case_eq (eq_int_bool x y); intro E.
  apply -&gt; 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 &lt;- 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 &lt;- neq_int_bool. intro; discriminate.
Qed.
</code></pre>

<p>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 <code>pow b e = 0</code> whenever <code>e &lt; 0</code>, which would make <code>pow</code> extensionally equal to <code>Zpower</code>. But it's also possible that <code>pow 1 e = 1</code> whenever <code>e &lt; 0</code>.</p>

<p>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</p>

<pre><code>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.
</code></pre>

CC BY-SA 3.0
2011-09-12T11:54:42.460Z
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?
Anton
CC BY-SA 3.0
2011-09-12T12:41:24.780Z
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).
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2011-09-10T00:24:42.357Z
2011-09-10T00:24:42.357Z
Gilles 'SO- stop being evil'
<p>I want to verify a program written in C. I am using <a href="http://krakatoa.lri.fr/" rel="nofollow">Jessie</a> to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions. </p>

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

<p>For example the power function:</p>

<pre><code>Require Export ZArith.
Open Scope Z_scope.

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

Definition eq_int_bool : Z -&gt; Z -&gt; bool.
Admitted.

Lemma eq_int_bool_axiom :
  (forall (x:Z), (forall (y:Z), ((eq_int_bool x y) = true &lt;-&gt; 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.
</code></pre>

<p>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.</p>

CC BY-SA 3.0
2012-04-18T19:12:31.963Z
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?
Andrej Bauer
<lo.logic><coq><program-verification><formal-methods>
How to use induction without Fixpoint definition in Coq?
Anton
# How to use induction without Fixpoint definition in Coq?

(Asked by: username_0 on 2011-09-09)

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.

**Tags:** lo.logic, coq, program-verification, formal-methods

> **Comments:**
> **username_1**: 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?  

---

## 1 answers

### Answer by username_2 on 2011-09-10. Score: 7

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: 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).  

---

