fix: array_get_dec etc. tactics to solve more cases (#5037)

Using `Nat.lt_trans` is too restrictive, and using `Nat.lt_of_lt_of_le`
should make this tactic prove more goals.

This fixes a regression probably introduced by #3991; at least in some
cases before that `apply sizeOf_get` would have solved the goal here.
And it’s true that this is now subsumed by `simp`, but because of the
order that `macro_rules` are tried, the too restrictive variant with
`Nat.lt_trans` would be tried before `simp`, without backtracking.

Fixes #5027

src/Init/Data/Array/Mem.lean

@@ -38,8 +38,8 @@ macro "array_get_dec" : tactic =>
     -- subsumed by simp
     -- | with_reducible apply sizeOf_get
     -- | with_reducible apply sizeOf_getElem
-    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
-    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp_arith
     )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -52,7 +52,7 @@ macro "array_mem_dec" : tactic =>
   `(tactic| first
     | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
     | with_reducible
-        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        apply Nat.lt_of_lt_of_le (Array.sizeOf_lt_of_mem ?h)
         case' h => assumption
       simp_arith)
 

src/Init/Data/List/BasicAux.lean

@@ -192,7 +192,7 @@ macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
     | with_reducible apply sizeOf_lt_of_mem; assumption; done
     | with_reducible
-        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
         case' h => assumption
       simp_arith)
 

tests/lean/run/issue5027.lean

@@ -0,0 +1,16 @@
+inductive Term (α: Type): Type where
+  | Composite : Array (Term α) → Term α
+  | Atom: α → Term α
+
+-- height of a term
+def height (f: Term α): Nat :=
+  let rec max_height (a: Array (Term α)) (i: Nat) (m: Nat): Nat :=
+    if h: i < a.size then
+      -- The recusive call to height used to fail because of a too weak
+      -- array_get_dec
+      max_height a (i + 1) (max (height a[i]) m)
+    else
+      m
+  match f with
+  | .Composite a => 1 + max_height a 0 0
+  | .Atom _ => 1