Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

[Proof Ground 2020] Substrings

Given a string `s`, its subsequence is any string that can be obtained by erasing some (possibly none or all) characters of `s`. For example, `ace` is a subsequence of `abcde`. A *proper* subsequence of `s` is any subsequence of `s` but `s` itself. Consider the following problem: given two strings `x` and `y`, is every proper subsequence of `x` a subsequence of `y`? Examples: - `x = ab` and `y = ba`: yes - `x = abcd` and `y = cdabc`: no. `ad` is not a subsequence of `y`. Your task is to prove that a given algorithm for this problem is correct (task 1). To make it easier, you can choose to program your own solution and prove it correct (task 2). This will score you 50%. Submitted by: Martin Raszyk Coq: Fabian Kunze | Lean: Simon Hudon & Kevin Kappelmann | Isabelle: Simon Wimmer

Resources

Definitions File

theory Defs
imports Main
begin

inductive subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr "\<sqsubseteq>" 50) where
[intro]: "[] \<sqsubseteq>  _"
| [intro]: "xs \<sqsubseteq> ys \<Longrightarrow> x # xs \<sqsubseteq> x # ys"
| [intro]: "xs \<sqsubseteq> ys \<Longrightarrow> xs \<sqsubseteq> y # ys"

definition proper_subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr "\<sqsubset>" 50) where
"xs \<sqsubset> ys \<longleftrightarrow> xs \<noteq> ys \<and> xs \<sqsubseteq> ys"

definition all_proper_subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
"all_proper_subseq xs ys \<longleftrightarrow> (\<forall>xs'. xs' \<sqsubset> xs \<longrightarrow> xs' \<sqsubseteq> ys)"

fun aux where
"aux [] _ = True"
| "aux _ [] = False"
| "aux (x#xs) (y#ys) = (if x = y then aux xs ys else aux (x # xs) ys)"

fun aux2 where
"aux2 ys acc [] = True"
| "aux2 ys acc (x # xs) \<longleftrightarrow> aux (acc @ xs) ys \<and> aux2 ys (acc @ [x]) xs"

definition
"judge1 xs ys \<longleftrightarrow> aux2 ys [] xs"

end

Template File

theory Submission
imports Defs
begin

theorem judge1_correct: "judge1 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
sorry

definition
"judge2 xs ys \<longleftrightarrow> judge1 xs ys"

theorem judge2_correct:
"judge2 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
unfolding judge2_def by (rule judge1_correct)

theorem judge2_is_executable:
"judge2 ''ab'' ''ab'' \<longleftrightarrow> True"
"judge2 ''ba'' ''ab'' \<longleftrightarrow> True"
"judge2 ''abcd'' ''cdabc'' \<longleftrightarrow> False"
by eval+

end

Check File

theory Check
imports Submission
begin

theorem judge1_correct: "judge1 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
by (rule Submission.judge1_correct)

theorem judge2_correct:
"judge2 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
by (rule Submission.judge2_correct)

theorem judge2_is_executable:
"judge2 ''ab'' ''ab'' \<longleftrightarrow> True"
"judge2 ''ba'' ''ab'' \<longleftrightarrow> True"
"judge2 ''abcd'' ''cdabc'' \<longleftrightarrow> False"
by eval+

end

Definitions File

import data.list.basic

variable {α : Type*}

-- `<+` is notation for `is_sublist`
def is_strict_sublist (xs ys : list α) : Prop :=
xs <+ ys ∧ xs ≠ ys

infix ` <<+ `:50 := is_strict_sublist

