test: termination checking and duplicated terms (#2993)

These tests came out of #2981 and #2982; let’s have them in master even
if the changes there will not happen right away.

tests/lean/issue2981.lean

@@ -0,0 +1,27 @@
+/-!
+Terms are often duplicated in lean. One example is default arguments
+referring to earlier ones; observed in the wild with `Array.foldl` and friends.
+
+Ideally, compiling a recursive definition will still only consider such a recursive call once.
+-/
+
+def dup (a : Nat) (b : Nat := a) := a + b
+
+namespace TestingFix
+
+def rec : Nat → Nat
+ | 0 => 1
+ | n+1 => dup (dup (dup (rec n)))
+decreasing_by trace "Tactic is run (ideally only once)"; decreasing_tactic
+
+end TestingFix
+
+namespace TestingGuessLex
+
+-- GuessLex should run the tactic an extra time, that is expected
+def rec : Nat → Nat → Nat
+ | 0, _m => 1
+ | n+1, m => dup (dup (dup (rec n (m + 1))))
+decreasing_by trace "Tactic is run (ideally only twice)"; decreasing_tactic
+
+end TestingGuessLex

tests/lean/issue2981.lean.expected.out

@@ -0,0 +1,24 @@
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only once)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)
+Tactic is run (ideally only twice)

tests/lean/run/issue2982.lean

@@ -0,0 +1,59 @@
+/-!
+If the recursive call is passed to the `case` tactic, it
+gets duplicate fairly often, and into different contexts
+(see below)
+So let us construct proofs that depend on that context,
+to check that the proofs are not confused.
+
+A work-around is
+```
+  let r := foo n
+  cases r
+```
+-/
+
+-- set_option trace.Elab.definition.wf true
+def foo : (n : Nat) → ∃ m, m > n
+ | 0 => ⟨1, Nat.zero_lt_one⟩
+ | n+1 => by
+  cases foo n
+  · case _ m hm => exact ⟨m+1, Nat.succ_lt_succ hm⟩
+decreasing_by
+
+  -- trace_state
+  solve
+  | have this_is_in_the_context : ∃ m, m > n := by assumption
+    cases this_is_in_the_context
+    exact Nat.lt_succ_self _
+  | exact Nat.lt_succ_self _
+
+
+/-
+[Elab.definition.wf] replaceRecApps:
+      match n with
+      | 0 => Exists.intro 1 Nat.zero_lt_one
+      | Nat.succ n =>
+        Exists.casesOn (motive := fun t => foo n = t → ∃ m, m > n + 1) (foo n)
+          (fun w h h_1 => Exists.intro (w + 1) (Nat.succ_lt_succ h)) (Eq.refl (foo n))
+-/
+
+/-
+
+Contexts
+
+n: Nat
+x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
+t✝: ∃ m, m > n
+⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+n: Nat
+x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
+⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+n: Nat
+x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
+w✝: Nat
+h✝: w✝ > n
+⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+n: Nat
+x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
+⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
+-/