From c5fdd54cd8ad04fe00726ad8f23545cfa276146a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Feb 2022 10:02:27 -0800
Subject: [PATCH] feat: support for acyclicity at `unifyEqs`

closes #1022
---
 RELEASES.md                       |  2 ++
 src/Lean/Meta/Tactic/Acyclic.lean | 55 +++++++++++++++++++++++++++++++
 src/Lean/Meta/Tactic/Cases.lean   |  4 ++-
 tests/lean/run/1022.lean          | 30 +++++++++++++++++
 4 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 src/Lean/Meta/Tactic/Acyclic.lean
 create mode 100644 tests/lean/run/1022.lean

diff --git a/RELEASES.md b/RELEASES.md
index 132c211b3b..f508cecbc6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -86,3 +86,5 @@ termination_by' measure fun ⟨i, _⟩ => as.size - i
 * Add `arith` option to `Simp.Config`, the macro `simp_arith` expands to `simp (config := { arith := true })`. Only `Nat` and linear arithmetic is currently supported.
 
 * Add `fail msg?` tactic that always fail.
+
+* Add support for acyclicity at dependent elimination. See [issue #1022](https://github.com/leanprover/lean4/issues/1022).
diff --git a/src/Lean/Meta/Tactic/Acyclic.lean b/src/Lean/Meta/Tactic/Acyclic.lean
new file mode 100644
index 0000000000..c163e49ed7
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Acyclic.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.MatchUtil
+import Lean.Meta.Tactic.Simp.Main
+
+namespace Lean.Meta
+
+private def isTarget (lhs rhs : Expr) : MetaM Bool := do
+  if !lhs.isFVar || !lhs.occurs rhs then
+    return false
+  else
+    return rhs.isConstructorApp (← getEnv)
+
+/--
+  Close the given goal if `h` is a proof for an equality such as `as = a :: as`.
+  Inductive datatypes in Lean are acyclic.
+-/
+def acyclic (mvarId : MVarId) (h : Expr) : MetaM Bool := withMVarContext mvarId do
+  let type ← whnfD (← inferType h)
+  trace[Meta.Tactic.acyclic] "type: {type}"
+  let some (_, lhs, rhs) := type.eq? | return false
+  if (← isTarget lhs rhs) then
+    go h lhs rhs
+  else if (← isTarget rhs lhs) then
+    go (← mkEqSymm h) rhs lhs
+  else
+    return false
+where
+  go (h lhs rhs : Expr) : MetaM Bool := do
+    try
+      let sizeOf_lhs ← mkAppM ``sizeOf #[lhs]
+      let sizeOf_rhs ← mkAppM ``sizeOf #[rhs]
+      let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
+      let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
+      -- TODO: we only need the `sizeOf` simp theorems
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := (← getSimpTheorems) }) with
+      | some _ => return false
+      | none   =>
+        let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)
+        let hlt_self ← mkAppM ``Nat.lt_of_lt_of_eq #[hlt, heq]
+        let hlt_irrelf ← mkAppM ``Nat.lt_irrefl #[sizeOf_lhs]
+        assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkApp hlt_irrelf hlt_self))
+        trace[Meta.Tactic.acyclic] "succeeded"
+        return true
+    catch ex =>
+      trace[Meta.Tactic.acyclic] "failed with\n{ex.toMessageData}"
+      return false
+
+builtin_initialize
+  registerTraceClass `Meta.Tactic.acyclic
+
+end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index 968bac7522..141783c631 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Injection
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Subst
+import Lean.Meta.Tactic.Acyclic
 
 namespace Lean.Meta
 
@@ -228,13 +229,14 @@ partial def unifyEqs (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseN
           /- Remark: we use `let rec` here because otherwise the compiler would generate an insane amount of code.
             We can remove the `rec` after we fix the eagerly inlining issue in the compiler. -/
           let rec substEq (symm : Bool) := do
-            /- TODO: support for acyclicity (e.g., `xs ≠ x :: xs`) -/
             /- Remark: `substCore` fails if the equation is of the form `x = x` -/
             if let some (substNew, mvarId) ← observing? (substCore mvarId eqFVarId symm subst) then
               unifyEqs (numEqs - 1) mvarId substNew caseName?
             else if (← isDefEq a b) then
               /- Skip equality -/
               unifyEqs (numEqs - 1) (← clear mvarId eqFVarId) subst caseName?
+            else if (← acyclic mvarId (mkFVar eqFVarId)) then
+              pure none -- this alternative has been solved
             else
               throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
           let rec injection (a b : Expr) := do
diff --git a/tests/lean/run/1022.lean b/tests/lean/run/1022.lean
new file mode 100644
index 0000000000..d0fc778dbf
--- /dev/null
+++ b/tests/lean/run/1022.lean
@@ -0,0 +1,30 @@
+namespace STLC
+
+abbrev Var := Char
+
+inductive type where
+  | base  : type
+  | arrow : type → type → type
+
+inductive term where
+  | var : Var → term
+  | lam : Var → type → term → term
+  | app : term → term → term
+
+def ctx := List (Var × type)
+
+open type term in
+inductive typing : ctx → term → type → Prop where
+  | var  : typing ((x, A) :: Γ) (var x) A -- simplified
+  | arri : typing ((x, A) :: Γ) M B → typing Γ (lam x A M) (arrow A B)
+  | arre : typing Γ M (arrow A B) → typing Γ N A → typing Γ (app M N) B
+
+open type term in
+theorem no_δ : ¬ ∃ A B, typing nil (lam x A (app (var x) (var x))) (arrow A B) :=
+  fun h => match h with
+  | Exists.intro A (Exists.intro B h) => match h with
+    | typing.arri h => match h with
+      | typing.arre (A := T) h₁ h₂ => match h₂ with
+        | typing.var => nomatch h₁
+
+namespace STLC