def all_proper_sublist (xs ys : list α) : Prop := ∀ (xs' <<+ xs), xs' <+ ys

variable [decidable_eq α]

def judge_aux : list α → list α → Prop
| [] _ := true
| _ [] := false
| (x::xs) (y::ys) :=
if x = y then judge_aux xs ys
else judge_aux (x :: xs) ys

def judge_aux2 (ys : list α) : list α → list α → Prop
| acc [] := true
| acc (x :: xs) := judge_aux (acc ++ xs) ys ∧ judge_aux2 (acc ++ [x]) xs

def judge1 (xs ys : list α) : Prop :=
xs ≠ ys ∧ xs.length = ys.length ∧ judge_aux2 ys [] xs

----------------------just some definitions to prevent cheating------------------------

definition judge1_correct_prop : Prop := ∀ {α : Type*} [eq_inst : decidable_eq α] (xs ys : list α),
@judge1 α eq_inst xs ys ↔ all_proper_sublist xs ys

notation `judge1_correct_prop` := judge1_correct_prop

Template File

import .defs

variables {α : Type*} [decidable_eq α]

theorem judge1_correct : ∀ (xs ys : list α),
judge1 xs ys ↔ all_proper_sublist xs ys :=
sorry

def judge2 (xs ys : list α) : Prop := judge1 xs ys

theorem judge2_correct : ∀ (xs ys : list α),
judge2 xs ys ↔ all_proper_sublist xs ys :=
sorry

Check File

import .defs
import .submission

theorem check_judge1_correct : judge1_correct_prop := @judge1_correct

definition judge2_correct_prop : Prop := ∀ {α : Type*} [eq_inst : decidable_eq α] (xs ys : list α),
@judge2 α eq_inst xs ys ↔ all_proper_sublist xs ys

theorem check_judge2_correct : judge2_correct_prop := @judge2_correct

Definitions File

From Coq Require Export Lists.List.
Export List.ListNotations.
Require Export PeanoNat.

Inductive subseq : list nat -> list nat -> Prop :=
subseq_nil : subseq [] []
| subseq_take xs ys x: subseq xs ys -> subseq (x::xs) (x::ys)
| subseq_drop xs ys x: subseq xs ys -> subseq xs (x::ys).

Definition proper_subseq (xs ys : list nat) :=
xs <> ys /\ subseq xs ys.

Definition all_proper_subseq (xs ys : list nat) :=
forall xs', proper_subseq xs' xs -> subseq xs' ys.

Fixpoint aux (xs ys : list nat) :bool :=
match xs,ys with
[],_ => true
| _,[] => false
| x::xs,y::ys => if Nat.eq_dec x y then aux xs ys else aux (x::xs) ys
end.

Fixpoint aux2 (ys acc xs : list nat) : bool :=
match xs with
[] => true
| x::xs => aux (acc++xs) ys && aux2 ys (acc++[x]) xs
end.

Definition judge1 xs ys := aux2 ys [] xs.

Template File

Require Import Defs.

(** * Task 1: completion of this gives full points*)
Lemma judge1_correct xs ys:
(all_proper_subseq xs ys) <-> judge1 xs ys = true.

(** Show any implementation correct for half the points *)

Definition judge2:= judge1.

Lemma judge2_correct xs ys:
(all_proper_subseq xs ys) <-> judge2 xs ys = true.
Proof.
apply judge1_correct.
Qed.

Definitions File

theory Defs
imports Main
begin

inductive subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr "\<sqsubseteq>" 50) where
[intro]: "[] \<sqsubseteq>  _"
| [intro]: "xs \<sqsubseteq> ys \<Longrightarrow> x # xs \<sqsubseteq> x # ys"
| [intro]: "xs \<sqsubseteq> ys \<Longrightarrow> xs \<sqsubseteq> y # ys"

definition proper_subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr "\<sqsubset>" 50) where
"xs \<sqsubset> ys \<longleftrightarrow> xs \<noteq> ys \<and> xs \<sqsubseteq> ys"

definition all_proper_subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
"all_proper_subseq xs ys \<longleftrightarrow> (\<forall>xs'. xs' \<sqsubset> xs \<longrightarrow> xs' \<sqsubseteq> ys)"

fun aux where
"aux [] _ = True"
| "aux _ [] = False"
| "aux (x#xs) (y#ys) = (if x = y then aux xs ys else aux (x # xs) ys)"

fun aux2 where
"aux2 ys acc [] = True"
| "aux2 ys acc (x # xs) \<longleftrightarrow> aux (acc @ xs) ys \<and> aux2 ys (acc @ [x]) xs"

definition
"judge1 xs ys \<longleftrightarrow> aux2 ys [] xs"

end

Template File

theory Submission
imports Defs
begin

theorem judge1_correct: "judge1 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
sorry

definition
"judge2 xs ys \<longleftrightarrow> judge1 xs ys"

theorem judge2_correct:
"judge2 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
unfolding judge2_def by (rule judge1_correct)

theorem judge2_is_executable:
"judge2 ''ab'' ''ab'' \<longleftrightarrow> True"
"judge2 ''ba'' ''ab'' \<longleftrightarrow> True"
"judge2 ''abcd'' ''cdabc'' \<longleftrightarrow> False"
by eval+

end

Check File

theory Check
imports Submission
begin

theorem judge1_correct: "judge1 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
by (rule Submission.judge1_correct)

theorem judge2_correct:
"judge2 xs ys \<longleftrightarrow> all_proper_subseq xs ys"
by (rule Submission.judge2_correct)

theorem judge2_is_executable:
"judge2 ''ab'' ''ab'' \<longleftrightarrow> True"
"judge2 ''ba'' ''ab'' \<longleftrightarrow> True"
"judge2 ''abcd'' ''cdabc'' \<longleftrightarrow> False"
by eval+

end

Terms and Conditions