Coq inductive reasoning about ACSL inductive predicates?

Question

Is it possible to use induction on inductive predicates defined in ACSL?

Consider the following example from the ACSL manual:

struct List {
    int value;
    struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
  @   case empty{L}: \forall struct List* l; reachable(l, l);
  @   case non_empty{L}: \forall struct List *l1,*l2;
  @     \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
  @ }
*/

I am trying to prove the following lemma:

/*@ lemma next_null_reachable: \forall struct List* l;
  @   \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);
*/

Alt-Ergo fails here, so I resort to manual Coq reasoning:

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (a : addr),
  ((valid_rw t a 2%Z)) ->
  ((P_reachable t t_1 a (null))) ->
  ((P_reachable t t_1 (t_1.[ (shiftfield_F_List_next a) ]) (null))).

But when I Search P_reachable, I find only two axioms generated:

Q_non_empty:
  forall (t : array int) (t_1 : farray addr addr) (a_1 a : addr),
  valid_rw t a_1 2 ->
  P_reachable t t_1 (t_1 .[ shiftfield_F_List_next a_1]) a ->
  P_reachable t t_1 a_1 a
Q_empty:
  forall (t : array int) (t_1 : farray addr addr) (a : addr),
  P_reachable t t_1 a a    

And no induction principle. So I can not apply induction P_reachable or destruct P_reachable.

I use WP plugin of frama-c version Sodium-20150201.

To reproduce, you could run frama-c -wp -wp-rte -wp-prover coqide file.c, where file.c contains the List and reachable definitions and the next_null_reachable lemma.

Answer 1

From the form of your goals, I'm assuming you're using the WP plugin. Indeed, it does not provide a lemma indicating that reachable is the smallest predicate verifying the two cases empty and non_empty, meaning that you can't use induction.

If I remember correctly, adding such an axiom would confuse first-order theorem provers (who would repeatedly construct instances of reachable through empty or non_empty and destruct them with the induction principle). However, the Coq output of WP could very well provide a complete translation.

A workaround is to provide an appropriate set of specialized lemmas (that will not be provable through WP) instead of the induction principle. See e.g. binary_search_proved.c in this archive.

Answer 2

I never used Alt-Ergo, but it seems that they don't create real inductive proposition, but rather axiomatize them. So you can't do induction but you can use the basic blocks they provide (Q_empty is your default constructor and Q_non_empty is your inductive constructor) to perform the proof.

I lack some basic definitions to replay your problem, but I would go by applying Q_non_empty once, which should ask me to prove a valid_rw statement and a sub P_reachable statement. They both should be provable using your context.