Rice's theorem

Cslib/Foundations/Semantics/ReductionSystem/Basic.lean

@@ -46,11 +46,15 @@ open Relation Relation.ReflTransGen
 instance (rs : ReductionSystem Term) : Trans rs.Red rs.MRed rs.MRed := by infer_instance
 instance (rs : ReductionSystem Term) : Trans rs.MRed rs.Red rs.MRed := by infer_instance
 
+instance (rs : ReductionSystem Term) : IsTrans Term rs.MRed := by infer_instance
+instance (rs : ReductionSystem Term) : Transitive rs.MRed := transitive_of_trans rs.MRed
+instance (rs : ReductionSystem Term) : Trans rs.MRed rs.MRed rs.MRed := instTransOfIsTrans
+
 end MultiStep
 
 open Lean Elab Meta Command Term
 
--- thank you to Kyle Miller for this: 
+-- thank you to Kyle Miller for this:
 -- https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/Working.20with.20variables.20in.20a.20command/near/529324084
 
 /-- A command to create a `ReductionSystem` from a relation, robust to use of `variable `-/
@@ -81,10 +85,10 @@ elab "create_reduction_sys" rel:ident name:ident : command => do
       }
       addTermInfo' name (.const name.getId params) (isBinder := true)
       addDeclarationRangesFromSyntax name.getId name
- 
-/-- 
+
+/--
   This command adds notations for a `ReductionSystem.Red` and `ReductionSystem.MRed`. This should
-  not usually be called directly, but from the `reduction_sys` attribute. 
+  not usually be called directly, but from the `reduction_sys` attribute.
 
   As an example `reduction_notation foo "β"` will add the notations "⭢β" and "↠β".
 
@@ -94,19 +98,19 @@ elab "create_reduction_sys" rel:ident name:ident : command => do
 -/
 syntax "reduction_notation" ident (str)? : command
 macro_rules
-  | `(reduction_notation $rs $sym) => 
+  | `(reduction_notation $rs $sym) =>
     `(
       notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red  $rs) t t'
       notation3 t:39 " ↠" $sym:str t':39 => (ReductionSystem.MRed $rs) t t'
      )
-  | `(reduction_notation $rs) => 
+  | `(reduction_notation $rs) =>
     `(
-      notation3 t:39 " ⭢" t':39 => (ReductionSystem.Red  $rs) t t'
-      notation3 t:39 " ↠" t':39 => (ReductionSystem.MRed $rs) t t'
+      notation3 t:39 " ⭢ " t':39 => (ReductionSystem.Red  $rs) t t'
+      notation3 t:39 " ↠ " t':39 => (ReductionSystem.MRed $rs) t t'
      )
 
 
-/-- 
+/--
   This attribute calls the `reduction_notation` command for the annotated declaration, such as in:
 
   ```

Cslib/Languages/CombinatoryLogic/Basic.lean

@@ -61,7 +61,7 @@ def Polynomial.eval {n : Nat} (Γ : SKI.Polynomial n) (l : List SKI) (hl : List.
 def Polynomial.varFreeToSKI (Γ : SKI.Polynomial 0) : SKI := Γ.eval [] (by trivial)
 
 /-- Inductively define a polynomial `Γ'` so that (up to the fact that we haven't
-defined reduction on polynomials) `Γ' ⬝ t ⇒* Γ[xₙ ← t]`. -/
+defined reduction on polynomials) `Γ' ⬝ t ↠ Γ[xₙ ← t]`. -/
 def Polynomial.elimVar {n : Nat} : SKI.Polynomial (n+1) → SKI.Polynomial n
   /- The K-combinator leaves plain terms unchanged by substitution `K ⬝ x ⬝ t ⇒ x` -/
   | SKI.Polynomial.term x => K ⬝' x
@@ -83,7 +83,7 @@ for the inner variables.
 -/
 theorem Polynomial.elimVar_correct {n : Nat} (Γ : SKI.Polynomial (n + 1)) {ys : List SKI}
     (hys : ys.length = n) (z : SKI) :
-    Γ.elimVar.eval ys hys ⬝ z ⇒* Γ.eval (ys ++ [z])
+    (Γ.elimVar.eval ys hys ⬝ z) ↠ Γ.eval (ys ++ [z])
       (by rw [List.length_append, hys, List.length_singleton])
     := by
   match n, Γ with
@@ -125,13 +125,13 @@ def Polynomial.toSKI {n : Nat} (Γ : SKI.Polynomial n) : SKI :=
 
 /-- Correctness for the toSKI (bracket abstraction) algorithm. -/
 theorem Polynomial.toSKI_correct {n : Nat} (Γ : SKI.Polynomial n) (xs : List SKI)
-    (hxs : xs.length = n) : Γ.toSKI.applyList xs ⇒* Γ.eval xs hxs := by
+    (hxs : xs.length = n) : Γ.toSKI.applyList xs ↠ Γ.eval xs hxs := by
   match n with
   | 0 =>
     unfold toSKI varFreeToSKI applyList
     rw [List.length_eq_zero_iff] at hxs
     simp_rw [hxs, List.foldl_nil]
-    apply MRed.refl
+    rfl
   | n+1 =>
     -- show that xs = ys + [z]
     have : xs ≠ [] := List.ne_nil_of_length_eq_add_one hxs
@@ -165,63 +165,63 @@ choose a descriptive name.
 def RPoly : SKI.Polynomial 2 := &1 ⬝' &0
 /-- A SKI term representing R -/
 def R : SKI := RPoly.toSKI
-theorem R_def (x y : SKI) : R ⬝ x ⬝ y ⇒* y ⬝ x :=
+theorem R_def (x y : SKI) : (R ⬝ x ⬝ y) ↠ y ⬝ x :=
   RPoly.toSKI_correct [x, y] (by simp)
 
 
 /-- Composition: B := λ f g x. f (g x) -/
 def BPoly : SKI.Polynomial 3 := &0 ⬝' (&1 ⬝' &2)
 /-- A SKI term representing B -/
 def B : SKI := BPoly.toSKI
-theorem B_def (f g x : SKI) : B ⬝ f ⬝ g ⬝ x ⇒* f ⬝ (g ⬝ x) :=
+theorem B_def (f g x : SKI) : (B ⬝ f ⬝ g ⬝ x) ↠ f ⬝ (g ⬝ x) :=
   BPoly.toSKI_correct [f, g, x] (by simp)
 
 
 /-- C := λ f x y. f y x -/
 def CPoly : SKI.Polynomial 3 := &0 ⬝' &2 ⬝' &1
 /-- A SKI term representing C -/
 def C : SKI := CPoly.toSKI
-theorem C_def (f x y : SKI) : C ⬝ f ⬝ x ⬝ y ⇒* f ⬝ y ⬝ x :=
+theorem C_def (f x y : SKI) : (C ⬝ f ⬝ x ⬝ y) ↠ f ⬝ y ⬝ x :=
   CPoly.toSKI_correct [f, x, y] (by simp)
 
 
 /-- Rotate right: RotR := λ x y z. z x y -/
 def RotRPoly : SKI.Polynomial 3 := &2 ⬝' &0 ⬝' &1
 /-- A SKI term representing RotR -/
 def RotR : SKI := RotRPoly.toSKI
-theorem rotR_def (x y z : SKI) : RotR ⬝ x ⬝ y ⬝ z ⇒* z ⬝ x ⬝ y :=
+theorem rotR_def (x y z : SKI) : (RotR ⬝ x ⬝ y ⬝ z) ↠ z ⬝ x ⬝ y :=
   RotRPoly.toSKI_correct [x, y, z] (by simp)
 
 
 /-- Rotate left: RotR := λ x y z. y z x -/
 def RotLPoly : SKI.Polynomial 3 := &1 ⬝' &2 ⬝' &0
 /-- A SKI term representing RotL -/
 def RotL : SKI := RotLPoly.toSKI
-theorem rotL_def (x y z : SKI) : RotL ⬝ x ⬝ y ⬝ z ⇒* y ⬝ z ⬝ x :=
+theorem rotL_def (x y z : SKI) : (RotL ⬝ x ⬝ y ⬝ z) ↠ y ⬝ z ⬝ x :=
   RotLPoly.toSKI_correct [x, y, z] (by simp)
 
 
 /-- Self application: δ := λ x. x x -/
 def δPoly : SKI.Polynomial 1 := &0 ⬝' &0
 /-- A SKI term representing δ -/
 def δ : SKI := δPoly.toSKI
-theorem δ_def (x : SKI) : δ ⬝ x ⇒* x ⬝ x :=
+theorem δ_def (x : SKI) : (δ ⬝ x) ↠ x ⬝ x :=
   δPoly.toSKI_correct [x] (by simp)
 
 
 /-- H := λ f x. f (x x) -/
 def HPoly : SKI.Polynomial 2 := &0 ⬝' (&1 ⬝' &1)
 /-- A SKI term representing H -/
 def H : SKI := HPoly.toSKI
-theorem H_def (f x : SKI) : H ⬝ f ⬝ x ⇒* f ⬝ (x ⬝ x) :=
+theorem H_def (f x : SKI) : (H ⬝ f ⬝ x) ↠ f ⬝ (x ⬝ x) :=
   HPoly.toSKI_correct [f, x] (by simp)
 
 
 /-- Curry's fixed-point combinator: Y := λ f. H f (H f) -/
 def YPoly : SKI.Polynomial 1 := H ⬝' &0 ⬝' (H ⬝' &0)
 /-- A SKI term representing Y -/
 def Y : SKI := YPoly.toSKI
-theorem Y_def (f : SKI) : Y ⬝ f ⇒* H ⬝ f ⬝ (H ⬝ f) :=
+theorem Y_def (f : SKI) : (Y ⬝ f) ↠ H ⬝ f ⬝ (H ⬝ f) :=
   YPoly.toSKI_correct [f] (by simp)
 
 
@@ -239,29 +239,29 @@ rather than up to a common reduct. An alternative is to use Turing's fixed-point
 (defined below).
 -/
 def fixedPoint (f : SKI) : SKI := H ⬝ f ⬝ (H ⬝ f)
-theorem fixedPoint_correct (f : SKI) : f.fixedPoint ⇒* f ⬝ f.fixedPoint := H_def f (H ⬝ f)
+theorem fixedPoint_correct (f : SKI) : f.fixedPoint ↠ f ⬝ f.fixedPoint := H_def f (H ⬝ f)
 
 /-- Auxiliary definition for Turing's fixed-point combinator: ΘAux := λ x y. y (x x y) -/
 def ΘAuxPoly : SKI.Polynomial 2 := &1 ⬝' (&0 ⬝' &0 ⬝' &1)
 /-- A term representing ΘAux -/
 def ΘAux : SKI := ΘAuxPoly.toSKI
-theorem ΘAux_def (x y : SKI) : ΘAux ⬝ x ⬝ y ⇒* y ⬝ (x ⬝ x ⬝ y) :=
+theorem ΘAux_def (x y : SKI) : (ΘAux ⬝ x ⬝ y) ↠ y ⬝ (x ⬝ x ⬝ y) :=
   ΘAuxPoly.toSKI_correct [x, y] (by simp)
 
 
 /-- Turing's fixed-point combinator: Θ := (λ x y. y (x x y)) (λ x y. y (x x y)) -/
 def Θ : SKI := ΘAux ⬝ ΘAux
 /-- A SKI term representing Θ -/
-theorem Θ_correct (f : SKI) : Θ ⬝ f ⇒* f ⬝ (Θ ⬝ f) := ΘAux_def ΘAux f
+theorem Θ_correct (f : SKI) : (Θ ⬝ f) ↠ f ⬝ (Θ ⬝ f) := ΘAux_def ΘAux f
 
 
 /-! ### Church Booleans -/
 
 /-- A term a represents the boolean value u if it is βη-equivalent to a standard Church boolean. -/
 def IsBool (u : Bool) (a : SKI) : Prop :=
-  ∀ x y : SKI, a ⬝ x ⬝ y ⇒* (if u then x else y)
+  ∀ x y : SKI, (a ⬝ x ⬝ y) ↠ (if u then x else y)
 
-theorem isBool_trans (u : Bool) (a a' : SKI) (h : a ⇒* a') (ha' : IsBool u a') :
+theorem isBool_trans (u : Bool) (a a' : SKI) (h : a ↠ a') (ha' : IsBool u a') :
     IsBool u a := by
   intro x y
   trans a' ⬝ x ⬝ y
@@ -278,13 +278,13 @@ theorem TT_correct : IsBool true TT := fun x y ↦ MRed.K x y
 def FF : SKI := K ⬝ I
 theorem FF_correct : IsBool false FF :=
   fun x y ↦ calc
-    FF ⬝ x ⬝ y ⇒ I ⬝ y := by apply red_head; exact red_K I x
-    _         ⇒ y := red_I y
+    (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply Relation.ReflTransGen.single; apply red_head; exact red_K I x
+    _         ⭢ y := red_I y
 
 /-- Conditional: Cond x y b := if b then x else y -/
 protected def Cond : SKI := RotR
 theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) :
-    SKI.Cond ⬝ x ⬝ y ⬝ a ⇒* if u then x else y := by
+    (SKI.Cond ⬝ x ⬝ y ⬝ a) ↠ if u then x else y := by
   trans a ⬝ x ⬝ y
   · exact rotR_def x y a
   · exact h x y
@@ -302,7 +302,7 @@ theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SK
 def AndPoly : SKI.Polynomial 2 := SKI.Cond ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' FF ⬝' &0
 /-- A SKI term representing And -/
 protected def And : SKI := AndPoly.toSKI
-theorem and_def (a b : SKI) : SKI.And ⬝ a ⬝ b ⇒* SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a :=
+theorem and_def (a b : SKI) : (SKI.And ⬝ a ⬝ b) ↠ SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a :=
   AndPoly.toSKI_correct [a, b] (by simp)
 
 theorem and_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
@@ -321,7 +321,7 @@ theorem and_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool u
 def OrPoly : SKI.Polynomial 2 := SKI.Cond ⬝' TT ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' &0
 /-- A SKI term representing Or -/
 protected def Or : SKI := OrPoly.toSKI
-theorem or_def (a b : SKI) : SKI.Or ⬝ a ⬝ b ⇒* SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a :=
+theorem or_def (a b : SKI) : (SKI.Or ⬝ a ⬝ b) ↠ SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a :=
   OrPoly.toSKI_correct [a, b] (by simp)
 
 theorem or_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
@@ -350,22 +350,22 @@ def Fst : SKI := R ⬝ TT
 /-- Second projection -/
 def Snd : SKI := R ⬝ FF
 
-theorem fst_correct (a b : SKI) : Fst ⬝ (MkPair ⬝ a ⬝ b) ⇒* a := by calc
-  _ ⇒* SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
-  _ ⇒* a := cond_correct TT a b true TT_correct
+theorem fst_correct (a b : SKI) : (Fst ⬝ (MkPair ⬝ a ⬝ b)) ↠ a := by calc
+  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
+  _ ↠ a := cond_correct TT a b true TT_correct
 
-theorem snd_correct (a b : SKI) : Snd ⬝ (MkPair ⬝ a ⬝ b) ⇒* b := by calc
-  _ ⇒* SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
-  _ ⇒* b := cond_correct FF a b false FF_correct
+theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc
+  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
+  _ ↠ b := cond_correct FF a b false FF_correct
 
 /-- Unpaired f ⟨x, y⟩ := f x y, cf `Nat.unparied`. -/
 def UnpairedPoly : SKI.Polynomial 2 := &0 ⬝' (Fst ⬝' &1) ⬝' (Snd ⬝' &1)
 /-- A term representing Unpaired -/
 protected def Unpaired : SKI := UnpairedPoly.toSKI
