From cf4e8739744ec0b8b5259162dfbf985501cec072 Mon Sep 17 00:00:00 2001
From: Daniel Fabian <daniel.fabian@integral-it.ch>
Date: Wed, 9 Mar 2022 21:44:25 +0000
Subject: [PATCH] feat: support Sort u in ac_refl.

---
 src/Init/Core.lean                |  8 ++++----
 src/Init/Data/AC.lean             | 12 ++++++------
 src/Lean/Meta/Tactic/AC/Main.lean |  2 +-
 tests/lean/run/ac_refl.lean       | 18 +++++++++++++++++-
 4 files changed, 28 insertions(+), 12 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index d6791b0483..979732db78 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1112,16 +1112,16 @@ constant reduceNat (n : Nat) : Nat := n
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b)    : a = b
 
-class IsAssociative (op : α → α → α) where
+class IsAssociative {α : Sort u} (op : α → α → α) where
   assoc : (a b c : α) → op (op a b) c = op a (op b c)
 
-class IsCommutative (op : α → α → α) where
+class IsCommutative {α : Sort u} (op : α → α → α) where
   comm : (a b : α) → op a b = op b a
 
-class IsIdempotent (op : α → α → α) where
+class IsIdempotent {α : Sort u} (op : α → α → α) where
   idempotent : (x : α) → op x x = x
 
-class IsNeutral (op : α → α → α) (neutral : α) where
+class IsNeutral {α : Sort u} (op : α → α → α) (neutral : α) where
   left_neutral : (a : α) → op neutral a = a
   right_neutral : (a : α) → op a neutral = a
 
diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean
index 39d8efa642..ef5bbdaf9f 100644
--- a/src/Init/Data/AC.lean
+++ b/src/Init/Data/AC.lean
@@ -14,11 +14,11 @@ inductive Expr
   | op (lhs rhs : Expr)
   deriving Inhabited, Repr, BEq
 
-structure Variable (op : α → α → α) where
+structure Variable {α : Sort u} (op : α → α → α) : Type u where
   value : α
   neutral : Option $ IsNeutral op value
 
-structure Context (α : Type u) where
+structure Context (α : Sort u) where
   op : α → α → α
   assoc : IsAssociative op
   comm : Option $ IsCommutative op
@@ -26,12 +26,12 @@ structure Context (α : Type u) where
   vars : List (Variable op)
   arbitrary : α
 
-class ContextInformation (α : Type u) where
+class ContextInformation (α : Sort u) where
   isNeutral : α → Nat → Bool
   isComm : α → Bool
   isIdem : α → Bool
 
-class EvalInformation (α : Type u) (β : Type v) where
+class EvalInformation (α : Sort u) (β : Sort v) where
   arbitrary : α → β
   evalOp : α → β → β → β
   evalVar : α → Nat → β
@@ -49,7 +49,7 @@ instance : EvalInformation (Context α) α where
   evalOp ctx := ctx.op
   evalVar ctx idx := ctx.var idx |>.value
 
-def eval (β : Type u) [EvalInformation α β] (ctx : α) : (ex : Expr) → β
+def eval (β : Sort u) [EvalInformation α β] (ctx : α) : (ex : Expr) → β
   | Expr.var idx => EvalInformation.evalVar ctx idx
   | Expr.op l r => EvalInformation.evalOp ctx (eval β ctx l) (eval β ctx r)
 
@@ -57,7 +57,7 @@ def Expr.toList : Expr → List Nat
   | Expr.var idx => [idx]
   | Expr.op l r => l.toList.append r.toList
 
-def evalList (β : Type u) [EvalInformation α β] (ctx : α) : List Nat → β
+def evalList (β : Sort u) [EvalInformation α β] (ctx : α) : List Nat → β
   | [] => EvalInformation.arbitrary ctx
   | [x] => EvalInformation.evalVar ctx x
   | x :: xs => EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList β ctx xs)
diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index c080a33fce..1a3096f4c5 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -93,7 +93,7 @@ def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr ×
   let rhs ← convert acExprNormed
   let α ← inferType vars[0]
   let u ← getLevel α
-  let proof := mkAppN (mkConst ``Context.eq_of_norm [u.dec.get!]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
+  let proof := mkAppN (mkConst ``Context.eq_of_norm [u]) #[α, context, lhs, rhs, ←mkEqRefl (mkConst ``Bool.true)]
   return (proof, tgt)
 where
   mkContext (vars : Array Expr) : MetaM (Array Bool × Expr) := do
diff --git a/tests/lean/run/ac_refl.lean b/tests/lean/run/ac_refl.lean
index abe6393330..11ad669e09 100644
--- a/tests/lean/run/ac_refl.lean
+++ b/tests/lean/run/ac_refl.lean
@@ -33,6 +33,22 @@ instance : IsCommutative (α := Nat) max := ⟨max_comm⟩
 instance : IsIdempotent (α := Nat) max := ⟨max_idem⟩
 instance : IsNeutral max 0 := ⟨Nat.zero_max, Nat.max_zero⟩
 
+instance : IsAssociative And := ⟨λ p q r => propext ⟨λ ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩, λ ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩⟩⟩
+instance : IsCommutative And := ⟨λ p q => propext ⟨λ ⟨hp, hq⟩ => ⟨hq, hp⟩, λ ⟨hq, hp⟩ => ⟨hp, hq⟩⟩⟩
+instance : IsIdempotent And := ⟨λ p => propext ⟨λ ⟨hp, _⟩ => hp, λ hp => ⟨hp, hp⟩⟩⟩
+instance : IsNeutral And True :=
+  ⟨λ p => propext ⟨λ ⟨_, hp⟩ => hp, λ hp => ⟨True.intro, hp⟩⟩, λ p => propext ⟨λ ⟨hp, _⟩ => hp, λ hp => ⟨hp, True.intro⟩⟩⟩
+
+theorem or_assoc (p q r : Prop) : ((p ∨ q) ∨ r) = (p ∨ q ∨ r) :=
+  propext ⟨λ hpqr => hpqr.elim (λ hpq => hpq.elim Or.inl $ λ hq => Or.inr $ Or.inl hq) $ λ hr => Or.inr $ Or.inr hr,
+    λ hpqr => hpqr.elim (λ hp => Or.inl $ Or.inl hp) $ λ hqr => hqr.elim (λ hq => Or.inl $ Or.inr hq) Or.inr⟩
+
+instance : IsAssociative Or := ⟨or_assoc⟩
+instance : IsCommutative Or := ⟨λ p q => propext ⟨λ hpq => hpq.elim Or.inr Or.inl, λ hqp => hqp.elim Or.inr Or.inl⟩⟩
+instance : IsIdempotent Or := ⟨λ p => propext ⟨λ hp => hp.elim id id, Or.inl⟩⟩
+instance : IsNeutral Or False :=
+  ⟨λ p => propext ⟨λ hfp => hfp.elim False.elim id, Or.inr⟩, λ p => propext ⟨λ hpf => hpf.elim id False.elim, Or.inl⟩⟩
+
 example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by ac_refl
 
 example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by ac_refl
@@ -64,5 +80,5 @@ theorem ex₃ (n : Nat) : (fun x => n + x) = (fun x => x + n) := by
 #print ex₃
 
 -- Repro: the Prop universe doesn't work
-example (p q : Prop) : p ∨ p ∨ q ∧ True = q ∨ p := by
+example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by
   ac_refl