From 03ec8cb30beefbf7ce84513e75376d5a192a3fbe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Apr 2022 16:04:46 -0700
Subject: [PATCH] feat: missing `sizeOf` theorems for `Array.get` and
 `List.get`

---
 src/Init/Data/Array/Mem.lean                 |  7 +++++++
 src/Init/Data/List/BasicAux.lean             |  8 ++++++++
 tests/lean/run/missingSizeOfArrayGetThm.lean | 17 +++++++++++++++++
 3 files changed, 32 insertions(+)
 create mode 100644 tests/lean/run/missingSizeOfArrayGetThm.lean

diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index b9d7ce7b74..8dccc1086c 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
+import Init.Data.List.BasicAux
 
 theorem List.sizeOf_get_lt [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
   match as, i with
@@ -40,4 +41,10 @@ theorem sizeOf_lt_of_mem [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈
   apply aux 0 h
 termination_by aux j _ => as.size - j
 
+@[simp] theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+  cases as
+  simp [get]
+  apply Nat.lt_trans (List.sizeOf_get ..)
+  simp_arith
+
 end Array
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 7b4586d80d..1877c76a46 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -145,4 +145,12 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
   next => apply append_cancel_right
   next => intro h; simp [h]
 
+@[simp] theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+  match as, i with
+  | a::as, ⟨0, _⟩  => simp_arith [get]
+  | a::as, ⟨i+1, h⟩ =>
+    have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
+    apply Nat.lt_trans ih
+    simp_arith
+
 end List
diff --git a/tests/lean/run/missingSizeOfArrayGetThm.lean b/tests/lean/run/missingSizeOfArrayGetThm.lean
new file mode 100644
index 0000000000..e518b2ac0d
--- /dev/null
+++ b/tests/lean/run/missingSizeOfArrayGetThm.lean
@@ -0,0 +1,17 @@
+inductive Node (Data : Type) : Type where
+| empty : Node Data
+| node  (children : Array (Node Data)) : Node Data
+| leaf  (data : Data) : Node Data
+
+def Node.FixedBranching (n : Nat) : Node Data → Prop
+  | empty => True
+  | node children => children.size = n ∧ ∀ i, (children.get i).FixedBranching n
+  | leaf _ => True
+decreasing_by
+  simp_wf
+  apply Nat.lt_trans (Array.sizeOf_get ..) -- TODO: remove after we add linarith
+  simp_arith
+
+structure MNode (Data : Type) (m : Nat) where
+  node : Node Data
+  fix_branching : node.FixedBranching m