Inconsistency using backchain with induction hypothesis

[kyagrd]

The backchain tactic allows unsafe use of induction hypothesis. The way how one can exploit this is to make backchain IH to introduce the inductive argument as a proof obligation in the conclusion, and then you make Abella forget about the inductive restriction by asserting the very conclusion you are obliged to prove, provided that the proof obligation is provable. But this clearly leads to inconsistency because inductive restriction is suddenly dropped. Here is an example proving bogus theorems about the two-level specification of the finite pi-calculus, which is distributed with Abella. I was working with Abella 2.0.5-dev version.

Specification "finite-pic". %% examples/process-calculi/pic_two_level

Theorem boo : forall A P Q, {one P A Q} -> exists R, {one Q A R}.
  induction on 1.  intros.  case H1.
    backchain IH with P = P. assert {one (out X Y Q) (up X Y) Q}. backchain H2.
    backchain IH with P = P. assert {one (taup Q) tau Q}. backchain H2.
    backchain IH with P = P. assert {one (match X X P1) A Q}. backchain H3.
    backchain IH with P = P. assert {one (plus P1 Q1) A Q}. backchain H3.
    backchain IH with P = P. assert {one (plus P1 Q1) A Q}. backchain H3.
    backchain IH with P = P. assert {one (par P2 Q1) A (par P1 Q1)}. backchain H3.
    backchain IH with P = P. assert {one (par P1 Q2) A (par P1 Q1)}. backchain H3.
    backchain IH with P = P. assert {one (nu (x\P1 x)) A (nu (x\Q1 x))}. backchain H3.
    backchain IH with P = P. assert {one (par P1 Q1) tau (nu (y\par (M y) (N y)))}. backchain H4.
    backchain IH with P = P. assert {one (par P1 Q1) tau (nu (y\par (M y) (N y)))}. backchain H4.
    backchain IH with P = P. assert {one (par P1 Q1) tau (par (M Y) T)}. backchain H4.
    backchain IH with P = P. assert {one (par P1 Q1) tau (par R (M Y))}. backchain H4.

Theorem boo_bulshit :
  (forall A P Q, {one P A Q} -> exists R, {one Q A R}) -> false.
% Proof.
  intros. case H1.
  assert {one (taup null) tau null}.
  apply H1 to H2.
  case H3.
% Q.E.D.

[chaudhuri]

Thanks. This seems to be due to some changes we made to the search mechanisms in Abella recently. We may need to make a bugfix version of 2.0.4 soon.

[yvting]

The problem is with the "backchain" tactic: it does not check inductive restrictions, but only the coinductive ones. This is clearly wrong, as pointed out by kyagrd. I am going to add a check for backchaining such that a conclusion annotated with can only be back-chained on a formula annotated also with .

[chaudhuri]

Right. Thanks Yuting.

I am slightly shocked at the age of this bug. I think Andrew intended backchain to simply be disallowed for inductive hypotheses. He definitely makes a remark like that in the Abella tutorials/reference guide -- something like case not allowed fon coinductively and backchain not allowed for inductively restricted formulas..

[agacek]

Yes, I never intended backchain to work on goals with the inductive restriction. I suspect that I had such a check in there originally, but I'm not certain.

[yvting]

The checking of inductive/co-inductive restrictions is done in the function 'backchain_arrow' in 'tactics.ml'. Originally, there code looks like the following

    match term_to_restriction head, term_to_restriction goal with
    | CoSmaller i, CoSmaller j when i = j -> ()
    | CoSmaller _, _ -> failwith "Coinductive restriction violated"
    | _, _ -> ()

As you can see, only the co-inductive restrictions are checked. My fix is to add the following extra case

    | _ as hr, Smaller i -> 
      (match hr with
      | Smaller j when i = j -> ()
      | _ -> failwith "Inductive restriction violated")

before the last case. The idea is that a star-annotated goal must be an inductive assumption that has not been established. To prove such a goal we must match it with a star-annotated hypothesis.

Please let me know if my understanding of star-annotated goals is correct. If so I think my fix is correct.

From Andrew's comment, I have a feeling that we should not even have star-annotated goals in the first place. That is, we should establish the star-annotated assumption at the point the inductive hypothesis is used. This means backchain on 'IH' should be disallowed. This is also a viable fix, a cleaner one I would argue.

[kyagrd]

Thanks for the quick fix.

BTW, "backchain IH" is actually quite convenient when the inductive argument is already in the list of assumptions and the form of the conclusion matches with the result of IH. Cases for Simple binary structures can often be handed with "split. intros. backchain IH. backchain IH." pattern of tactics.

[chaudhuri]

@kyagrd I think what we will do is allow backchain IH. The source of the bug was the second backchain in all of your cases. This we will probably now disallow. You will be forced to use search instead, which treats inductive restrictions correctly. Basically backchain was never intended to be a synonym for search in the trivial case.

We use the inductive restrictions to extract (in principle) an inductive invariant for the induction rule of G, but this extraction is dubious if a *-annotation occurs in the conclusion. It may still work, but we will have to puzzle it out.