[Proof Ground 2020] Substrings

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 α]

/- Task -/
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.
Admitted.

(** * Alternative Task *)
(** 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