From 8af59af336c93f21bde6033aacecdb0f914785a5 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Thu, 3 Apr 2025 23:31:28 -0400
Subject: [PATCH] list_insert_sorted
---
Invariant.lean | 23 ++++++++++++-----------
1 file changed, 12 insertions(+), 11 deletions(-)
diff --git a/Invariant.lean b/Invariant.lean
index edb75cf..13f2426 100644
--- a/Invariant.lean
+++ b/Invariant.lean
@@ -50,19 +50,20 @@ theorem list_insert_sorted (hs : List.Sorted (·<·) xs) : List.Sorted (·<·) (
split
· exact List.Sorted.of_cons hs
· split
- · rename_i hnlt
- exact List.Sorted.cons hnlt hs
+ · exact List.Sorted.cons ‹_› hs
+ · have : a < x := by
+ rename_i hne hnlt
+ apply Nat.lt_of_le_of_ne
+ exact Nat.le_of_not_lt hnlt
+ exact fun a_1 => hne (Eq.symm a_1)
- have : a < x := by
- rename_i hne hnlt
- apply Nat.lt_of_le_of_ne
- exact Nat.le_of_not_lt hnlt
- exact fun a_1 => hne (Eq.symm a_1)
+ simp only [List.sorted_cons]
- have h : List.Sorted (·<·) as := List.Sorted.of_cons hs
-
- have := ih h
- sorry
+ constructor
+ · intro b hmem
+ cases list_insert_mem hmem
+ <;> simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
+ · simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
def insert (x : ℕ) : NatSet → NatSet
| ⟨[], _⟩ => singleton x