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.