-theorem unpaired_def (f p : SKI) : SKI.Unpaired ⬝ f ⬝ p ⇒* f ⬝ (Fst ⬝ p) ⬝ (Snd ⬝ p) :=
+theorem unpaired_def (f p : SKI) : (SKI.Unpaired ⬝ f ⬝ p) ↠ f ⬝ (Fst ⬝ p) ⬝ (Snd ⬝ p) :=
   UnpairedPoly.toSKI_correct [f, p] (by simp)
 
-theorem unpaired_correct (f x y : SKI) : SKI.Unpaired ⬝ f ⬝ (MkPair ⬝ x ⬝ y) ⇒* f ⬝ x ⬝ y := by
+theorem unpaired_correct (f x y : SKI) : (SKI.Unpaired ⬝ f ⬝ (MkPair ⬝ x ⬝ y)) ↠ f ⬝ x ⬝ y := by
   trans f ⬝ (Fst ⬝ (MkPair ⬝ x ⬝ y)) ⬝ (Snd ⬝ (MkPair ⬝ x ⬝ y))
   · exact unpaired_def f _
   · apply parallel_mRed
@@ -377,7 +377,7 @@ theorem unpaired_correct (f x y : SKI) : SKI.Unpaired ⬝ f ⬝ (MkPair ⬝ x 
 def PairPoly : SKI.Polynomial 3 := MkPair ⬝' (&0 ⬝' &2) ⬝' (&1 ⬝' &2)
 /-- A SKI term representing Pair -/
 protected def Pair : SKI := PairPoly.toSKI
