modified how projection are reduced in lsimp

should improve state of #20 but still not solved

SciLean/Lean/Meta/Basic.lean

@@ -436,6 +436,20 @@ private def reduceProjections (e : Expr) (projections : List Projection) : CoreM
       else
         pure (applyProjections e projections)
 
+
+/-- Return none if no projections happen
+-/
+private def reduceProjections? (e : Expr) (projections : List Projection) : CoreM (Option Expr) :=
+  match projections with
+  | [] => pure none
+  | p :: ps => 
+    matchConstCtor e.getAppFn (fun _ => pure none) fun info _ => do
+      if e.getAppNumArgs = info.numParams + info.numFields then
+        reduceProjections (e.getArg! (info.numParams + p.index)) ps
+      else
+        pure none
+
+
 end ReduceProjOfCtor
 
 open ReduceProjOfCtor in
@@ -455,3 +469,10 @@ def reduceProjOfCtor (e : Expr) : MetaM Expr := do
   let (e',ps) ← peelOfProjections e
   reduceProjections e' ps
 
+open ReduceProjOfCtor in
+/-- Reduces structure projection of explicit constructors
+-/
+def reduceProjOfCtor? (e : Expr) : MetaM (Option Expr) := do
+  let (e',ps) ← peelOfProjections e
+  reduceProjections? e' ps
+

SciLean/Tactic/LSimp/Main.lean

@@ -55,9 +55,10 @@ def isOfNatNatLit (e : Expr) : Bool :=
 def reduceProj? (e : Expr) : MetaM (Option Expr) := do
   match e with
   | Expr.proj _ _ (.fvar _) => return none -- do not reduce projections on fvars
-  | Expr.proj _ i c => 
+  | Expr.proj n i c => 
     letTelescope c λ xs b => do
-      let some b ← Meta.project? b i
+      -- let some b ← Meta.project? b i
+      let some b ← reduceProjOfCtor? (.proj n i b)
         | return none
       mkLambdaFVars xs b
   | _               => return none
@@ -378,7 +379,7 @@ where
     | none   => return { expr := e }
 
   simpProj (e : Expr) : M Result := do
-    match (← reduceProj?' e) with
+    match (← reduceProj? e) with
     | some e => return { expr := e }
     | none =>
       let s := e.projExpr!

test/issues/20.lean

@@ -0,0 +1,84 @@
+import Std.Tactic.GuardMsgs
+import SciLean.Util.RewriteBy
+import SciLean.Tactic.LSimp.Elab
+import SciLean.Tactic.LetNormalize
+
+open SciLean
+
+
+/--
+info: fun i =>
+  let j := 42;
+  let foo := ((i * j, i + j), i ^ j, i / j);
+  foo.fst : Nat → Nat × Nat
+-/
+#guard_msgs in
+#check 
+   (fun i : Nat =>
+      let j := 42
+      let foo := ((i * j, i+j), (i ^ j, i / j))
+      foo.fst)
+   rewrite_by
+     lsimp (config := {zeta:=false}) only
+
+
+/--
+info: fun i =>
+  (let j := 42;
+    let foo := ((i * j, i + j), i ^ j, i / j);
+    foo).fst : Nat → Nat × Nat
+-/
+#guard_msgs in
+#check 
+   (fun i : Nat =>
+      (let j := 42
+       let foo := ((i * j, i+j), (i ^ j, i / j))
+       foo).fst)
+   rewrite_by
+     ldsimp (config := {zeta:=false}) only
+
+
+/--
+info: fun i =>
+  (let j := 42;
+    let foo := ((i * j, i + j), i ^ j, i / j);
+    foo.fst).snd : Nat → Nat
+-/
+#guard_msgs in
+#check 
+   (fun i : Nat =>
+      (let j := 42
+       let foo := ((i * j, i+j), (i ^ j, i / j))
+       foo.fst).snd)
+   rewrite_by
+     lsimp (config := {zeta:=false, proj:=false}) only
+
+
+/--
+info: fun i =>
+  let j := 42;
+  let foo := ((i * j, i + j), i ^ j, i / j);
+  foo.fst.snd : Nat → Nat
+-/
+#guard_msgs in
+#check 
+   (fun i : Nat =>
+      let j := 42
+      let foo := ((i * j, i+j), (i ^ j, i / j))
+      foo.fst.snd)
+   rewrite_by
+     lsimp (config := {zeta:=false}) only
+
+
+/--
+info: let a := 42;
+a : Nat
+-/
+#guard_msgs in
+#check 
+  (let a := 42
+   let b := 7
+   (a,b)).1
+  rewrite_by
+    lsimp (config := {zeta:=false}) only
+