Return to 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.

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.

I want to verificate 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 verifikate 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.

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.