Understanding and working with nested inductive definitons in coq

Question

I'm trying to prove insert_SearchTree, a theorem about the preservation of a binary search tree after an insertion relation, below. I'm not sure how to use the induction hypothesis which relies on the nested Inductive definitions, namely SearchTree's single constructor calls on SearchTree'. Once I instantiate and invert the IH, though, we are given an arguement hi0 which is incomparable to k?

  ....
  H1 : SearchTree' 0 (insert k0 v0 l) hi0
  H2 : k0 < k
  ============================
  SearchTree' 0 (insert k0 v0 l) k

Is my approach to this proof flawed, or is there a trick to make them comparable? I had thought to try to prove something like

 Theorem insert_SearchTree'':
  forall k v t hi,
   SearchTree' 0 t hi -> SearchTree' 0 (insert k v t) hi .
Proof.

but after attempting I realized this is not equivalent (and I think unproveable, although I'm not sure)... Any advice is welcome. Most of the code is auxiliary, and I included it based on the advice that questions be stand-alone.

Require Export Coq.Arith.Arith.
Require Export Coq.Arith.EqNat.
Require Export Coq.omega.Omega.

Notation  "a >=? b" := (Nat.leb b a)
                          (at level 70, only parsing) : nat_scope.
Notation  "a >? b"  := (Nat.ltb b a)
                       (at level 70, only parsing) : nat_scope.
Notation " a =? b"  := (beq_nat a b)
                       (at level 70) : nat_scope.

Print reflect.

Lemma beq_reflect : forall x y, reflect (x = y) (x =? y).
Proof.
  intros x y.
  apply iff_reflect. symmetry.  apply beq_nat_true_iff.
Qed.

Lemma blt_reflect : forall x y, reflect (x < y) (x <? y).
Proof.
  intros x y.
  apply iff_reflect. symmetry. apply Nat.ltb_lt.
Qed.

Lemma ble_reflect : forall x y, reflect (x <= y) (x <=? y).
Proof.
  intros x y.
  apply iff_reflect. symmetry. apply Nat.leb_le.
Qed.

Hint Resolve blt_reflect ble_reflect beq_reflect : bdestruct.

Ltac bdestruct X :=
  let H := fresh in let e := fresh "e" in
   evar (e: Prop);
   assert (H: reflect e X); subst e;
    [eauto with bdestruct
    | destruct H as [H|H];
       [ | try first [apply not_lt in H | apply not_le in H]]].

Section TREES.
Variable V : Type.
Variable default: V.

Definition key := nat.

Inductive tree : Type :=
 | E : tree
 | T: tree -> key -> V -> tree -> tree.

Inductive SearchTree' : key -> tree -> key -> Prop :=
| ST_E : forall lo hi, lo <= hi -> SearchTree' lo E hi
| ST_T: forall lo l k v r hi,
    SearchTree' lo l k ->
    SearchTree' (S k) r hi ->
    SearchTree' lo (T l k v r) hi.

Inductive SearchTree: tree -> Prop :=
| ST_intro: forall t hi, SearchTree' 0 t hi -> SearchTree t.

Fixpoint insert (x: key) (v: V) (s: tree) : tree :=
 match s with
 | E => T E x v E
 | T a y v' b => if  x <? y then T (insert x v a) y v' b
                        else if y <? x then T a y v' (insert x v b)
                        else T a x v b
 end.

Theorem insert_SearchTree:
  forall k v t,
   SearchTree t -> SearchTree (insert k v t).
Proof.
  clear default.
  intros.
  generalize dependent v.
  generalize dependent k.
  induction H.
  induction H.
  - admit.
  - intros.
    specialize (IHSearchTree'1 k0 v0).
    inversion IHSearchTree'1. 
    subst.
    simpl.
    bdestruct (k0 <? k).
    apply (ST_intro _ hi0 ).
    constructor.
    admit.

End TREES.

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-05-12T14:54:38

The goal is currently too weak when you start induction. At the beginning of the second case, the goal looks like this:

  H : SearchTree' lo l k
  H0 : SearchTree' (S k) r hi
  IHSearchTree'1 : forall (k : key) (v : V), SearchTree (insert k v l)
  IHSearchTree'2 : forall (k : key) (v : V), SearchTree (insert k v r)
  ============================
  forall (k0 : key) (v0 : V), SearchTree (insert k0 v0 (T l k v r))

and the high-level idea to go on is to combine H and IHSearchTree'2, or H0 and IHSearchTree'1, depending on which side the insertion goes. But this is impossible because the SearchTree predicate in the two IH assumptions is not compositional: knowing only that insert k0 v0 l is a search tree does not help to know whether a tree containing it, T (insert k0 v0 l) k v r, is also a search tree. So the proof doesn't go through.

When putting search trees together, we don't just want to know that something is a search tree. We also want to know some bounds on the keys (here in particular, they must be bounded by k). This is what the auxiliary predicate SearchTree' provides. This matter of compositionality is precisely why SearchTree is defined using an auxiliary inductive predicate SearchTree', which is compositional (it can be, and is, defined in terms of itself).

Properties about recursive functions on trees mentioning SearchTree should first be generalized as more informative properties using SearchTree' so induction can go through. It will look like this:

Lemma insert_SearchTree' :
  forall t k0 v0   ???   ,
    SearchTree' ??? t ??? -> SearchTree' ??? (insert k0 v0 t) ???.

There are multiple valid ways of filling these "???" blanks. Coming up with new ones is a good exercise for the reader. One way that should work well here and many other situations is to put variables for all the missing arguments of predicates, and then figure out some suitable relation between them:

Lemma insert_SearchTree' :
  forall t k0 v0 lo hi lo' hi',
    ??? (* find a suitable assumption *) ->
    SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.

The relation should reflect the behavior of insert. What insert does, as far as those bounds are concerned, is to add the key k0 to the tree, so the bounds must bound that, in addition to the rest of the tree:

Lemma insert_SearchTree' :
  forall t k0 v0 lo hi lo' hi',
    lo' <= lo -> hi <= hi' ->
    lo' <= k0 -> k0 < hi' ->
    SearchTree' lo t hi -> SearchTree' lo' (insert k0 v0 t) hi'.

Finally, since we're going to use induction on the SearchTree' lo t hi assumption, it's desirable to move most variables and hypotheses that it does not mention to the right, to strengthen the induction hypothesis further (as far as I can tell, this is always safe to do):

Lemma insert_SearchTree' :
  forall t k0 v0 lo hi,          (* k0 and v0 remain constant throughout the recursive applications of (insert k0 v0), so they can stay here (it would still be fine if they are moved with the rest). *)
    SearchTree' lo t hi -> 
    forall lo' hi',              (* The bounds are going to change at every step, so they move to the right of the inductive predicate. *)
      lo' <= lo -> hi <= hi' ->
      lo' <= k0 -> k0 < hi' ->
      SearchTree' lo' (insert k0 v0 t) hi'.

Proving this lemma and using it to prove insert_SearchTree is left as an exercise for the reader.

Understanding and working with nested inductive definitons in coq

1 Answers