chore(CombinatoryLogic): miscellaneous grind golfing (#345)

Low priority

---------

Co-authored-by: twwar <tom.waring@unimelb.edu.au>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: 3 people

Cslib/Languages/CombinatoryLogic/Basic.lean

@@ -140,7 +140,7 @@ theorem Polynomial.toSKI_correct {n : Nat} (Γ : SKI.Polynomial n) (xs : List SK
     replace ⟨ys, z, h⟩ := h
     -- apply inductive step, using elimVar_correct
     have : ys.length = n := by
-      replace h := congr_arg List.length <| h
+      replace h := congr_arg List.length h
       simp_rw [List.length_append, List.length_singleton, hxs] at h
       exact Nat.succ_inj.mp h.symm
     simp_rw [h, applyList_concat]

Cslib/Languages/CombinatoryLogic/Confluence.lean

@@ -172,13 +172,9 @@ theorem parallelReduction_diamond : Diamond ParallelReduction := by
       let ⟨a'', c', h⟩ := Sab_irreducible a c a' ha'
       rw [h.2.2]
       use a'' ⬝ b' ⬝ (c' ⬝ b'), .red_S a'' c' b'
-      apply ParallelReduction.par
-      · apply ParallelReduction.par
-        · exact h.1
-        · exact hb'
-      · apply ParallelReduction.par
-        · exact h.2.1
-        · exact hb'
+      apply ParallelReduction.par <;>
+        apply ParallelReduction.par <;>
+        grind
   case red_I =>
     cases h₂
     case refl => use a₁; exact ⟨.refl a₁, .red_I a₁⟩
@@ -201,7 +197,7 @@ theorem parallelReduction_diamond : Diamond ParallelReduction := by
     cases h₂
     case refl =>
       use a ⬝ c ⬝ (b ⬝ c)
-      exact ⟨.refl _, .red_S _ _ _⟩
+      exact ⟨.refl _, .red_S ..⟩
     case par d c' hd hc =>
       let ⟨a', b', h⟩ := Sab_irreducible a b d hd
       rw [h.2.2]
@@ -210,7 +206,7 @@ theorem parallelReduction_diamond : Diamond ParallelReduction := by
       · apply ParallelReduction.par
         · exact .par h.left hc
         · exact .par h.2.1 hc
-      · exact .red_S _ _ _
+      · exact .red_S ..
     case red_S => exact ⟨a ⬝ c ⬝ (b ⬝ c), .refl _, .refl _,⟩
 
 theorem join_parallelReduction_equivalence :

Cslib/Languages/CombinatoryLogic/Evaluation.lean

@@ -169,19 +169,7 @@ instance : DecidablePred RedexFree := fun _ => decidable_of_iff' _ redexFree_iff
 /-- A term is redex free iff its only many-step reduction is itself. -/
 theorem redexFree_iff_mred_eq {x : SKI} : x.RedexFree ↔ ∀ y, (x ↠ y) ↔ x = y := by
   constructor
-  case mp =>
-    intro h y
-    constructor
-    case mp =>
-      intro h'
-      cases h'.cases_head
-      case inl => assumption
-      case inr h' =>
-        obtain ⟨z, hz, _⟩ := h'
-        cases h.normal_red ⟨_, hz⟩
-    case mpr =>
-      intro h
-      rw [h]
+  case mp => grind [RedexFree.normal_red]
   case mpr =>
     intro h
     rw [redexFree_iff]
@@ -232,21 +220,7 @@ theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool
       · exact mJoin_red_head K <| mJoin_red_head S hxy
       · apply Relation.MJoin.single
         exact hy S K
-  by_cases u
-  case pos hu =>
-    by_cases v
-    case pos hv =>
-      rw [hu, hv]
-    case neg hv =>
-      simp_rw [hu, hv, Bool.false_eq_true, reduceIte] at h
-      exact False.elim <| sk_nequiv h
-  case neg hu =>
-    by_cases v
-    case pos hv =>
-      simp_rw [hu, hv, Bool.false_eq_true, reduceIte] at h
-      exact False.elim <| sk_nequiv (mJoin_red_equivalence.symm h)
-    case neg hv =>
-      simp_rw [hu, hv]
+  grind [sk_nequiv, mJoin_red_equivalence.symm h]
 
 lemma TF_nequiv : ¬ MJoin Red TT FF := fun h =>
   (Bool.eq_not_self true).mp <| isBool_injective TT FF true false TT_correct FF_correct h

Cslib/Languages/CombinatoryLogic/Recursion.lean

@@ -304,23 +304,17 @@ theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI)
   induction n generalizing m x
   all_goals apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ f)
   case zero.a =>
-    apply isChurch_trans (a' := x)
-    · have : IsChurch (fNat m) (f ⬝ x) := hf m x hx
-      rw [Nat.add_zero] at hroot
-      simp_rw [hroot] at this
-      apply rfindAboveAux_base
-      assumption
-    · assumption
+    apply isChurch_trans (a' := x) <;>
+      grind [rfindAboveAux_base]
   case succ.a n ih =>
-    unfold RFindAbove
     apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f)
     · let y := (fNat m).pred
-      have : IsChurch (y+1) (f ⬝ x) := by
+      have : IsChurch (y + 1) (f ⬝ x) := by
         subst y
         exact Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf m x hx
       apply rfindAboveAux_step
       assumption
-    · replace ih := ih (SKI.Succ ⬝ x) (m+1) (succ_correct _ x hx)
+    · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx)
       grind
   -- close the `h` goals of the above `apply isChurch_trans`
   all_goals {apply MRed.head; apply MRed.head; exact fixedPoint_correct _}
@@ -347,8 +341,8 @@ theorem add_def (a b : SKI) : (SKI.Add ⬝ a ⬝ b) ↠ a ⬝ SKI.Succ ⬝ b :=
   AddPoly.toSKI_correct [a, b] (by simp)
 
 theorem add_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n+m) (SKI.Add ⬝ a ⬝ b) := by
-  refine isChurch_trans (n+m) (a' := Church n SKI.Succ b) ?_ ?_
+    IsChurch (n + m) (SKI.Add ⬝ a ⬝ b) := by
+  refine isChurch_trans (n + m) (a' := Church n SKI.Succ b) ?_ ?_
   · calc
     _ ↠ a ⬝ SKI.Succ ⬝ b := add_def a b
     _ ↠ Church n SKI.Succ b := ha SKI.Succ b
@@ -367,15 +361,15 @@ theorem mul_def (a b : SKI) : (SKI.Mul ⬝ a ⬝ b) ↠ a ⬝ (SKI.Add ⬝ b) 
   MulPoly.toSKI_correct [a, b] (by simp)
 
 theorem mul_correct {n m : Nat} {a b : SKI} (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n*m) (SKI.Mul ⬝ a ⬝ b) := by
-  refine isChurch_trans (n*m) (a' := Church n (SKI.Add ⬝ b) SKI.Zero) ?_ ?_
+    IsChurch (n * m) (SKI.Mul ⬝ a ⬝ b) := by
+  refine isChurch_trans (n * m) (a' := Church n (SKI.Add ⬝ b) SKI.Zero) ?_ ?_
   · exact Trans.trans (mul_def a b) (ha (SKI.Add ⬝ b) SKI.Zero)
   · clear ha
     induction n with
       | zero => simp_rw [Nat.zero_mul, Church]; exact zero_correct
       | succ n ih =>
         simp_rw [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church]
-        exact add_correct m (n*m) b (Church n (SKI.Add ⬝ b) SKI.Zero) hb ih
+        exact add_correct m (n * m) b (Church n (SKI.Add ⬝ b) SKI.Zero) hb ih
 
 /-- Subtraction: λ n m. n Pred m -/
 def SubPoly : SKI.Polynomial 2 := &1 ⬝' Pred ⬝' &0
@@ -385,8 +379,8 @@ theorem sub_def (a b : SKI) : (SKI.Sub ⬝ a ⬝ b) ↠ b ⬝ Pred ⬝ a :=
   SubPoly.toSKI_correct [a, b] (by simp)
 
 theorem sub_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n-m) (SKI.Sub ⬝ a ⬝ b) := by
-  refine isChurch_trans (n-m) (a' := Church m Pred a) ?_ ?_
+    IsChurch (n - m) (SKI.Sub ⬝ a ⬝ b) := by
+  refine isChurch_trans (n - m) (a' := Church m Pred a) ?_ ?_
   · calc
     _ ↠ b ⬝ Pred ⬝ a := sub_def a b
     _ ↠ Church m Pred a := hb Pred a