Cookies disclaimer

I agree 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

Resources

Download Files

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
Download Files

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
Download Files

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.


Terms and Conditions