Subsequences in Coq

Question

I am a new to proof assistants and recently got stuck on the subsequence exercise from the chapter on inductively defined propositions from Logical Foundations.

The exercise asks to define an inductive proposition subseq for lists of natural numbers and prove several claims. While trying to prove transitivity, I defined a function subseqb : list nat -> list nat -> bool and tried proving that it is equivalent to subseq. I am only able to prove the following direction: forall {l1 l2 : list nat}, subseqb l1 l2 = true -> subseq l1 l2.

All of my attempts at proving the converse fail, and seem to boil down to my inability to prove the lemma cons_cancel_subseq below. I tried induction on subseq hypotheses, lists and list lengths in various orders, as well as using list reversal.

Can someone point out how to prove either of the incomplete results below?

Require Import List.
Require Import Nat.
Require Import Bool.
Import ListNotations.

Inductive subseq : list nat -> list nat -> Prop :=
  | hl1 : subseq [] []
  | hl2 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),
      subseq lst1 (x :: lst2)
  | hl3 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),
      subseq (x :: lst1) (x :: lst2).

Fixpoint subseqb (lst1 l2 : list nat) : bool :=
  match lst1, l2 with
    | [], [] => true
    | [], y :: ys => true
    | x :: xs, [] => false
    | x :: xs, y :: ys => match x =? y with
                            | true => subseqb xs ys
                            | false => subseqb lst1 ys
                          end
  end.

Theorem subseq__subseqb : forall {l1 l2 : list nat},
    subseq l1 l2 -> subseqb l1 l2 = true.
Proof.
  Abort.

Lemma cons_canel_subseq : forall {x : nat} {lst1 lst2 : list nat},
    subseq (x :: lst1) (x :: lst2) -> subseq lst1 lst2.
Proof.
  Abort.

Answer 1

Regarding your lemma cons_cancel_subseq, your issue has probably to do with performing induction on predicates which are not applied on variables. You can try and use dependent induction for such a setting (you'll need to import Program.Equality from the standard library for that though).

But a better idea is to obtain your lemma as a corollary of another one where the arguments to subseq are variables. I suggest the following:

Definition tail (l : list nat) : list nat :=
  match l with
    | [] => []
    | x :: l' => l'
  end.

Lemma subseq_tl {lst1 lst2 : list nat} :
    subseq lst1 lst2 -> subseq (tail lst1) lst2.

Note, though, that your are taking a very long detour: you should be able to prove transitivity of subseq much more direcly. I would suggest the following:

Theorem subseq_trans {l1 l2 l3 : list nat} :
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros H1 H2.
  induction H2 in l1, H1 |- *.

ie, induction on the second proof of subseq, generalizing over any subsequence of l2.

Answer 2

Here is a complete proof of cons_cancel_subseq. There is a lot going on, and it can probably be simplified with someone more familiar with Coq. Let me explain the high-level details.

The basic structure of the proof follows this sequence:

• Destruct the subseq evidence, the hl1 and hl3 cases should be trivial.
• Now, if the underlying data looks like an hl2, then we need to dig into the lists because it must be the case that l2 = prefix ++ x :: suffix, and we need to process the prefix to obtain the matching x. Thus, we need to perform induction on l2.
• From there we get a trivial base case and l2 = a :: l2', now we consider the cases when x = a and x <> a separately.
• For both situations, we destruct the subseq evidence again, potentially recursing using the inductive hypothesis.

Some important technical things to note:

• In order to destruct the evidence in a way that is going to be useful we want to make it look like subseq a b for variables a and b. Of course, we don't have that, but we can fix it by using the remember tactic on the arguments to subseq. This will setup the evidence in a more amenable way and record the necessary equalities for us. This is similar to dependent induction but I personally prefer this method.
• I use the pose proof tactic to introduce new facts, it is like forward reasoning. Coq is great at backward reasoning but a lot of the time you just want to learn a new fact and this tactic helps with that.
• Because we introduced a lot of equations we have a lot of extra variables, the subst_list tactic breaks down an equation of the form x :: l1 = y :: l2 into the obvious equalities and substitutes them all away. This is useful to get rid of the extra equations when they are no longer needed.

As has already been noted the route you're taking is harder than what is needed to prove transitivity. But, it's also a lot more fun. I think your subseq_subseqb theorem will require the same skills used to prove the cons_cancel_subseq lemma, and these skills are pretty handy when working with inductive propositions.