From e4f2c39ab26e8c8f7d3e59578a1bd532d2ddfb95 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 29 Nov 2023 16:40:57 +0100
Subject: [PATCH] test: termination checking and duplicated terms (#2993)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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              | 27 ++++++++++++
 tests/lean/issue2981.lean.expected.out | 24 +++++++++++
 tests/lean/run/issue2982.lean          | 59 ++++++++++++++++++++++++++
 3 files changed, 110 insertions(+)
 create mode 100644 tests/lean/issue2981.lean
 create mode 100644 tests/lean/issue2981.lean.expected.out
 create mode 100644 tests/lean/run/issue2982.lean

diff --git a/tests/lean/issue2981.lean b/tests/lean/issue2981.lean
new file mode 100644
index 0000000000..47944aa03f
--- /dev/null
+++ b/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
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
new file mode 100644
index 0000000000..4a83ac3f35
--- /dev/null
+++ b/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)
diff --git a/tests/lean/run/issue2982.lean b/tests/lean/run/issue2982.lean
new file mode 100644
index 0000000000..6bca320f31
--- /dev/null
+++ b/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)
+-/