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.

Download Files
### Definitions File

### Template File

### Check 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

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

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

### Template File

### Check 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

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

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

### Template 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.

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