initial commit

ROOTS

@@ -0,0 +1 @@
+VerifyThis2024

VerifyThis2024/ROOT

@@ -0,0 +1,6 @@
+session VerifyThis2024 = HOL +
+  options [document = pdf, document_output = "output"]
+theories [document = false]
+    Ropes
+document_files
+    "root.tex"

VerifyThis2024/Ropes.thy

@@ -0,0 +1,170 @@
+theory Ropes
+imports Main
+begin
+
+section\<open>Challenge 0 from VerifyThis 2024: https://www.pm.inf.ethz.ch/research/verifythis.html\<close>
+
+subsection\<open>The Rope Data Structure\<close>
+
+text\<open>The task is to implement a "Rope" ( https://en.wikipedia.org/wiki/Rope_(data_structure) ) 
+- a special type of binary tree to represent a string (in honor of Billy who can't be here today).\<close>
+
+datatype Rope =  Leaf String.literal nat | Node Rope nat Rope 
+
+abbreviation \<open>hello_world_rope \<equiv> Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5)\<close> 
+
+text\<open>A Rope subdivides a string into substrings where a leaf contains a substring 
+and a weight that is equal to the number of characters in the substring (see example from wiki page). 
+The corresponding parent node stores the sum of left child weights (see example from wiki page).\<close>
+
+subsection\<open>Tasks\<close>
+
+text\<open>Implement a function @{term \<open>valid_rope (r :: Rope) :: bool\<close>} which checks that a rope is well constructed\<close>
+
+fun sum_weights :: \<open>Rope \<Rightarrow> nat\<close> where 
+\<open>sum_weights (Leaf _ s) = s\<close>|
+\<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close>
+
+fun valid_rope :: \<open>Rope \<Rightarrow> bool\<close> where
+\<open>valid_rope (Leaf s w) = (size s = w)\<close>|
+\<open>valid_rope (Node l w r) = (valid_rope l \<and> valid_rope r \<and> (w = sum_weights l))\<close>
+
+text\<open>Implement a naive traversal function @{term \<open>to_str (r :: Rope) :: string\<close>} that converts the Rope to the stored string.\<close>
+
+fun to_str :: \<open>Rope \<Rightarrow> String.literal\<close> where 
+\<open>to_str (Leaf s _) = s\<close>|
+\<open>to_str (Node l _ r) = to_str l + to_str r\<close>
+
+value \<open>to_str (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
+
+value \<open>valid_rope (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
+
+text\<open>Implement a function @{term \<open>str_len (r :: Rope)\<close>} that can efficiently compute the length of the string. Further, prove its correctness\<close>
+
+lemma literal_plus_size_eq: \<open>size ((l::String.literal) + r) = size l + size r\<close>
+  by (simp add: plus_literal.rep_eq size_literal.rep_eq)
+
+fun str_len :: \<open>Rope \<Rightarrow> nat\<close> where 
+\<open>str_len (Leaf _ N) = N\<close>|
+\<open>str_len (Node l w r) = w + str_len r\<close>
+
+value \<open>size (to_str hello_world_rope)\<close>
+
+lemma sum_weights_eq_size:
+  assumes \<open>valid_rope r\<close> 
+  shows \<open>sum_weights r = size (to_str r)\<close>
+using assms proof(induction r)
+  case (Leaf s w)
+  then show ?case by simp
+next
+  case (Node l w r)
+  have \<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close> by simp
+  moreover have \<open>... = size (to_str l) + size (to_str r)\<close> using Node by simp
+  moreover have \<open>... = size (to_str l + to_str r)\<close> using literal_plus_size_eq by simp
+  ultimately show ?case by simp
+qed
+
+lemma str_len_eq_size:
+  assumes \<open>valid_rope r\<close>
+  shows   \<open>str_len r = size (to_str r)\<close>
+using assms proof(induction r)
+  case (Leaf s w)
+  then show ?case by simp
+next
+  case (Node l w r)
+  hence left_valid: \<open>valid_rope l\<close> and right_valid: \<open>valid_rope r\<close> and w_def : \<open>w = sum_weights l\<close> by simp+
+  hence \<open>str_len (Node l w r) = sum_weights l + str_len r\<close> by (simp add: Node)
+  moreover have \<open>... = size (to_str l) + size (to_str r)\<close> by (simp add: sum_weights_eq_size left_valid right_valid Node)
+  moreover have \<open>... = size (to_str l + to_str r)\<close> by (simp add: literal_plus_size_eq)
+  ultimately show ?case by simp
+qed
+
+lemma str_len_sum_weights_eq:
+  assumes \<open>valid_rope r\<close>
+  shows \<open>str_len r = sum_weights r\<close>
+  using str_len_eq_size sum_weights_eq_size assms by auto
+
+text\<open>Implement a function that computes the concatenation of two ropes @{term \<open>rope_concat (l::Rope) (r :: Rope)\<close>}\<close>
+
+definition rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> where
+\<open>rope_concat l r = Node l (str_len l) r\<close>
+
+lemma valid_rope_concat:
+  assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
+  shows \<open>valid_rope (rope_concat l r)\<close> by (simp add: assms str_len_sum_weights_eq rope_concat_def)
+
+lemma rope_concat_eq: \<open>to_str (rope_concat l r) = to_str l + to_str r\<close> by (simp add: rope_concat_def)
+
+text\<open>Implement a function @{term \<open>rope_delete (r :: Rope) (i :: nat) (len :: nat)\<close>} that returns a rope where the @{term \<open>len\<close>} 
+characters starting from the position @{term \<open>i\<close>} have been removed.\<close>
+
+fun sub_str :: \<open>String.literal \<Rightarrow> nat set \<Rightarrow> String.literal\<close> where
+\<open>sub_str s I = String.implode (nths (literal.explode s) I)\<close>
+
+lemma explode_sub_str: \<open>literal.explode (sub_str s I) = nths (literal.explode s) I\<close> 
+  by (metis String.implode_explode_eq implode.rep_eq nths_map sub_str.simps)
+
+lemma size_implode_single: \<open>size (String.implode [x]) = Suc 0\<close> by (simp add: size_literal.rep_eq)
+
+lemma size_implode: \<open>size (String.implode xs) = length xs\<close> 
+proof(induction xs)
+  case Nil
+  then show ?case 
+    by (simp add: size_literal.rep_eq)
+next
+  case (Cons a xs)
+  have \<open>size (String.implode (a # xs)) = (size (String.implode [a] + String.implode xs))\<close> 
+    apply (simp add: String.implode_def)
+    by (metis String.explode_implode_eq add_0 add_Suc implode.abs_eq length_Cons list.simps(8,9)
+        list.size(3) literal_plus_size_eq size_literal.rep_eq)
+  moreover have \<open>... = Suc (size (String.implode xs))\<close> by (simp add: literal_plus_size_eq size_implode_single)
+  moreover have \<open>... = Suc (length xs)\<close> using Cons by blast
+  ultimately show ?case by simp 
+qed
+
+lemma size_sub_str: \<open>size (sub_str s I) = card {i. i < size s \<and> i \<in> I}\<close> 
+  by(simp add: size_implode length_nths size_literal.rep_eq)
+
+lemma atLeastLessThan_eq: \<open>{i..<size s} = {ia. ia < size s \<and> i \<le> ia}\<close> by auto
+
+lemma atLeastAtMost_eq: \<open>(if i < size s then {..i} else {..<size s}) = {ia. ia < size s \<and> ia \<le> i}\<close> by auto
+
+lemma size_sub_str_atLeast: \<open>size (sub_str s {i..}) = size s - i\<close> unfolding size_sub_str[of s \<open>{i..}\<close>]
+  by (simp add: atLeastLessThan_eq[symmetric])
+
+lemma size_sub_str_atMost: \<open>size (sub_str s {..i}) = (if i < size s then Suc i else size s)\<close> unfolding size_sub_str[of s \<open>{..i}\<close>]
+  by (simp add: atLeastAtMost_eq[symmetric])
+
+fun split :: \<open>Rope \<Rightarrow> nat \<Rightarrow> Rope \<times> Rope\<close> where
+\<open>split (Leaf s w) i = (Leaf (sub_str s {0..i}) w, Leaf (sub_str s {i..size s}) (size s - i))\<close>|
+\<open>split (Node l w r) i = (if i < w then 
+                            (let (left, right) = split l i 
+                             in (left, rope_concat right r)) 
+                        else 
+                             (if i > w then 
+                                 (let (left,right) = split r (i - w) 
+                                  in (rope_concat l left, right)) 
+                              else (l,r)))\<close>
+
+fun rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close> where
+\<open>rope_delete rope i len = (let (left,rem) = split rope i; 
+                               (_, right) = split rem len 
+                            in rope_concat left right)\<close>
+
+
+definition \<open>hello_my_rope \<equiv> rope_concat (Leaf STR ''Hello_'' 6) (Leaf STR ''my_'' 3)\<close>
+
+definition \<open>name_i_rope \<equiv> rope_concat (Leaf STR ''na'' 2) (Leaf STR ''me_i'' 4)\<close>
+
+definition \<open>s_Simon_rope \<equiv> rope_concat (Leaf STR ''s'' 1) (Leaf STR ''_Simon'' 6)\<close>
+
+definition \<open>name_is_Simon_rope \<equiv> rope_concat name_i_rope s_Simon_rope\<close>
+
+definition \<open>hello_my_name_is_Simon_rope \<equiv> rope_concat (rope_concat hello_my_rope name_is_Simon_rope) (Leaf STR '''' 0)\<close>
+
+value \<open>to_str (rope_delete hello_my_name_is_Simon_rope (0) 18)\<close>
+
+text\<open>Implement a method @{term \<open>rope_insert (r :: Rope) (i :: nat) (I :: String.literal)\<close>} that inserts the string @{term I} at position @{term \<open>i\<close>}.\<close>
+
+text\<open>These methods are correct as is, but do not perform the most optimally. Optimize these operations by rebalancing the Rope.\<close>
+end

VerifyThis2024/document/root.tex

@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{VerifyThis2024}
+\author{user}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

document/root.tex

@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{IsabelleClub}
+\author{user}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: