Reduce code entropy

Author: nomeata

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -68,26 +68,24 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
     let mvarId ← mvarId.assertExt `aSize (mkConst `Nat) aSize
     let (aSizeFVarId, mvarId) ← mvarId.intro1
     let (hEq, mvarId) ← mvarId.intro1
-    let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix (substNewEqs := false)
+    let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix
     subgoals.mapIdxM fun i subgoal => do
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId
-      let hEqSz  := (subst.get hEq).fvarId!
       if h : i < sizes.size then
-         let n := sizes[i]
-         let mvarId ← mvarId.clear subgoal.newHs[0]!
-         let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!
-         mvarId.withContext do
-           let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
-           let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
-           let (xs, mvarId)  ← mvarId.introN n
-           let (hEqLit, mvarId) ← mvarId.intro1
-           let mvarId ← mvarId.clear hEqSz
-           let (subst, mvarId) ← substCore mvarId hEqLit false subst
-           pure { mvarId := mvarId, elems := xs, subst := subst }
+        let hEqSz  := (subst.get hEq).fvarId!
+        let n := sizes[i]
+        mvarId.withContext do
+          let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
+          let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
+          let (xs, mvarId)  ← mvarId.introN n
+          let (hEqLit, mvarId) ← mvarId.intro1
+          let mvarId ← mvarId.clear hEqSz
+          let (subst, mvarId) ← substCore mvarId hEqLit (symm := false) subst
+          pure { mvarId := mvarId, elems := xs, subst := subst }
       else
-         let (subst, mvarId) ← substCore mvarId hEq false subst
-         let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
-         pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
+        let (subst, mvarId) ← substCore mvarId hEq (symm := false) subst
+        let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
+        pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
 
 end Lean.Meta

src/Lean/Meta/Match/CaseValues.lean

@@ -30,7 +30,7 @@ structure CaseValueSubgoal where
 
   Remark: `subst` field of the second subgoal is equal to the input `subst`. -/
 private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
-    (subst : FVarSubst := {}) (substNewEq : Bool)
+    (subst : FVarSubst := {})
     : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
   mvarId.withContext do
     let tag ← mvarId.getTag
@@ -47,26 +47,15 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P
     let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }
     let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P
-    let (thenSubst, thenMVarId) ←
-      if substNewEq then
-        substCore thenMVarId thenH (symm := false) subst (clearH := false)
-      else
-        pure (subst, thenMVarId)
     thenMVarId.withContext do
-      trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
-      let thenH := (thenSubst.get thenH).fvarId!
+      trace[Meta] "subst domain: {subst.domain.map (·.name)}"
+      let thenH := (subst.get thenH).fvarId!
       trace[Meta] "searching for decl"
       let _ ← thenH.getDecl
       trace[Meta] "found decl"
-    let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
+    let thenSubgoal := { mvarId := thenMVarId, newH := (subst.get thenH).fvarId!, subst : CaseValueSubgoal }
     pure (thenSubgoal, elseSubgoal)
 
-def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := do
-  let s ← caseValueAux mvarId fvarId value (substNewEq := true)
-  appendTagSuffix s.1.mvarId `thenBranch
-  appendTagSuffix s.2.mvarId `elseBranch
-  pure s
-
 structure CaseValuesSubgoal where
   mvarId : MVarId
   newHs  : Array FVarId := #[]
@@ -88,22 +77,19 @@ structure CaseValuesSubgoal where
 
   If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
 -/
-def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) (substNewEqs : Bool) : MetaM (Array CaseValuesSubgoal) :=
+def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h) : MetaM (Array CaseValuesSubgoal) :=
   let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
     | _, mvarId, [],    _,  _        => throwTacticEx `caseValues mvarId "list of values must not be empty"
     | i, mvarId, v::vs, hs, subgoals => do
-      let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) (substNewEq := !substNewEqs) {}
+      let (thenSubgoal, elseSubgoal) ← caseValueAux mvarId fvarId v (hNamePrefix.appendIndexAfter i) {}
       appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
       let thenMVarId ← hs.foldlM
         (fun thenMVarId h => match thenSubgoal.subst.get h with
           | Expr.fvar fvarId => thenMVarId.tryClear fvarId
           | _                => pure thenMVarId)
         thenSubgoal.mvarId
-      let subgoals ← if substNewEqs then
-         let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) thenSubgoal.subst (clearH := true)
-         pure <| subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
-      else
-         pure <| subgoals.push { mvarId := thenMVarId, newHs := #[thenSubgoal.newH], subst := thenSubgoal.subst }
+      let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) thenSubgoal.subst (clearH := true)
+      let subgoals := subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
       match vs with
       | [] => do
         appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))

src/Lean/Meta/Match/Match.lean

@@ -686,7 +686,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
   trace[Meta.Match.match] "value step"
   let x :: xs := p.vars | unreachable!
   let values := collectValues p
-  let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
+  let subgoals ← caseValues p.mvarId x.fvarId! values
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
     if h : i < values.size then

tests/lean/run/meta6.lean

@@ -71,7 +71,7 @@ withLocalDeclD `y nat fun y => do
 let vType ← mkAppM `Vec #[nat, x];
 withLocalDeclD `v vType fun v => do
 let m ← mkFreshExprSyntheticOpaqueMVar vType;
-let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5] (substNewEqs := false);
+let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
 subgoals.forM fun s => do {
   print (MessageData.ofGoal s.mvarId);
   s.mvarId.assumption