// Subsequence relation for insertion/deletion codes
// Source: HeytingLean.CodingTheory.InsDel.Subsequence
// Theorem preserved: subseq_refl, subseq_nil_left

pub fn is_subsequence<T: Eq>(xs: &[T], ys: &[T]) -> bool {
    let mut xi = 0;
    for y in ys {
        if xi < xs.len() && xs[xi] == *y {
            xi += 1;
        }
    }
    xi == xs.len()
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_subseq_refl() {
        let xs = vec![1u8, 2, 3, 4];
        assert!(is_subsequence(&xs, &xs));
    }

    #[test]
    fn test_nil_subseq() {
        let empty: Vec<u8> = vec![];
        assert!(is_subsequence(&empty, &[1, 2, 3]));
    }

    #[test]
    fn test_subsequence_true() {
        assert!(is_subsequence(&[1u8, 3], &[1, 2, 3, 4]));
    }

    #[test]
    fn test_subsequence_false() {
        assert!(!is_subsequence(&[3u8, 1], &[1, 2, 3, 4]));
    }
}