feat: make relation more general readying for mutuals

src/Lean/Elab/Coinductive.lean

@@ -34,7 +34,7 @@ structure CoInductiveView.CtorView where
   type?     : Option Term
   deriving Inhabited
 
-structure CoInductiveView : Type where
+structure CoInductiveView where
   ref             : TSyntax ``Lean.Parser.Command.coinductive
   declId          : TSyntax ``Parser.Command.declId
   modifiers       : Modifiers
@@ -101,6 +101,15 @@ def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoI
 
 def ofStx (stx : Syntax) := elabModifiers stx[0] >>= (ofModifiersAndStx · stx[1])
 
+def extractIds : TSyntax ``Parser.Term.bracketedBinder → Array Ident
+  | ⟨.node _ _ #[.atom _ _, .node _ `null ids, _, _,  .atom _ _]⟩ => ids.map (⟨·⟩)
+  | _ => #[]
+
+def toBinderIds (c : CoInductiveView) : Array Ident := (c.binders.map extractIds).flatten
+
+def toRelType (c : CoInductiveView) : CommandElabM Term :=
+  c.binders.reverse.foldlM (fun curr acc => `($acc:bracketedBinder → $curr)) c.type
+
 end CoInductiveView
 
 open Parser.Term in
@@ -110,9 +119,6 @@ abbrev bb := bracketedBinder
 instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩
 end
 
-def extractIds : TSyntax ``Parser.Term.bracketedBinder → Array Ident
-  | ⟨.node _ _ #[_, .node _ `null ids, _, _,  _]⟩ => ids.map (⟨·⟩)
-  | _ => #[]
 
 partial def typeToArgArr (type : Term) : Array Term × Term := Prod.map List.toArray id $ go type.raw
   where go
@@ -127,7 +133,6 @@ def extractName : Syntax → Name
   | .ident _ _ nm _ => nm
   | _ => .anonymous
 
-
 def split : Nat → List α → (List α) × (List α)
   | _, []  => ⟨[], []⟩
   | 0, arr => ⟨[], arr⟩
@@ -136,7 +141,7 @@ def split : Nat → List α → (List α) × (List α)
 def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM Unit := do
   let shortDeclName := topView.shortDeclName ++ `Shape
 
-  let v ← `(bb| ($(mkIdent topView.shortDeclName) : $(topView.type)) )
+  let v ← `(bb| ($(mkIdent topView.shortDeclName) : $(←topView.toRelType)) )
 
   let view := {
     ref             := .missing
@@ -152,9 +157,12 @@ def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM
     computedFields  := #[]
   }
 
+  trace[Elab.CoInductive] s!"{repr topView.binders}"
+  trace[Elab.CoInductive] s!"{topView.toBinderIds}"
+
   let stx ← `(command|
-    abbrev $(mkIdent $ topView.shortDeclName ++ `Is) $(topView.binders)* (R : $(topView.type)) : Prop :=
-      ∀ { $argArr* }, R $argArr* → $(mkIdent shortDeclName) $((topView.binders.map extractIds).flatten)* R $argArr*)
+    abbrev $(mkIdent $ topView.shortDeclName ++ `Is) $(topView.binders)* (R : $(←topView.toRelType)) : Prop :=
+      ∀ { $argArr* }, R $(topView.toBinderIds)* $argArr* → $(mkIdent shortDeclName) $(topView.toBinderIds)* R $argArr*)
 
   trace[Elab.CoInductive] "Generating Is check:"
   trace[Elab.CoInductive] stx
@@ -175,6 +183,7 @@ def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM
         let ⟨pre, post⟩ := (split topView.binders.size arr.toList).map (·.toArray) (·.toArray)
 
         let out ← `($isTy $pre* $(mkIdent topView.shortDeclName) $post*)
+
         args.reverse.foldlM (fun acc curr => `($curr → $acc)) out
 
       return {
@@ -185,6 +194,23 @@ def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM
         type?     := type?
       }
 
+/- def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do -/
+/-   let view := views[0]! -/
+
+/-   let viewCheck ← views.mapM fun view => do -/
+/-     let ⟨tyArr, out⟩ := typeToArgArr view.type -/
+/-     let argArr := (← tyArr.mapM (fun _ => mkFreshBinderName)).map mkIdent -/
+
+/-     -- In theory we could make this handle types by simply changing the existential quantification but this would yield some pretty funny results -/
+/-     let .node _ ``Parser.Term.prop _ := out.raw | throwErrorAt out "Expected return type to be a Prop" -/
+/-     return Prod.mk view argArr -/
+
+/-   throwError "sorry" -/
+  /- generateIs view argArr -/
+  /- let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* => -/
+  /-   ∃ R, @$(mkIdent $ view.shortDeclName ++ `Is) $((view.binders.map extractIds).flatten)* R ∧ R $argArr*) -/
+  /- elabCommand stx -/
+
 -- TODO: handle mutual coinductive predicates
 def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
   let view := views[0]!
@@ -197,6 +223,6 @@ def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit :=
 
   generateIs view argArr
   let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
-    ∃ R, @$(mkIdent $ view.shortDeclName ++ `Is) $((view.binders.map extractIds).flatten)* R ∧ R $argArr*)
+    ∃ R, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* R ∧ R $(view.toBinderIds)* $argArr*)
   elabCommand stx
 

