feat: missing sizeOf theorems for Array.get and List.get

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

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

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