false can be proved

[cu1ch3n]

We (@jiangsy) found that there might be a bug in the equality check, and we could exploit it to prove false. Here is an working example tested on abella-2.0.7 and the lastest abella-2.0.8-dev:

Define append : olist -> olist -> olist -> prop by
    append nil L L ;
    append (N :: L1) L2 (N :: L3) := append L1 L2 L3.

Theorem append_mem : forall AB A B X,
    append A B AB -> (member X A \/ member X B) -> member X AB.
induction on 1. intros. case H2.
    case H1. case H3. case H3. search. apply IH to H4 _. search.
    case H1. search. apply IH to H4 _. search.

Theorem mem_FxE_FyE : forall F E FxE (X : o) FyE Y M,
    append F (X :: E) FxE -> append F (Y :: E) FyE -> member M FxE ->
    (X = M -> false) -> (Y = M -> false) -> member M FyE.
induction on 1. intros. case H1.
    case H3. apply H4 to _. case H2. search.
    case H3. case H2. search.
        case H2. apply IH to H6 H8 _ _ _. search.

Kind ty type.

Type i      ty.
Type tyvar  ty -> ty -> o.
Type exvar  ty -> o.

Define wfj : olist -> prop by
    wfj nil;
    nabla x, wfj (tyvar x A :: E) := wfj E;
    nabla x, wfj (exvar x :: E) := wfj E.

Theorem member_prune : forall (E : olist) B, nabla (x : ty),
    member (B x) E -> exists Fr, B = x\Fr.
induction on 1. intros. case H1.
    search. apply IH to H2. search.

Theorem wfj_tyvar_exvar : forall E X A,
    wfj E -> member (tyvar X A) E -> member (exvar X) E -> false.
induction on 1. intros. case H1.
    case H2.
    case H2. case H3. apply member_prune to H5.
        case H3. apply IH to H4 H5 H6.
    case H2. case H3. apply member_prune to H5.
        apply IH to H4 H5 H6.

Theorem false_lemma : forall F E FtyE FexE A B, nabla x,
    append (F x) (tyvar x A :: E) (FtyE x) ->
    append (F x) (exvar x :: E) (FexE x) ->  wfj (FtyE x) -> wfj (FexE x) ->
    member (tyvar x B) (FtyE x) -> member (tyvar x B) (FexE x).
intros. apply mem_FxE_FyE to H1 H2 _ _ _. search.

Theorem prove_false : false.
apply false_lemma to _ _ _ _ _ with
    FtyE = x\(tyvar x i :: nil), FexE = x\(exvar x :: nil).
case H1. case H2.

[chaudhuri]

Thanks for the report. Trying to figure out what went wrong.

[lambdacalculator]

Could you leave a note here for posterity saying what the bug was?

[chaudhuri]

Thanks for asking for this. It turns out that the bug is not yet fully fixed. Here is a simpler example that still triggers this unsoundness:

Kind u type.
Type i u.
Type p, q, r u -> o.

Define dd : o -> prop by
  dd (q i).

Theorem lem: forall X Y,
  dd X ->
  dd Y ->
  (X = r i -> false) ->
  (Y = r i -> false).
intros. case H1. case H2. apply H3 to H4.

Theorem foo: forall F, dd F -> false.
intros.
apply lem to H1 H1 _ _. search. case H1.

Theorem bar: dd (q i).
search.

Theorem unsound: false.
apply foo to bar.

The issue is that apply with unknowns calls search to finish the generated subgoals, but doesn't make sure that the different invocations of search have compatible instances for generated meta-variables. Needs a more careful implementation than the quick hack I attempted earlier.

By the way, this is a very old bug in Abella. Seems to happen even in pre 2.0.x.

[lambdacalculator]

Thanks, although your example didn't actually use p : u -> o, so it could be a little simpler! It's interesting that this has been around this long and not discovered.

[chaudhuri]

Pre 2.0.x the search tactic basically didn't handle equality, so this bug was never triggered. Now that we eagerly destruct equalities when they enter the context during search, it seems that we accidentally instantiate variables that should not be instantiated. I'm trying a few potential fixes out now.

[chaudhuri]

Turns out this issue was noted at least twice earlier in two different issues: #113 and #127. Sadly, we didn't weed out all the cases where search was implicitly invoked without protecting the bind state for meta-variables. Might be worth it to methodically check every single tactic once again.