diff options
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index ce9c3e2..8222879 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -31,10 +31,10 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N case isFalse goRight => dsimp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, Fin.isValue] cases r -- to work around cast - case leaf => simp (config:={ground:=true}) at goRight; exact absurd goRight.symm n_m_not_zero + case leaf => simp +ground at goRight; exact absurd goRight.symm n_m_not_zero case branch rv rl rr rm_le_n rmax_height_difference rsubtree_full => rw[get_right, right_unfold] - case h₂ => simp_arith[leftLen_unfold] + case h₂ => simp +arith[leftLen_unfold] simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, leftLen_unfold] have : ∀(a : Nat), a + n + 1 - n - 1 = a := λa↦(Nat.add_sub_cancel _ _).subst $ (Nat.add_assoc a n 1).subst (motive := λx↦a+n+1-n-1 = x-(n+1)) $ (Nat.sub_sub (a+n+1) n 1).subst rfl simp only[this] @@ -76,7 +76,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => @@ -111,7 +111,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u} simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => @@ -258,7 +258,7 @@ else simp only [h₃, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢ case zero => - simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ + simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ subst o contradiction case succ pp _ _ _ _ => @@ -348,7 +348,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea simp only [h₄, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄ + simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄ subst o contradiction case succ pp _ _ _ _ => |