Theory Challenge1A

section ‹Challenge 1.A›
theory Challenge1A
imports Main
begin

text ‹Problem definition:
🌐‹https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges%202019/ghc_sort.pdf››

  subsection ‹Implementation›
  text ‹We phrase the algorithm as a functional program. 
    Instead of a list of indexes for segment boundaries,
    we return a list of lists, containing the segments.›

  text ‹We start with auxiliary functions to take the longest
    increasing/decreasing sequence from the start of the list
  ›  
  fun take_incr :: "int list ⇒ _" where
    "take_incr [] = []"
  | "take_incr [x] = [x]"
  | "take_incr (x#y#xs) = (if x<y then x#take_incr (y#xs) else [x])"  

  fun take_decr :: "int list ⇒ _" where
    "take_decr [] = []"
  | "take_decr [x] = [x]"
  | "take_decr (x#y#xs) = (if x≥y then x#take_decr (y#xs) else [x])"  
  
  fun take where
    "take [] = []"
  | "take [x] = [x]"
  | "take (x#y#xs) = (if x<y then take_incr (x#y#xs) else take_decr (x#y#xs))"  

  
  definition "take2 xs ≡ let l=take xs in (l,drop (length l) xs)"
    ― ‹Splits of a longest increasing/decreasing sequence from the list›

  
  text ‹The main algorithm then iterates until the whole input list is split›
  function cuts where
    "cuts xs = (if xs=[] then [] else let (c,xs) = take2 xs in c#cuts xs)"    
    by pat_completeness auto

  subsection ‹Termination›  
  text ‹First, we show termination. This will give us induction and proper unfolding lemmas.›

  lemma take_non_empty:
    "take xs ≠ []" if "xs ≠ []"
    using that
    apply (cases xs)
     apply clarsimp
    subgoal for x ys
      apply (cases ys)
       apply auto
      done
    done

  termination
    apply (relation "measure length")
     apply (auto simp: take2_def Let_def)
    using take_non_empty
    apply auto
    done
    
  declare cuts.simps[simp del]  
    
  subsection ‹Correctness›
  

  subsubsection ‹Property 1: The Exact Sequence is Covered›
  lemma tdconc: "∃ys. xs = take_decr xs @ ys"
    apply (induction xs rule: take_decr.induct)
    apply auto
    done

  lemma ticonc: "∃ys. xs = take_incr xs @ ys"
    apply (induction xs rule: take_incr.induct)
    apply auto
    done

  lemma take_conc: "∃ys. xs = take xs@ys"  
    using tdconc ticonc 
    apply (cases xs rule: take.cases)
    by auto 
  
  theorem concat_cuts: "concat (cuts xs) = xs"
    apply (induction xs rule: cuts.induct)
    apply (subst cuts.simps)
    apply (auto simp: take2_def Let_def)
    by (metis append_eq_conv_conj take_conc)  
  
        
        
  subsubsection ‹Property 2: Monotonicity›
  text ‹We define constants to specify increasing/decreasing sequences.›
  fun incr where
    "incr [] ⟷ True"
  | "incr [_] ⟷ True"
  | "incr (x#y#xs) ⟷ x<y ∧ incr (y#xs)"  
  
  fun decr where
    "decr [] ⟷ True"
  | "decr [_] ⟷ True"
  | "decr (x#y#xs) ⟷ x≥y ∧ decr (y#xs)"  
  
  lemma tki: "incr (take_incr xs)"
    apply (induction xs rule: take_incr.induct)
    apply auto
    apply (case_tac xs)
    apply auto
    done
    
  lemma tkd: "decr (take_decr xs)"
    apply (induction xs rule: take_decr.induct)
    apply auto
    apply (case_tac xs)
    apply auto
    done
  
  lemma icod: "incr (take xs) ∨ decr (take xs)"
    apply (cases xs rule: take.cases) 
    apply (auto simp: tki tkd simp del: take_incr.simps take_decr.simps)
    done   
        
  theorem cuts_incr_decr: "∀c∈set (cuts xs). incr c ∨ decr c"  
    apply (induction xs rule: cuts.induct)
    apply (subst cuts.simps)
    apply (auto simp: take2_def Let_def)
    using icod by blast
    
      
  subsubsection ‹Property 3: Maximality›      
  text ‹Specification of a cut that consists of maximal segments:
    The segements are non-empty, and for every two neighbouring segments,
    the first value of the last segment cannot be used to continue the first segment:
  ›
  fun maxi where
     "maxi [] ⟷ True"
   | "maxi [c] ⟷ c≠[]"
   | "maxi (c1#c2#cs) ⟷ (c1≠[] ∧ c2≠[] ∧ maxi (c2#cs) ∧ ( 
        incr c1 ∧ ¬(last c1 < hd c2) 
      ∨ decr c1 ∧ ¬(last c1 ≥ hd c2)        
        ))"  

  text ‹Obviously, our specification implies that there are no 
    empty segments›    
  lemma maxi_imp_non_empty: "maxi xs ⟹ []∉set xs"  
    by (induction xs rule: maxi.induct) auto
        
          
  lemma tdconc': "xs≠[] ⟹ 
    ∃ys. xs = take_decr xs @ ys ∧ (ys≠[] 
      ⟶ ¬(last (take_decr xs) ≥ hd ys))"
    apply (induction xs rule: take_decr.induct)
    apply auto
    apply (case_tac xs) apply (auto split: if_splits)
    done
    
  lemma ticonc': "xs≠[] ⟹ ∃ys. xs = take_incr xs @ ys ∧ (ys≠[] ⟶ ¬(last (take_incr xs) < hd ys))"
    apply (induction xs rule: take_incr.induct)
    apply auto
    apply (case_tac xs) apply (auto split: if_splits)
    done

  lemma take_conc': "xs≠[] ⟹ ∃ys. xs = take xs@ys ∧ (ys≠[] ⟶ (
    take xs=take_incr xs ∧ ¬(last (take_incr xs) < hd ys)
  ∨ take xs=take_decr xs ∧ ¬(last (take_decr xs) ≥ hd ys)  
  ))"  
    using tdconc' ticonc' 
    apply (cases xs rule: take.cases)
    by auto 
    
    
  lemma take_decr_non_empty:
    "take_decr xs ≠ []" if "xs ≠ []"
    using that
    apply (cases xs)
     apply auto
    subgoal for x ys
      apply (cases ys)
       apply (auto split: if_split_asm)
      done
    done
  
  lemma take_incr_non_empty:
    "take_incr xs ≠ []" if "xs ≠ []"
    using that
    apply (cases xs)
     apply auto
    subgoal for x ys
      apply (cases ys)
       apply (auto split: if_split_asm)
      done
    done
    
  lemma take_conc'': "xs≠[] ⟹ ∃ys. xs = take xs@ys ∧ (ys≠[] ⟶ (
    incr (take xs) ∧ ¬(last (take xs) < hd ys)
  ∨ decr (take xs) ∧ ¬(last (take xs) ≥ hd ys)  
  ))"  
    using tdconc' ticonc' tki tkd 
    apply (cases xs rule: take.cases)
    apply auto
    apply (auto simp add: take_incr_non_empty) 
    apply (simp add: take_decr_non_empty)
    apply (metis list.distinct(1) take_incr.simps(3))
    by (smt list.simps(3) take_decr.simps(3))
    
    
  
  lemma [simp]: "cuts [] = []"
    apply (subst cuts.simps) by auto
    
  lemma [simp]: "cuts xs ≠ [] ⟷ xs ≠ []"  
    apply (subst cuts.simps) 
    apply (auto simp: take2_def Let_def)
    done

  lemma inv_cuts: "cuts xs = c#cs ⟹ ∃ys. c=take xs ∧ xs=c@ys ∧ cs = cuts ys"
    apply (subst (asm) cuts.simps)
    apply (cases xs rule: cuts.cases)
    apply (auto split: if_splits simp: take2_def Let_def)
    by (metis append_eq_conv_conj take_conc)
    
  theorem maximal_cuts: "maxi (cuts xs)" 
    apply (induction "cuts xs" arbitrary: xs rule: maxi.induct)
    subgoal by auto
    subgoal for c xs
      apply (drule sym; simp)
      apply (subst (asm) cuts.simps)
      apply (auto split: if_splits prod.splits simp: take2_def Let_def take_non_empty)
      done
    subgoal for c1 c2 cs xs
      apply (drule sym)
      apply simp
      apply (drule inv_cuts; clarsimp)
      apply auto
      subgoal by (metis cuts.simps list.distinct(1) take_non_empty) 
      subgoal by (metis append.left_neutral inv_cuts not_Cons_self) 
      subgoal using icod by blast 
      subgoal by (metis
            Nil_is_append_conv cuts.simps hd_append2 inv_cuts list.distinct(1)
            same_append_eq take_conc'' take_non_empty) 
      subgoal by (metis
            append_is_Nil_conv cuts.simps hd_append2 inv_cuts list.distinct(1)
            same_append_eq take_conc'' take_non_empty) 
      done
    done

  subsubsection ‹Equivalent Formulation Over Indexes›
  text ‹After the competition, we got the comment that a specification of 
    monotonic sequences via indexes might be more readable.
  
    We show that our functional specification is equivalent to a 
    specification over indexes.›
    
  fun ii_induction where
    "ii_induction [] = ()"
  | "ii_induction [_] = ()"
  | "ii_induction (_#y#xs) = ii_induction (y#xs)"      

  locale cnvSpec =
    fixes fP P
    assumes [simp]: "fP [] ⟷ True"
    assumes [simp]: "fP [x] ⟷ True"
    assumes [simp]: "fP (a#b#xs) ⟷ P a b ∧ fP (b#xs)"
  begin

    lemma idx_spec: "fP xs ⟷ (∀i<length xs - 1. P (xs!i) (xs!Suc i))"
      apply (induction xs rule: ii_induction.induct)
      using less_Suc_eq_0_disj
      by auto
  
  end

  locale cnvSpec' =
    fixes fP P P'
    assumes [simp]: "fP [] ⟷ True"
    assumes [simp]: "fP [x] ⟷ P' x"
    assumes [simp]: "fP (a#b#xs) ⟷ P' a ∧ P' b ∧ P a b ∧ fP (b#xs)"
  begin

    lemma idx_spec: "fP xs ⟷ (∀i<length xs. P' (xs!i)) ∧ (∀i<length xs - 1. P (xs!i) (xs!Suc i))"
      apply (induction xs rule: ii_induction.induct)
      apply auto []
      apply auto []
      apply clarsimp
      by (smt less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
  
  end
    
  interpretation INCR: cnvSpec incr "(<)"
    apply unfold_locales by auto
  
  interpretation DECR: cnvSpec decr "(≥)"
    apply unfold_locales by auto
  
  interpretation MAXI: cnvSpec' maxi "λc1 c2. ( ( 
        incr c1 ∧ ¬(last c1 < hd c2) 
      ∨ decr c1 ∧ ¬(last c1 ≥ hd c2)        
        ))"
      "λx. x ≠ []"  
    apply unfold_locales by auto
  
  lemma incr_by_idx: "incr xs = (∀i<length xs - 1. xs ! i < xs ! Suc i)" 
    by (rule INCR.idx_spec)
    
  lemma decr_by_idx: "decr xs = (∀i<length xs - 1. xs ! i ≥ xs ! Suc i)" 
    by (rule DECR.idx_spec)
    
  lemma maxi_by_idx: "maxi xs ⟷
    (∀i<length xs. xs ! i ≠ []) ∧
    (∀i<length xs - 1. 
         incr (xs ! i) ∧ ¬ last (xs ! i) < hd (xs ! Suc i) 
       ∨ decr (xs ! i) ∧ ¬ hd (xs ! Suc i) ≤ last (xs ! i)
    )"
    by (rule MAXI.idx_spec)

  theorem all_correct:  
    "concat (cuts xs) = xs"
    "∀c∈set (cuts xs). incr c ∨ decr c"
    "maxi (cuts xs)"
    "[] ∉ set (cuts xs)"
    using cuts_incr_decr concat_cuts maximal_cuts 
          maxi_imp_non_empty[OF maximal_cuts]
    by auto

end