From cb3a2f7947f172bdfc945d99e68ccdf3105ae66a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Nov 2020 08:46:45 -0800
Subject: [PATCH] test: add coercion pullback example from "Hints in
 Unification"

---
 tests/lean/run/unifhint3.lean | 69 +++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 tests/lean/run/unifhint3.lean

diff --git a/tests/lean/run/unifhint3.lean b/tests/lean/run/unifhint3.lean
new file mode 100644
index 0000000000..edb8b56ee5
--- /dev/null
+++ b/tests/lean/run/unifhint3.lean
@@ -0,0 +1,69 @@
+/- Coercion pullback example from the paper "Hints in Unification" -/
+
+universes u
+
+structure Monoid where
+  α    : Type u
+  op   : α → α → α
+  unit : α
+
+structure Group where
+  α    : Type u
+  op   : α → α → α
+  unit : α
+  inv : α → α
+
+structure Ring where
+  α    : Type u
+  mul  : α → α → α
+  add  : α → α → α
+  neg  : α → α
+  one  : α
+  zero : α
+
+def Group.ofRing (r : Ring) : Group where
+  α    := r.α
+  op   := r.add
+  inv  := r.neg
+  unit := r.zero
+
+def Monoid.ofRing (r : Ring) : Monoid where
+  α    := r.α
+  op   := r.mul
+  unit := r.one
+
+instance : CoeSort Ring (Type u) where
+  coe s := s.α
+
+instance : CoeSort Monoid (Type u) where
+  coe s := s.α
+
+instance : CoeSort Group (Type u) where
+  coe s := s.α
+
+def gop {s : Group} (a b : s) : s :=
+  s.op a b
+
+def mop {s : Monoid} (a b : s) : s :=
+  s.op a b
+
+infix:70 [1] "*" => mop
+infix:65 [1] "+" => gop
+
+unif_hint (r : Ring) (g : Group) where
+  g =?= Group.ofRing r
+  |-
+  r.α =?= g.α
+
+unif_hint (r : Ring) (m : Monoid) where
+  m =?= Monoid.ofRing r
+  |-
+  r.α =?= m.α
+
+def distrib {r : Ring} (a b c : r) := a * (b + c) = a * b + a * c
+
+theorem ex1 {r : Ring} (a b c : r) : distrib a b c = (a * (b + c) = a * b + a * c) :=
+  rfl
+
+theorem ex2 {r : Ring} (a b c : r) : distrib a b c = (mop a (gop b c) = gop (mop a b) (mop a c)) :=
+  rfl