-theorem pair_def (f g x : SKI) : SKI.Pair ⬝ f ⬝ g ⬝ x ⇒* MkPair ⬝ (f ⬝ x) ⬝ (g ⬝ x) :=
+theorem pair_def (f g x : SKI) : (SKI.Pair ⬝ f ⬝ g ⬝ x) ↠ MkPair ⬝ (f ⬝ x) ⬝ (g ⬝ x) :=
   PairPoly.toSKI_correct [f, g, x] (by simp)
 
 end SKI

Cslib/Languages/CombinatoryLogic/Confluence.lean

@@ -9,11 +9,11 @@ import Cslib.Foundations.Data.Relation
 /-!
 # SKI reduction is confluent
 
-This file proves the **Church-Rosser** theorem for the SKI calculus, that is, if `a ⇒* b` and
-`a ⇒* c`, `b ⇒* d` and `c ⇒* d` for some term `d`. More strongly (though equivalently), we show
+This file proves the **Church-Rosser** theorem for the SKI calculus, that is, if `a ↠ b` and
+`a ↠ c`, `b ↠ d` and `c ↠ d` for some term `d`. More strongly (though equivalently), we show
 that the relation of having a common reduct is transitive — in the above situation, `a` and `b`,
 and `a` and `c` have common reducts, so the result implies the same of `b` and `c`. Note that
-`CommonReduct` is symmetric (trivially) and reflexive (since `⇒*` is), so we in fact show that
+`CommonReduct` is symmetric (trivially) and reflexive (since `↠` is), so we in fact show that
 `CommonReduct` is an equivalence.
 
 Our proof
@@ -23,21 +23,21 @@ Chapter 4 of Peter Selinger's notes:
 
 ## Main definitions
 
-- `ParallelReduction` : a relation `⇒ₚ` on terms such that `⇒ ⊆ ⇒ₚ ⊆ ⇒*`, allowing simultaneous
+- `ParallelReduction` : a relation `⇒ₚ` on terms such that `⇒ ⊆ ⇒ₚ ⊆ ↠`, allowing simultaneous
 reduction on the head and tail of a term.
 
 ## Main results
 
 - `parallelReduction_diamond` : parallel reduction satisfies the diamond property, that is, it is
 confluent in a single step.
 - `commonReduct_equivalence` : by a general result, the diamond property for `⇒ₚ` implies the same
