Changes

1 changed files (+4/-8)

• Long.lean > Manual.lean
  • @@ -18,8 +18,7 @@ def Sorted : List α → Prop
    | [] | [_] => True | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) - theorem insSorted (a : α) (xs : List α) : - Sorted xs → Sorted (ins a xs) := by + theorem insSorted (a : α) (xs : List α) : Sorted xs → Sorted (ins a xs) := by induction xs case nil => simp [Sorted, ins] case cons x xs ih =>
  • @@ -46,16 +45,14 @@ · have ih₂ := ih h₄
    simp only [ins, h₂, ↓reduceIte] at ih₂ exact ih₂ - theorem insSortSorted (xs : List α) : - Sorted xs.insSort := by + theorem insSortSorted (xs : List α) : Sorted xs.insSort := by induction xs case nil => simp [List.insSort, Sorted] case cons x xs ih => rw [List.insSort] exact (insSorted x xs.insSort) ih - theorem insPerm (xs : List α) (a : α) : - List.Perm (a :: xs) (ins a xs) := by + theorem insPerm (xs : List α) (a : α) : List.Perm (a :: xs) (ins a xs) := by induction xs case nil => rw [ins] case _ x xs ih =>
  • @@ -65,8 +62,7 @@ · simp [h₁]
    · simp only [h₁] exact .trans (.swap x a xs) (.cons x ih) - theorem insSortPerm (xs : List α) : - List.Perm xs xs.insSort := by + theorem insSortPerm (xs : List α) : List.Perm xs xs.insSort := by induction xs case nil => rw [List.insSort] case cons h t ih =>