diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BitVec.lean | 4 | ||||
| -rw-r--r-- | Common/List.lean | 13 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 |
3 files changed, 10 insertions, 9 deletions
diff --git a/Common/BitVec.lean b/Common/BitVec.lean index ad46efb..31af340 100644 --- a/Common/BitVec.lean +++ b/Common/BitVec.lean @@ -1,8 +1,8 @@ def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := - a ||| BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]) + a ||| BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]) def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := - a &&& BitVec.not (BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])) + a &&& BitVec.not (BitVec.ofNatLT (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])) def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n := if v then diff --git a/Common/List.lean b/Common/List.lean index 704f8b2..1c8f4a6 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -10,19 +10,20 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length simp constructor assumption - | true => simp_arith[hi] + | true => simp[hi] def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α | [] => [] | a :: as => let smallerPred := λ b ↦ pred b a let largerEqualPred := not ∘ smallerPred - have : List.length (List.filter smallerPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] - have : List.length (List.filter largerEqualPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] let smallers := as.filter smallerPred let biggers := as.filter largerEqualPred (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers) termination_by l => l.length + decreasing_by + all_goals + simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList] def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt @@ -86,7 +87,7 @@ protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : Li case cons l ls hi => unfold mapWithProof.worker have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc) - simp_arith[←hi] + simp +arith[←hi] theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length := List.length_mapWithProof_Aux list f [] @@ -95,8 +96,8 @@ theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ [] theorem mapWithProof_neNilIffNeNil {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list ≠ [] ↔ (list.mapWithProof f) ≠ [] := ⟨ - λh₁ ↦ List.length_pos.mp $ length_mapWithProof.subst (List.length_pos.mpr h₁), - λh₁ ↦ List.length_pos.mp $ length_mapWithProof.substr (List.length_pos.mpr h₁) + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.subst (List.length_pos_iff.mpr h₁), + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.substr (List.length_pos_iff.mpr h₁) ⟩ theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] := diff --git a/Common/Parsing.lean b/Common/Parsing.lean index b1ee779..8237613 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -103,7 +103,7 @@ instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where have : x + e.width *y < e.elements.size := by simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂ rw[e.size_valid] - exact Nat.two_d_coordinate_to_index_lt_size h₁.right.left h₂.right.left + exact Nat.two_d_coordinate_to_index_lt_size h₁.left h₂.left r := r ++ (ToString.toString e.elements[x+e.width*y]) r |