-for its reflexive-transitive closure. This closure is exactly `⇒*`, which implies the
+for its reflexive-transitive closure. This closure is exactly `↠`, which implies the
 **Church-Rosser** theorem as sketched above.
 -/
 
 namespace SKI
 
-open Red MRed
+open Red MRed ReductionSystem
 
 /-- A reduction step allowing simultaneous reduction of disjoint redexes -/
 inductive ParallelReduction : SKI → SKI → Prop
@@ -55,8 +55,8 @@ inductive ParallelReduction : SKI → SKI → Prop
 /-- Notation for parallel reduction -/
 scoped infix:90 " ⇒ₚ " => ParallelReduction
 
-/-- The inclusion `⇒ₚ ⊆ ⇒*` -/
-theorem mRed_of_parallelReduction {a a' : SKI} (h : a ⇒ₚ a') : a ⇒* a' := by
+/-- The inclusion `⇒ₚ ⊆ ↠` -/
+theorem mRed_of_parallelReduction {a a' : SKI} (h : a ⇒ₚ a') : a ↠ a' := by
   cases h
   case refl => exact Relation.ReflTransGen.refl
   case par a a' b b' ha hb =>
@@ -68,7 +68,7 @@ theorem mRed_of_parallelReduction {a a' : SKI} (h : a ⇒ₚ a') : a ⇒* a' :=
   case red_S a b c => exact Relation.ReflTransGen.single (red_S a b c)
 
 /-- The inclusion `⇒ ⊆ ⇒ₚ` -/
-theorem parallelReduction_of_red {a a' : SKI} (h : a ⇒ a') : a ⇒ₚ a' := by
+theorem parallelReduction_of_red {a a' : SKI} (h : a ⭢ a') : a ⇒ₚ a' := by
   cases h
   case red_S => apply ParallelReduction.red_S
   case red_K => apply ParallelReduction.red_K
@@ -86,12 +86,12 @@ theorem parallelReduction_of_red {a a' : SKI} (h : a ⇒ a') : a ⇒ₚ a' := by
 `parallelReduction_of_red` imply that `⇒` and `⇒ₚ` have the same reflexive-transitive
 closure. -/
 theorem reflTransGen_parallelReduction_mRed :
-    Relation.ReflTransGen ParallelReduction = MRed := by
+    Relation.ReflTransGen ParallelReduction = RedSKI.MRed := by
   ext a b
   constructor
   · apply Relation.reflTransGen_minimal
-    · exact MRed.reflexive
-    · exact MRed.transitive
+    · exact fun _ => by rfl
+    · exact instTransitiveMRed RedSKI
     · exact @mRed_of_parallelReduction
   · apply Relation.reflTransGen_minimal
     · exact Relation.reflexive_reflTransGen
@@ -101,7 +101,7 @@ theorem reflTransGen_parallelReduction_mRed :
 /-!
 Irreducibility for the (partially applied) primitive combinators.
 
-TODO: possibly these should be proven more generally (in another file) for `⇒*`.
+TODO: possibly these should be proven more generally (in another file) for `↠`.
 -/
 
 lemma I_irreducible (a : SKI) (h : I ⇒ₚ a) : a = I := by
@@ -234,7 +234,7 @@ theorem commonReduct_equivalence : Equivalence CommonReduct := by
   exact join_parallelReduction_equivalence
 
 /-- The **Church-Rosser** theorem in the form it is usually stated. -/
-theorem MRed.diamond (a b c : SKI) (hab : a ⇒* b) (hac : a ⇒* c) : CommonReduct b c := by
+theorem MRed.diamond (a b c : SKI) (hab : a ↠ b) (hac : a ↠ c) : CommonReduct b c := by
   apply commonReduct_equivalence.trans (y := a)
   · exact commonReduct_equivalence.symm (commonReduct_of_single hab)
   · exact commonReduct_of_single hac