tests/lean/run/coindBisim.lean

@@ -8,29 +8,29 @@ structure FSM where
 coinductive Bisim (fsm : FSM) : fsm.S → fsm.S → Prop :=
   | step {s t : fsm.S} :
     (fsm.A s ↔ fsm.A t)
-    → (∀ c, Bisim (fsm.d s c) (fsm.d t c))
+    → (∀ c, Bisim fsm (fsm.d s c) (fsm.d t c))
     → Bisim fsm s t
 
 /--
-info: inductive Bisim.Shape : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
+info: inductive Bisim.Shape : (fsm : FSM) → ((fsm : FSM) → fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
 number of parameters: 4
 constructors:
-Bisim.Shape.step : ∀ {fsm : FSM} {Bisim : fsm.S → fsm.S → Prop} {s t : fsm.S},
-  (fsm.A s ↔ fsm.A t) → (∀ (c : Nat), Bisim (fsm.d s c) (fsm.d t c)) → Bisim.Shape fsm Bisim s t
+Bisim.Shape.step : ∀ {fsm : FSM} {Bisim : (fsm : FSM) → fsm.S → fsm.S → Prop} {s t : fsm.S},
+  (fsm.A s ↔ fsm.A t) → (∀ (c : Nat), Bisim fsm (fsm.d s c) (fsm.d t c)) → Bisim.Shape fsm Bisim s t
 -/
 #guard_msgs in
 #print Bisim.Shape
 
 /--
-info: @[reducible] def Bisim.Is : (fsm : FSM) → (fsm.S → fsm.S → Prop) → Prop :=
-fun fsm R => ∀ {x x_1 : fsm.S}, R x x_1 → Bisim.Shape fsm R x x_1
+info: @[reducible] def Bisim.Is : FSM → ((fsm : FSM) → fsm.S → fsm.S → Prop) → Prop :=
+fun fsm R => ∀ {x x_1 : fsm.S}, R fsm x x_1 → Bisim.Shape fsm R x x_1
 -/
 #guard_msgs in
 #print Bisim.Is
 
 /--
 info: def Bisim : (fsm : FSM) → fsm.S → fsm.S → Prop :=
-fun fsm x x_1 => ∃ R, Bisim.Is fsm R ∧ R x x_1
+fun fsm x x_1 => ∃ R, Bisim.Is fsm R ∧ R fsm x x_1
 -/
 #guard_msgs in
 #print Bisim
@@ -40,29 +40,29 @@ fun fsm x x_1 => ∃ R, Bisim.Is fsm R ∧ R x x_1
 #print axioms Bisim
 
 theorem bisim_refl : Bisim f a a := by
-  exists fun a b => a = b
+  exists fun _ a b => a = b
   simp only [and_true]
   intro s t seqt
   constructor <;> simp_all
 
 theorem bisim_symm (h : Bisim f a b): Bisim f b a := by
   rcases h with ⟨rel, relIsBisim, rab⟩
-  exists fun a b => rel b a
+  exists fun f a b => rel f b a
   simp_all
   intro a b holds
   specialize relIsBisim holds
   rcases relIsBisim with ⟨imp, z⟩
   constructor <;> simp_all only [implies_true, and_self]
 
-theorem Bisim.unfold {f} : Bisim.Is f (Bisim f) := by
+theorem Bisim.unfold {f} : Bisim.Is f Bisim := by
   rintro s t ⟨R, h_is, h_Rst⟩
   constructor
   · exact (h_is h_Rst).1
   · intro c; exact ⟨R, h_is, (h_is h_Rst).2 c⟩
 
 theorem bisim_trans (h_ab : Bisim f a b) (h_bc : Bisim f b c) :
     Bisim f a c := by
-  exists (∃ u, Bisim f · u ∧ Bisim f u ·)
+  exists (fun f s t => ∃ u, Bisim f s u ∧ Bisim f u t)
   constructor
   intro s t h_Rst
   · rcases h_Rst with ⟨u, h_su, h_ut⟩