From a88d3b2b2686037b0f661dc2163ff3daf40f07db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 21 Aug 2024 11:16:53 +0100
Subject: [PATCH 01/10] feat: add simple co-inductive predicates

---
 src/Lean/Elab/Coinductive.lean | 332 +++++++++++++++++++++++++++++++++
 src/Lean/Elab/Declaration.lean |   9 +
 src/Lean/Parser/Command.lean   |   5 +-
 3 files changed, 345 insertions(+), 1 deletion(-)
 create mode 100644 src/Lean/Elab/Coinductive.lean

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
new file mode 100644
index 000000000000..b3aae810795b
--- /dev/null
+++ b/src/Lean/Elab/Coinductive.lean
@@ -0,0 +1,332 @@
+prelude
+import Lean.Util.CollectLevelParams
+import Lean.Elab.DeclUtil
+import Lean.Elab.DefView
+import Lean.Elab.Inductive
+import Lean.Elab.Structure
+import Lean.Elab.MutualDef
+import Lean.Elab.DeclarationRange
+
+import Lean.Util.Trace
+import Lean.Elab.Binders
+import Lean.Elab.DeclarationRange
+import Lean.Elab.Command
+import Lean.Elab.Inductive
+import Lean.Elab.Exception
+
+namespace Lean.Elab.Command
+
+open Lean Lean.Elab Lean.Elab.Term Lean.Parser Command
+
+builtin_initialize
+  registerTraceClass `Elab.CoInductive
+
+structure CoInductiveView.CtorView where
+  ref       : Syntax
+  modifiers : Modifiers
+  declName  : Name
+  binders   : Array BinderView
+  type?     : Option Term
+  deriving Inhabited
+
+structure CoInductiveView : Type where
+  ref             : TSyntax ``Lean.Parser.Command.coinductive
+  declId          : TSyntax ``Parser.Command.declId
+  modifiers       : Modifiers
+  shortDeclName   : Name
+  declName        : Name
+  levelNames      : List Name
+  binders         : Array BinderView
+  type            : Term
+  ctors           : Array CoInductiveView.CtorView
+  /- derivingClasses : Array Lean.Elab.DerivingClassView -/
+  /- computedFields  : Array Lean.Elab.Command.ComputedFieldView -/
+  deriving Inhabited
+
+namespace CoInductiveView
+
+section
+/--
+  Given syntax of the forms
+    a) (`:` term)?
+    b) `:` term
+  return `term` if it is present, or a hole if not. -/
+private def expandBinderType (ref : Syntax) (stx : Syntax) : Syntax :=
+  if stx.getNumArgs == 0 then
+    mkHole ref
+  else
+    stx[1]
+
+/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/
+private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
+  match stx with
+  | `(_) => mkFreshIdent stx (canonical := true)
+  | _    => pure stx
+
+/--
+Expand `optional (binderTactic <|> binderDefault)`
+```
+def binderTactic  := leading_parser " := " >> " by " >> tacticParser
+def binderDefault := leading_parser " := " >> termParser
+```
+-/
+private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax := do
+  if optBinderModifier.isNone then
+    return type
+  else
+    let modifier := optBinderModifier[0]
+    let kind     := modifier.getKind
+    if kind == `Lean.Parser.Term.binderDefault then
+      let defaultVal := modifier[1]
+      `(optParam $(⟨type⟩) $(⟨defaultVal⟩))
+    else if kind == `Lean.Parser.Term.binderTactic then
+      let tac := modifier[2]
+      let name ← declareTacticSyntax tac
+      `(autoParam $(⟨type⟩) $(mkIdentFrom tac name))
+    else
+      throwUnsupportedSyntax
+private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
+  ids.getArgs.mapM fun id =>
+    let k := id.getKind
+    if k == identKind || k == `Lean.Parser.Term.hole then
+      return id
+    else
+      throwErrorAt id "identifier or `_` expected"
+
+/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
+private def expandOptIdent (stx : Syntax) : TermElabM Syntax := do
+  if stx.isNone then
+    let id ← withFreshMacroScope <| MonadQuotation.addMacroScope `inst
+    return mkIdentFrom stx id
+  else
+    return stx[0]
+
+/--
+Convert `stx` into an array of `BinderView`s.
+`stx` must be an identifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
+-/
+private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
+  let k := stx.getKind
+  if stx.isIdent || k == ``Lean.Parser.Term.hole then
+    -- binderIdent
+    return #[{ ref := stx, id := (← expandBinderIdent stx), type := mkHole stx, bi := .default }]
+  else if k == ``Lean.Parser.Term.explicitBinder then
+    -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
+    let ids ← getBinderIds stx[1]
+    let type        := stx[2]
+    let optModifier := stx[3]
+    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := .default }
+  else if k == ``Lean.Parser.Term.implicitBinder then
+    -- `{` binderIdent+ binderType `}`
+    let ids ← getBinderIds stx[1]
+    let type := stx[2]
+    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .implicit }
+  else if k == ``Lean.Parser.Term.strictImplicitBinder then
+    -- `⦃` binderIdent+ binderType `⦄`
+    let ids ← getBinderIds stx[1]
+    let type := stx[2]
+    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .strictImplicit }
+  else if k == ``Lean.Parser.Term.instBinder then
+    -- `[` optIdent type `]`
+    let id ← expandOptIdent stx[1]
+    let type := stx[2]
+    return #[ { ref := id, id := id, type := type, bi := .instImplicit } ]
+  else
+    throwUnsupportedSyntax
+end
+
+/- #check Lean.Elab.Binders.to -/
+
+/- open private toBinderViews from Lean.Elab.Binders in -/
+private def toBViews (stx : Syntax) : CommandElabM $ Array Elab.Term.BinderView := do
+  let x ← liftTermElabM $ stx.getArgs.mapM toBinderViews
+  return x.flatten
+
+def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoInductiveView.CtorView := do
+  let mut ctorModifiers ← elabModifiers ref[2]
+  if let some leadingDocComment := ref[0].getOptional? then
+    if ctorModifiers.docString?.isSome then
+      logErrorAt leadingDocComment "duplicate doc string"
+    ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+  if ctorModifiers.isPrivate && modifiers.isPrivate then
+    throwError "invalid 'private' constructor in a 'private' inductive datatype"
+  if ctorModifiers.isProtected && modifiers.isPrivate then
+    throwError "invalid 'protected' constructor in a 'private' inductive datatype"
+
+  checkValidCtorModifier ctorModifiers
+  let ctorName := ref.getIdAt 3
+  let ctorName := declName ++ ctorName
+  let ctorName ← withRef ref[3] $ Elab.applyVisibility ctorModifiers.visibility ctorName
+  let (binders, type?) := Elab.expandOptDeclSig ref[4]
+  addDocString' ctorName ctorModifiers.docString?
+  Elab.addAuxDeclarationRanges ctorName ref ref[3]
+
+  let binders ← toBViews binders
+
+  return { ref, modifiers := ctorModifiers, declName := ctorName, binders, type? := type?.map (⟨·⟩) }
+
+def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do
+  let (binders, type) := Elab.expandDeclSig decl[2]!
+
+  let binders ← toBViews binders
+
+  let declId  := ⟨decl[1]⟩
+  let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId declId.raw modifiers
+
+  let ctors ← decl[4].getArgs.mapM $ CtorView.ofStx declName modifiers
+
+  Elab.addDeclarationRanges declName decl
+
+  return {
+    ref := ⟨decl⟩
+
+    declName
+    shortDeclName
+
+    levelNames
+    type := ⟨type⟩
+
+    binders
+    ctors
+
+    declId
+    modifiers
+  }
+
+def ofStx (stx : Syntax) := elabModifiers stx[0] >>= (ofModifiersAndStx · stx[1])
+
+end CoInductiveView
+
+open Parser.Term in
+section
+abbrev bb            : Lean.Parser.Parser := bracketedBinder
+abbrev matchAltExprs : Lean.Parser.Parser := matchAlts
+
+/- Since `bb` and `matchAltExprs` are aliases for `bracketedBinder`, resp. `matchAlts`,
+we can safely coerce syntax of these categories  -/
+instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder)      where coe x := ⟨x.raw⟩
+instance : Coe (TSyntax ``matchAltExprs) (TSyntax ``matchAlts) where coe x := ⟨x.raw⟩
+end
+
+def binderViewtoBracketedBinder (v : BinderView) : CommandElabM $ TSyntax ``Parser.Term.bracketedBinder := do match v.bi with
+  | .default =>        `(bb|( $(⟨v.id⟩):ident : $(⟨v.type⟩) ))
+  | .implicit =>       `(bb|{ $(⟨v.id⟩):ident : $(⟨v.type⟩) })
+  | .strictImplicit => `(bb|⦃ $(⟨v.id⟩):ident : $(⟨v.type⟩) ⦄)
+  | .instImplicit =>   `(bb|[ $(⟨v.id⟩):ident : $(⟨v.type⟩) ])
+
+partial def typeToArgArr (type : Term) : Array Term × Term := Prod.map List.toArray id $ go type.raw
+  where go
+    | Syntax.node _ ``Parser.Term.arrow #[hd, _, tail] => Prod.map (⟨hd⟩ :: ·) id $ go tail
+    | rest => ⟨[], ⟨rest⟩⟩
+
+def appsToArgArr (type : Term) : Array Term × Term := match type.raw with
+    | Syntax.node _ ``Parser.Term.app #[v, cont] => ⟨cont.getArgs.map (⟨·⟩), ⟨v⟩⟩
+    | rest => ⟨#[], ⟨rest⟩⟩
+
+deriving instance Repr for BinderView
+
+def extractName : Syntax → Name
+  | .ident _ _ nm _ => nm
+  | _ => .anonymous
+
+def generateIs (topView : CoInductiveView) (argArr : Array Ident) (tyArr : Array Term) : CommandElabM Unit := do
+  let id := topView.shortDeclName ++ `Invariant
+
+  let isTy ← `($(mkIdent id) $(topView.binders.map (⟨·.id⟩))* $(mkIdent topView.shortDeclName) $argArr*)
+
+  let v : Array (TSyntax ``ctor) ← topView.ctors.mapM $ handleCtor isTy
+
+  let x ← argArr.zip tyArr |>.mapM (fun ⟨id, v⟩ => `(bb| ($id : $v) ))
+
+  -- TODO: Use elabInductiveViews
+  let invariant ← `(command|
+    inductive $(mkIdent id) $(←topView.binders.mapM binderViewtoBracketedBinder)* ($(topView.shortDeclName |> mkIdent) : $(topView.type)) $x* : Prop := $v*
+  )
+
+  trace[Elab.CoInductive] "Generating invariant:"
+  trace[Elab.CoInductive] invariant
+
+  let stx ← `(command|
+    abbrev $(topView.shortDeclName ++ `Is |> mkIdent) $(←topView.binders.mapM binderViewtoBracketedBinder)* (R : $(topView.type)) : Prop :=
+      ∀ { $argArr* }, R $argArr* → $(mkIdent id) $(topView.binders.map (⟨·.id⟩))* R $argArr*)
+
+  trace[Elab.CoInductive] "Generating Is check:"
+  trace[Elab.CoInductive] stx
+
+  Elab.Command.elabCommand invariant
+  Elab.Command.elabCommand stx
+
+  where
+    correctorIterator (loc : Term)
+      | ⟨.ident _ _ nm _⟩ :: tla, binderV :: tlb => do
+        let .ident _ _ nmx _ := binderV.id | unreachable!
+        if nm == nmx then correctorIterator loc tla tlb
+        else throwErrorAt loc s!"Expected {binderV.id}"
+      | loc :: _, binderV :: _ => throwErrorAt loc s!"Expected {binderV.id}"
+      | rest, [] =>
+        pure rest
+      | [], _ => throwErrorAt loc "Insufficent arguments"
+
+    handleRetty appl arr id := do
+      let .ident _ _ nm _ := id.raw  | throwErrorAt id s!"Expected return type to be {topView.declId}" 
+      if nm != topView.shortDeclName then throwErrorAt id s!"Expected return type to be {topView.declId}"
+
+      correctorIterator appl arr.toList topView.binders.toList
+
+    -- Removal array × Equational array
+    equationalTransformer (loc : Term) : List Term → List Ident → CommandElabM ((List (Ident × Ident)) × (List Term))
+      | [], [] => return Prod.mk [] []
+      | x@⟨.ident _ _ _ _⟩ :: tla, hdb :: tlb => do
+        let ⟨rem, eq⟩ ← equationalTransformer loc tla tlb
+        return ⟨(Prod.mk ⟨x.raw⟩ hdb) :: rem, eq⟩
+      | hda :: tla, hdb :: tlb => do
+        let ⟨rem, eq⟩ ← equationalTransformer loc tla tlb
+        return ⟨rem, (←`($hda = $hdb)) :: eq⟩
+      | [], _ | _, [] => throwErrorAt loc "Incorrect number of arguments"
+
+    handleCtor isTy view := do
+      let nm := view.declName.replacePrefix topView.declName .anonymous
+
+      let .some type := view.type? | throwErrorAt view.ref "An coinductive predicate without a retty could better be expressed inductively" -- TODO: is this the case
+      let ⟨args, out⟩ := typeToArgArr type
+
+      let ⟨arr, id⟩ := appsToArgArr out
+      let arr ← handleRetty out arr id
+
+      let ⟨eqRpl, eqs⟩ ← equationalTransformer out arr argArr.toList
+
+      let binders := view.binders.filter (fun x => eqRpl.find? (fun v => (extractName x.id) == extractName v.fst.raw) |>.isNone )
+      let binders ← binders.mapM binderViewtoBracketedBinder
+
+      let out ← (eqs.toArray ++ args).reverse.foldlM (fun acc curr => `($curr → $acc)) isTy
+      let out ← `(ctor| | $(mkIdent nm):ident $binders* : $out)
+
+      let out ← eqRpl.foldlM (fun term ⟨src, rpl⟩ =>
+        let src := extractName src
+        term.replaceM (fun
+          | .ident _ _ nm _ =>
+            if nm == src then return some rpl
+            else return none
+          | _ => return none)) out.raw
+
+      trace[Elab.CoInductive] "Generating ctor"
+      trace[Elab.CoInductive] out
+
+      return ⟨out⟩
+
+-- TODO: handle mutual coinductive predicates
+
+def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
+  let view := views[0]!
+
+  let ⟨tyArr, out⟩ := typeToArgArr view.type
+  let argArr := (← tyArr.mapM (fun _ => Elab.Term.mkFreshBinderName)).map mkIdent
+
+  let .node _ ``Parser.Term.prop _ := out.raw | throwErrorAt out "Expected return type to be a Prop"
+
+  generateIs view argArr tyArr
+  let stx ← `(
+    def $(view.shortDeclName |> mkIdent) $(←view.binders.mapM binderViewtoBracketedBinder)* : $(view.type) :=
+      fun $argArr* => ∃ R, @$(view.shortDeclName ++ `Is |> mkIdent) $(view.binders.map (⟨·.id⟩)):ident* R ∧ R $argArr* )
+  Elab.Command.elabCommand stx
+
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 720c1c899d2e..492d64e7b98d 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -8,6 +8,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Elab.DeclUtil
 import Lean.Elab.DefView
 import Lean.Elab.Inductive
+import Lean.Elab.Coinductive
 import Lean.Elab.Structure
 import Lean.Elab.MutualDef
 import Lean.Elab.DeclarationRange
@@ -47,6 +48,7 @@ private def isNamedDef (stx : Syntax) : Bool :=
     k == ``Lean.Parser.Command.opaque ||
     k == ``Lean.Parser.Command.axiom ||
     k == ``Lean.Parser.Command.inductive ||
+    k == ``Lean.Parser.Command.coinductive ||
     k == ``Lean.Parser.Command.classInductive ||
     k == ``Lean.Parser.Command.structure
 
@@ -183,6 +185,10 @@ def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   let v ← inductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 
+def elabCoInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let v ← CoInductiveView.ofModifiersAndStx modifiers stx
+  elabCoInductiveViews #[v]
+
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let modifiers := modifiers.addAttr { name := `class }
   let v ← classInductiveSyntaxToView modifiers stx
@@ -216,6 +222,9 @@ def elabDeclaration : CommandElab := fun stx => do
     else if declKind == ``Lean.Parser.Command.«inductive» then
       let modifiers ← elabModifiers stx[0]
       elabInductive modifiers decl
+    else if declKind == ``Lean.Parser.Command.«coinductive» then
+      let modifiers ← elabModifiers stx[0]
+      elabCoInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
       let modifiers ← elabModifiers stx[0]
       elabClassInductive modifiers decl
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index e457dc8703d7..03fe329617a6 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -198,6 +198,9 @@ For more information about [inductive types](https://lean-lang.org/theorem_provi
 def «inductive»      := leading_parser
   "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
+def «coinductive»      := leading_parser
+  "coinductive " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> optional (symbol " :=" <|> " where") >>
+  many ctor >> optional (ppDedent ppLine >> computedFields) -- >> optDeriving --TODO: Handle deriving
 def classInductive   := leading_parser
   atomic (group (symbol "class " >> "inductive ")) >>
   recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >>
@@ -236,7 +239,7 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def declaration := leading_parser
   declModifiers false >>
   («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
-   «inductive» <|> classInductive <|> «structure»)
+   «coinductive» <|> «inductive» <|> classInductive <|> «structure»)
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
 @[builtin_command_parser] def noncomputableSection := leading_parser

From 409b3aa7da9be46346b8e244061f606cc34843c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 21 Aug 2024 14:16:28 +0100
Subject: [PATCH 02/10] fix: add copyright

---
 src/Lean/Elab/Coinductive.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index b3aae810795b..d1672a02f6b3 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: William Sørensen
+-/
 prelude
 import Lean.Util.CollectLevelParams
 import Lean.Elab.DeclUtil

From 6fb6f9b409161dc9ffd19c7c3e5f09321eb55b87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 21 Aug 2024 16:50:02 +0100
Subject: [PATCH 03/10] feat: add tests

---
 src/Lean/Elab/Coinductive.lean |  2 +-
 tests/lean/run/coindBisim.lean | 87 ++++++++++++++++++++++++++++++++++
 tests/lean/run/coindTypes.lean |  7 +++
 3 files changed, 95 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/coindBisim.lean
 create mode 100644 tests/lean/run/coindTypes.lean

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index d1672a02f6b3..ca2764d91329 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -50,7 +50,7 @@ structure CoInductiveView : Type where
 
 namespace CoInductiveView
 
-section
+section -- toBinderViews defn
 /--
   Given syntax of the forms
     a) (`:` term)?
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
new file mode 100644
index 000000000000..aa07d751e631
--- /dev/null
+++ b/tests/lean/run/coindBisim.lean
@@ -0,0 +1,87 @@
+structure FSM where
+  S : Type
+  d : S → Nat → S
+  A : S → Prop
+
+-- Example of a coinductive predicate defined over FSMs
+
+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))
+    → Bisim fsm s t
+
+/--
+info: inductive Bisim.Invariant : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
+number of parameters: 4
+constructors:
+Bisim.Invariant.step : ∀ {fsm : FSM} {Bisim : fsm.S → fsm.S → Prop} {x x_1 : fsm.S},
+  (fsm.A x ↔ fsm.A x_1) → (∀ (c : Nat), Bisim (fsm.d x c) (fsm.d x_1 c)) → Bisim.Invariant fsm Bisim x x_1
+-/
+#guard_msgs in
+#print Bisim.Invariant
+
+/--
+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.Invariant 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
+-/
+#guard_msgs in
+#print Bisim
+
+/-- info: 'Bisim' does not depend on any axioms -/
+#guard_msgs in
+#print axioms Bisim
+
+theorem bisim_refl : Bisim f a a := by
+  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
+  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
+  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 (fun 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⟩
+    have ⟨h_su₁, h_su₂⟩ := h_su.unfold
+    have ⟨h_ut₁, h_ut₂⟩ := h_ut.unfold
+    refine ⟨?_, ?_⟩
+    · rw [h_su₁, h_ut₁]
+    · intro c; exact ⟨_, h_su₂ c, h_ut₂ c⟩
+  · exact ⟨b, h_ab, h_bc⟩
+
+/-- info: 'bisim_refl' depends on axioms: [propext, Quot.sound] -/
+#guard_msgs in
+#print axioms bisim_refl
+
+/-- info: 'bisim_symm' depends on axioms: [propext, Quot.sound] -/
+#guard_msgs in
+#print axioms bisim_symm
+
+/-- info: 'bisim_trans' depends on axioms: [propext] -/
+#guard_msgs in
+#print axioms bisim_trans
+
diff --git a/tests/lean/run/coindTypes.lean b/tests/lean/run/coindTypes.lean
new file mode 100644
index 000000000000..e2b44ffe43b2
--- /dev/null
+++ b/tests/lean/run/coindTypes.lean
@@ -0,0 +1,7 @@
+-- Coinductive currently does only work on Prop
+
+/-- error: Expected return type to be a Prop -/
+#guard_msgs in
+coinductive S (α : Type) : Type :=
+  | cons (hd : α) (tl : S α)
+

From 8955cdf1635afb0602600dd1bcf483c7a0a7d987 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Thu, 22 Aug 2024 11:28:03 +0100
Subject: [PATCH 04/10] refactor: lift generation up to elabInductiveView for
 Shapes

---
 src/Lean/Elab/Coinductive.lean | 127 ++++++++++++++-------------------
 tests/lean/run/coindBisim.lean |  10 +--
 2 files changed, 59 insertions(+), 78 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index ca2764d91329..5c5d8b1beb59 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -30,7 +30,7 @@ structure CoInductiveView.CtorView where
   ref       : Syntax
   modifiers : Modifiers
   declName  : Name
-  binders   : Array BinderView
+  binders   : TSyntaxArray ``Lean.Parser.Term.bracketedBinder
   type?     : Option Term
   deriving Inhabited
 
@@ -140,8 +140,6 @@ private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
     throwUnsupportedSyntax
 end
 
-/- #check Lean.Elab.Binders.to -/
-
 /- open private toBinderViews from Lean.Elab.Binders in -/
 private def toBViews (stx : Syntax) : CommandElabM $ Array Elab.Term.BinderView := do
   let x ← liftTermElabM $ stx.getArgs.mapM toBinderViews
@@ -166,9 +164,7 @@ def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : Co
   addDocString' ctorName ctorModifiers.docString?
   Elab.addAuxDeclarationRanges ctorName ref ref[3]
 
-  let binders ← toBViews binders
-
-  return { ref, modifiers := ctorModifiers, declName := ctorName, binders, type? := type?.map (⟨·⟩) }
+  return { ref, modifiers := ctorModifiers, declName := ctorName, binders := binders.getArgs.map (⟨·⟩), type? := type?.map (⟨·⟩) }
 
 def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do
   let (binders, type) := Elab.expandDeclSig decl[2]!
@@ -234,93 +230,78 @@ def extractName : Syntax → Name
   | .ident _ _ nm _ => nm
   | _ => .anonymous
 
-def generateIs (topView : CoInductiveView) (argArr : Array Ident) (tyArr : Array Term) : CommandElabM Unit := do
-  let id := topView.shortDeclName ++ `Invariant
+def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM Unit := do
+  let shortDeclName := topView.shortDeclName ++ `Shape
 
-  let isTy ← `($(mkIdent id) $(topView.binders.map (⟨·.id⟩))* $(mkIdent topView.shortDeclName) $argArr*)
+  /- let v ← topView.ctors.mapM $ handleCtor $ mkIdent id -/
 
-  let v : Array (TSyntax ``ctor) ← topView.ctors.mapM $ handleCtor isTy
+  let binders := topView.binders.push ({
+      ref := .missing
+      id := mkIdent topView.shortDeclName
+      type := topView.type
+      bi := .default
+  })
 
-  let x ← argArr.zip tyArr |>.mapM (fun ⟨id, v⟩ => `(bb| ($id : $v) ))
-
-  -- TODO: Use elabInductiveViews
-  let invariant ← `(command|
-    inductive $(mkIdent id) $(←topView.binders.mapM binderViewtoBracketedBinder)* ($(topView.shortDeclName |> mkIdent) : $(topView.type)) $x* : Prop := $v*
-  )
-
-  trace[Elab.CoInductive] "Generating invariant:"
-  trace[Elab.CoInductive] invariant
+  let view : InductiveView := {
+    ref             := .missing
+    declId          := ←`(declId| $(mkIdent shortDeclName))
+    modifiers       := topView.modifiers
+    shortDeclName
+    declName        := topView.declName ++ `Shape
+    levelNames      := topView.levelNames
+    binders         := .node .none `null (←binders.mapM binderViewtoBracketedBinder)
+    type?           := some topView.type
+    ctors           := ←topView.ctors.mapM $ handleCtor $ mkIdent shortDeclName
+    derivingClasses := #[]
+    computedFields  := #[]
+  }
 
   let stx ← `(command|
     abbrev $(topView.shortDeclName ++ `Is |> mkIdent) $(←topView.binders.mapM binderViewtoBracketedBinder)* (R : $(topView.type)) : Prop :=
-      ∀ { $argArr* }, R $argArr* → $(mkIdent id) $(topView.binders.map (⟨·.id⟩))* R $argArr*)
+      ∀ { $argArr* }, R $argArr* → $(mkIdent shortDeclName) $(topView.binders.map (⟨·.id⟩))* R $argArr*)
 
   trace[Elab.CoInductive] "Generating Is check:"
   trace[Elab.CoInductive] stx
 
-  Elab.Command.elabCommand invariant
+  /- Elab.Command.elabCommand invariant -/
+  elabInductiveViews #[view]
   Elab.Command.elabCommand stx
 
   where
-    correctorIterator (loc : Term)
-      | ⟨.ident _ _ nm _⟩ :: tla, binderV :: tlb => do
-        let .ident _ _ nmx _ := binderV.id | unreachable!
-        if nm == nmx then correctorIterator loc tla tlb
-        else throwErrorAt loc s!"Expected {binderV.id}"
-      | loc :: _, binderV :: _ => throwErrorAt loc s!"Expected {binderV.id}"
-      | rest, [] =>
-        pure rest
-      | [], _ => throwErrorAt loc "Insufficent arguments"
-
-    handleRetty appl arr id := do
-      let .ident _ _ nm _ := id.raw  | throwErrorAt id s!"Expected return type to be {topView.declId}" 
-      if nm != topView.shortDeclName then throwErrorAt id s!"Expected return type to be {topView.declId}"
-
-      correctorIterator appl arr.toList topView.binders.toList
-
-    -- Removal array × Equational array
-    equationalTransformer (loc : Term) : List Term → List Ident → CommandElabM ((List (Ident × Ident)) × (List Term))
-      | [], [] => return Prod.mk [] []
-      | x@⟨.ident _ _ _ _⟩ :: tla, hdb :: tlb => do
-        let ⟨rem, eq⟩ ← equationalTransformer loc tla tlb
-        return ⟨(Prod.mk ⟨x.raw⟩ hdb) :: rem, eq⟩
-      | hda :: tla, hdb :: tlb => do
-        let ⟨rem, eq⟩ ← equationalTransformer loc tla tlb
-        return ⟨rem, (←`($hda = $hdb)) :: eq⟩
-      | [], _ | _, [] => throwErrorAt loc "Incorrect number of arguments"
-
+    split {α} : Nat → List α → (List α) × (List α)
+      | _, [] => Prod.mk [] []
+      | 0, arr => Prod.mk [] arr
+      | n+1, hd :: tl =>
+        let ⟨a, b⟩ := split n tl
+        ⟨hd :: a, b⟩
+
+    -- Coming in these have the form of  | name ... : ... Nm       topBinders...         args...
+    -- But we want them to have the form | name ... : ... Nm.Shape topBinders... RecName args...
     handleCtor isTy view := do
-      let nm := view.declName.replacePrefix topView.declName .anonymous
-
-      let .some type := view.type? | throwErrorAt view.ref "An coinductive predicate without a retty could better be expressed inductively" -- TODO: is this the case
-      let ⟨args, out⟩ := typeToArgArr type
+      let nm := view.declName.replacePrefix topView.declName (topView.declName ++ `Shape)
 
-      let ⟨arr, id⟩ := appsToArgArr out
-      let arr ← handleRetty out arr id
+      let type? ← view.type?.mapM fun type => do
+        let ⟨args, out⟩ := typeToArgArr type
 
-      let ⟨eqRpl, eqs⟩ ← equationalTransformer out arr argArr.toList
+        let ⟨arr, _⟩ := appsToArgArr out
+        let len := topView.binders.size
 
-      let binders := view.binders.filter (fun x => eqRpl.find? (fun v => (extractName x.id) == extractName v.fst.raw) |>.isNone )
-      let binders ← binders.mapM binderViewtoBracketedBinder
+        let ⟨pre, post⟩ := split len arr.toList
+        let pre         := List.toArray pre
+        let post        := List.toArray post
 
-      let out ← (eqs.toArray ++ args).reverse.foldlM (fun acc curr => `($curr → $acc)) isTy
-      let out ← `(ctor| | $(mkIdent nm):ident $binders* : $out)
+        let out ← `($isTy $pre* $(mkIdent topView.shortDeclName) $post*)
+        args.reverse.foldlM (fun acc curr => `($curr → $acc)) out
 
-      let out ← eqRpl.foldlM (fun term ⟨src, rpl⟩ =>
-        let src := extractName src
-        term.replaceM (fun
-          | .ident _ _ nm _ =>
-            if nm == src then return some rpl
-            else return none
-          | _ => return none)) out.raw
-
-      trace[Elab.CoInductive] "Generating ctor"
-      trace[Elab.CoInductive] out
-
-      return ⟨out⟩
+      return {
+        ref       := .missing
+        modifiers := view.modifiers
+        declName  := nm
+        binders   := .node .none `null (view.binders.map (·.raw))
+        type?     := type?
+      }
 
 -- TODO: handle mutual coinductive predicates
-
 def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
   let view := views[0]!
 
@@ -329,7 +310,7 @@ def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit :=
 
   let .node _ ``Parser.Term.prop _ := out.raw | throwErrorAt out "Expected return type to be a Prop"
 
-  generateIs view argArr tyArr
+  generateIs view argArr
   let stx ← `(
     def $(view.shortDeclName |> mkIdent) $(←view.binders.mapM binderViewtoBracketedBinder)* : $(view.type) :=
       fun $argArr* => ∃ R, @$(view.shortDeclName ++ `Is |> mkIdent) $(view.binders.map (⟨·.id⟩)):ident* R ∧ R $argArr* )
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
index aa07d751e631..b20a769e99ed 100644
--- a/tests/lean/run/coindBisim.lean
+++ b/tests/lean/run/coindBisim.lean
@@ -12,18 +12,18 @@ coinductive Bisim (fsm : FSM) : fsm.S → fsm.S → Prop :=
     → Bisim fsm s t
 
 /--
-info: inductive Bisim.Invariant : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
+info: inductive Bisim.Shape : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
 number of parameters: 4
 constructors:
-Bisim.Invariant.step : ∀ {fsm : FSM} {Bisim : fsm.S → fsm.S → Prop} {x x_1 : fsm.S},
-  (fsm.A x ↔ fsm.A x_1) → (∀ (c : Nat), Bisim (fsm.d x c) (fsm.d x_1 c)) → Bisim.Invariant fsm Bisim x x_1
+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
 -/
 #guard_msgs in
-#print Bisim.Invariant
+#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.Invariant fsm R x x_1
+fun fsm R => ∀ {x x_1 : fsm.S}, R x x_1 → Bisim.Shape fsm R x x_1
 -/
 #guard_msgs in
 #print Bisim.Is

From d80810071bd0b041219831633e11785b66b716f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Thu, 22 Aug 2024 15:25:16 +0100
Subject: [PATCH 05/10] refactor: remove usage of BinderViews

---
 src/Lean/Elab/Coinductive.lean | 184 ++++++---------------------------
 tests/lean/run/coindBisim.lean |   2 +-
 2 files changed, 35 insertions(+), 151 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index 5c5d8b1beb59..670fb2e9eae8 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -41,7 +41,7 @@ structure CoInductiveView : Type where
   shortDeclName   : Name
   declName        : Name
   levelNames      : List Name
-  binders         : Array BinderView
+  binders         : TSyntaxArray ``Lean.Parser.Term.bracketedBinder
   type            : Term
   ctors           : Array CoInductiveView.CtorView
   /- derivingClasses : Array Lean.Elab.DerivingClassView -/
@@ -50,101 +50,6 @@ structure CoInductiveView : Type where
 
 namespace CoInductiveView
 
-section -- toBinderViews defn
-/--
-  Given syntax of the forms
-    a) (`:` term)?
-    b) `:` term
-  return `term` if it is present, or a hole if not. -/
-private def expandBinderType (ref : Syntax) (stx : Syntax) : Syntax :=
-  if stx.getNumArgs == 0 then
-    mkHole ref
-  else
-    stx[1]
-
-/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/
-private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
-  match stx with
-  | `(_) => mkFreshIdent stx (canonical := true)
-  | _    => pure stx
-
-/--
-Expand `optional (binderTactic <|> binderDefault)`
-```
-def binderTactic  := leading_parser " := " >> " by " >> tacticParser
-def binderDefault := leading_parser " := " >> termParser
-```
--/
-private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax := do
-  if optBinderModifier.isNone then
-    return type
-  else
-    let modifier := optBinderModifier[0]
-    let kind     := modifier.getKind
-    if kind == `Lean.Parser.Term.binderDefault then
-      let defaultVal := modifier[1]
-      `(optParam $(⟨type⟩) $(⟨defaultVal⟩))
-    else if kind == `Lean.Parser.Term.binderTactic then
-      let tac := modifier[2]
-      let name ← declareTacticSyntax tac
-      `(autoParam $(⟨type⟩) $(mkIdentFrom tac name))
-    else
-      throwUnsupportedSyntax
-private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
-  ids.getArgs.mapM fun id =>
-    let k := id.getKind
-    if k == identKind || k == `Lean.Parser.Term.hole then
-      return id
-    else
-      throwErrorAt id "identifier or `_` expected"
-
-/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
-private def expandOptIdent (stx : Syntax) : TermElabM Syntax := do
-  if stx.isNone then
-    let id ← withFreshMacroScope <| MonadQuotation.addMacroScope `inst
-    return mkIdentFrom stx id
-  else
-    return stx[0]
-
-/--
-Convert `stx` into an array of `BinderView`s.
-`stx` must be an identifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
--/
-private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
-  let k := stx.getKind
-  if stx.isIdent || k == ``Lean.Parser.Term.hole then
-    -- binderIdent
-    return #[{ ref := stx, id := (← expandBinderIdent stx), type := mkHole stx, bi := .default }]
-  else if k == ``Lean.Parser.Term.explicitBinder then
-    -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
-    let ids ← getBinderIds stx[1]
-    let type        := stx[2]
-    let optModifier := stx[3]
-    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := .default }
-  else if k == ``Lean.Parser.Term.implicitBinder then
-    -- `{` binderIdent+ binderType `}`
-    let ids ← getBinderIds stx[1]
-    let type := stx[2]
-    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .implicit }
-  else if k == ``Lean.Parser.Term.strictImplicitBinder then
-    -- `⦃` binderIdent+ binderType `⦄`
-    let ids ← getBinderIds stx[1]
-    let type := stx[2]
-    ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .strictImplicit }
-  else if k == ``Lean.Parser.Term.instBinder then
-    -- `[` optIdent type `]`
-    let id ← expandOptIdent stx[1]
-    let type := stx[2]
-    return #[ { ref := id, id := id, type := type, bi := .instImplicit } ]
-  else
-    throwUnsupportedSyntax
-end
-
-/- open private toBinderViews from Lean.Elab.Binders in -/
-private def toBViews (stx : Syntax) : CommandElabM $ Array Elab.Term.BinderView := do
-  let x ← liftTermElabM $ stx.getArgs.mapM toBinderViews
-  return x.flatten
-
 def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoInductiveView.CtorView := do
   let mut ctorModifiers ← elabModifiers ref[2]
   if let some leadingDocComment := ref[0].getOptional? then
@@ -159,24 +64,24 @@ def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : Co
   checkValidCtorModifier ctorModifiers
   let ctorName := ref.getIdAt 3
   let ctorName := declName ++ ctorName
-  let ctorName ← withRef ref[3] $ Elab.applyVisibility ctorModifiers.visibility ctorName
-  let (binders, type?) := Elab.expandOptDeclSig ref[4]
+  let ctorName ← withRef ref[3] $ applyVisibility ctorModifiers.visibility ctorName
+  let (binders, type?) := expandOptDeclSig ref[4]
   addDocString' ctorName ctorModifiers.docString?
-  Elab.addAuxDeclarationRanges ctorName ref ref[3]
+  addAuxDeclarationRanges ctorName ref ref[3]
 
   return { ref, modifiers := ctorModifiers, declName := ctorName, binders := binders.getArgs.map (⟨·⟩), type? := type?.map (⟨·⟩) }
 
 def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do
-  let (binders, type) := Elab.expandDeclSig decl[2]!
+  let (binders, type) := expandDeclSig decl[2]!
 
-  let binders ← toBViews binders
+  let binders := binders.getArgs.map (⟨·⟩)
 
   let declId  := ⟨decl[1]⟩
   let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId declId.raw modifiers
 
   let ctors ← decl[4].getArgs.mapM $ CtorView.ofStx declName modifiers
 
-  Elab.addDeclarationRanges declName decl
+  addDeclarationRanges declName decl
 
   return {
     ref := ⟨decl⟩
@@ -200,56 +105,47 @@ end CoInductiveView
 
 open Parser.Term in
 section
-abbrev bb            : Lean.Parser.Parser := bracketedBinder
-abbrev matchAltExprs : Lean.Parser.Parser := matchAlts
-
-/- Since `bb` and `matchAltExprs` are aliases for `bracketedBinder`, resp. `matchAlts`,
-we can safely coerce syntax of these categories  -/
-instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder)      where coe x := ⟨x.raw⟩
-instance : Coe (TSyntax ``matchAltExprs) (TSyntax ``matchAlts) where coe x := ⟨x.raw⟩
+abbrev bb := bracketedBinder
+/- Since `bb` is an alias for `bracketedBinder`, we can safely coerce syntax of these categories  -/
+instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩
 end
 
-def binderViewtoBracketedBinder (v : BinderView) : CommandElabM $ TSyntax ``Parser.Term.bracketedBinder := do match v.bi with
-  | .default =>        `(bb|( $(⟨v.id⟩):ident : $(⟨v.type⟩) ))
-  | .implicit =>       `(bb|{ $(⟨v.id⟩):ident : $(⟨v.type⟩) })
-  | .strictImplicit => `(bb|⦃ $(⟨v.id⟩):ident : $(⟨v.type⟩) ⦄)
-  | .instImplicit =>   `(bb|[ $(⟨v.id⟩):ident : $(⟨v.type⟩) ])
+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
-    | Syntax.node _ ``Parser.Term.arrow #[hd, _, tail] => Prod.map (⟨hd⟩ :: ·) id $ go tail
+    | .node _ ``Parser.Term.arrow #[hd, _, tail] => Prod.map (⟨hd⟩ :: ·) id $ go tail
     | rest => ⟨[], ⟨rest⟩⟩
 
 def appsToArgArr (type : Term) : Array Term × Term := match type.raw with
-    | Syntax.node _ ``Parser.Term.app #[v, cont] => ⟨cont.getArgs.map (⟨·⟩), ⟨v⟩⟩
-    | rest => ⟨#[], ⟨rest⟩⟩
-
-deriving instance Repr for BinderView
+  | .node _ ``Parser.Term.app #[v, cont] => ⟨cont.getArgs.map (⟨·⟩), ⟨v⟩⟩
+  | rest => ⟨#[], ⟨rest⟩⟩
 
 def extractName : Syntax → Name
   | .ident _ _ nm _ => nm
   | _ => .anonymous
 
+
+def split : Nat → List α → (List α) × (List α)
+  | _, []  => ⟨[], []⟩
+  | 0, arr => ⟨[], arr⟩
+  | n+1, hd :: tl => Prod.map (hd :: ·) id $ split n tl
+
 def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM Unit := do
   let shortDeclName := topView.shortDeclName ++ `Shape
 
-  /- let v ← topView.ctors.mapM $ handleCtor $ mkIdent id -/
+  let v ← `(bb| ($(mkIdent topView.shortDeclName) : $(topView.type)) )
 
-  let binders := topView.binders.push ({
-      ref := .missing
-      id := mkIdent topView.shortDeclName
-      type := topView.type
-      bi := .default
-  })
-
-  let view : InductiveView := {
+  let view := {
     ref             := .missing
     declId          := ←`(declId| $(mkIdent shortDeclName))
     modifiers       := topView.modifiers
     shortDeclName
     declName        := topView.declName ++ `Shape
     levelNames      := topView.levelNames
-    binders         := .node .none `null (←binders.mapM binderViewtoBracketedBinder)
+    binders         := .node .none `null $ topView.binders.push v
     type?           := some topView.type
     ctors           := ←topView.ctors.mapM $ handleCtor $ mkIdent shortDeclName
     derivingClasses := #[]
@@ -257,24 +153,16 @@ def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM
   }
 
   let stx ← `(command|
-    abbrev $(topView.shortDeclName ++ `Is |> mkIdent) $(←topView.binders.mapM binderViewtoBracketedBinder)* (R : $(topView.type)) : Prop :=
-      ∀ { $argArr* }, R $argArr* → $(mkIdent shortDeclName) $(topView.binders.map (⟨·.id⟩))* R $argArr*)
+    abbrev $(mkIdent $ topView.shortDeclName ++ `Is) $(topView.binders)* (R : $(topView.type)) : Prop :=
+      ∀ { $argArr* }, R $argArr* → $(mkIdent shortDeclName) $((topView.binders.map extractIds).flatten)* R $argArr*)
 
   trace[Elab.CoInductive] "Generating Is check:"
   trace[Elab.CoInductive] stx
 
-  /- Elab.Command.elabCommand invariant -/
   elabInductiveViews #[view]
-  Elab.Command.elabCommand stx
+  elabCommand stx
 
   where
-    split {α} : Nat → List α → (List α) × (List α)
-      | _, [] => Prod.mk [] []
-      | 0, arr => Prod.mk [] arr
-      | n+1, hd :: tl =>
-        let ⟨a, b⟩ := split n tl
-        ⟨hd :: a, b⟩
-
     -- Coming in these have the form of  | name ... : ... Nm       topBinders...         args...
     -- But we want them to have the form | name ... : ... Nm.Shape topBinders... RecName args...
     handleCtor isTy view := do
@@ -282,13 +170,9 @@ def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM
 
       let type? ← view.type?.mapM fun type => do
         let ⟨args, out⟩ := typeToArgArr type
-
         let ⟨arr, _⟩ := appsToArgArr out
-        let len := topView.binders.size
 
-        let ⟨pre, post⟩ := split len arr.toList
-        let pre         := List.toArray pre
-        let post        := List.toArray post
+        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
@@ -306,13 +190,13 @@ def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit :=
   let view := views[0]!
 
   let ⟨tyArr, out⟩ := typeToArgArr view.type
-  let argArr := (← tyArr.mapM (fun _ => Elab.Term.mkFreshBinderName)).map mkIdent
+  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"
 
   generateIs view argArr
-  let stx ← `(
-    def $(view.shortDeclName |> mkIdent) $(←view.binders.mapM binderViewtoBracketedBinder)* : $(view.type) :=
-      fun $argArr* => ∃ R, @$(view.shortDeclName ++ `Is |> mkIdent) $(view.binders.map (⟨·.id⟩)):ident* R ∧ R $argArr* )
-  Elab.Command.elabCommand stx
+  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
 
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
index b20a769e99ed..cedb2828440a 100644
--- a/tests/lean/run/coindBisim.lean
+++ b/tests/lean/run/coindBisim.lean
@@ -62,7 +62,7 @@ theorem Bisim.unfold {f} : Bisim.Is f (Bisim f) := by
 
 theorem bisim_trans (h_ab : Bisim f a b) (h_bc : Bisim f b c) :
     Bisim f a c := by
-  exists (fun s t => ∃ u, Bisim f s u ∧ Bisim f u t)
+  exists (∃ u, Bisim f · u ∧ Bisim f u ·)
   constructor
   intro s t h_Rst
   · rcases h_Rst with ⟨u, h_su, h_ut⟩

From 0615cb515653a1bfecfb53480458c2a24f58a0e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Thu, 22 Aug 2024 17:16:48 +0100
Subject: [PATCH 06/10] feat: make relation more general readying for mutuals

---
 src/Lean/Elab/Coinductive.lean | 44 +++++++++++++++++++++++++++-------
 tests/lean/run/coindBisim.lean | 22 ++++++++---------
 2 files changed, 46 insertions(+), 20 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index 670fb2e9eae8..c877e9e8d7fb 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/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
 
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
index cedb2828440a..ba7195d7f8f1 100644
--- a/tests/lean/run/coindBisim.lean
+++ b/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,21 +40,21 @@ 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
@@ -62,7 +62,7 @@ theorem Bisim.unfold {f} : Bisim.Is f (Bisim f) := by
 
 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⟩

From fa1545fc74b7d738dd9b1a33fd6ca15099e23cf4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Fri, 23 Aug 2024 13:45:25 +0100
Subject: [PATCH 07/10] feat: mutual co-inductives

---
 src/Lean/Elab/Coinductive.lean | 141 ++++++++++++++++-----------------
 tests/lean/run/coindBisim.lean |   4 +-
 2 files changed, 71 insertions(+), 74 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index c877e9e8d7fb..f34065b41fae 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -138,91 +138,88 @@ def split : Nat → List α → (List α) × (List α)
   | 0, arr => ⟨[], arr⟩
   | n+1, hd :: tl => Prod.map (hd :: ·) id $ split n tl
 
-def generateIs (topView : CoInductiveView) (argArr : Array Ident) : CommandElabM Unit := do
-  let shortDeclName := topView.shortDeclName ++ `Shape
 
-  let v ← `(bb| ($(mkIdent topView.shortDeclName) : $(←topView.toRelType)) )
-
-  let view := {
-    ref             := .missing
-    declId          := ←`(declId| $(mkIdent shortDeclName))
-    modifiers       := topView.modifiers
-    shortDeclName
-    declName        := topView.declName ++ `Shape
-    levelNames      := topView.levelNames
-    binders         := .node .none `null $ topView.binders.push v
-    type?           := some topView.type
-    ctors           := ←topView.ctors.mapM $ handleCtor $ mkIdent shortDeclName
-    derivingClasses := #[]
-    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.toRelType)) : Prop :=
-      ∀ { $argArr* }, R $(topView.toBinderIds)* $argArr* → $(mkIdent shortDeclName) $(topView.toBinderIds)* R $argArr*)
-
-  trace[Elab.CoInductive] "Generating Is check:"
-  trace[Elab.CoInductive] stx
-
-  elabInductiveViews #[view]
-  elabCommand stx
-
-  where
     -- Coming in these have the form of  | name ... : ... Nm       topBinders...         args...
     -- But we want them to have the form | name ... : ... Nm.Shape topBinders... RecName args...
-    handleCtor isTy view := do
-      let nm := view.declName.replacePrefix topView.declName (topView.declName ++ `Shape)
-
-      let type? ← view.type?.mapM fun type => do
-        let ⟨args, out⟩ := typeToArgArr type
-        let ⟨arr, _⟩ := appsToArgArr out
+def handleCtor (names : Array Ident) (topView : CoInductiveView) (isTy : Ident) (view : CoInductiveView.CtorView) : CommandElabM CtorView := do
+  let nm := view.declName.replacePrefix topView.declName (topView.declName ++ `Shape)
 
-        let ⟨pre, post⟩ := (split topView.binders.size arr.toList).map (·.toArray) (·.toArray)
+  let type? ← view.type?.mapM fun type => do
+    let ⟨args, out⟩ := typeToArgArr type
+    let ⟨arr, _⟩ := appsToArgArr out
 
-        let out ← `($isTy $pre* $(mkIdent topView.shortDeclName) $post*)
+    let ⟨pre, post⟩ := (split topView.binders.size arr.toList).map (·.toArray) (·.toArray)
 
-        args.reverse.foldlM (fun acc curr => `($curr → $acc)) out
+    let out ← `($isTy $pre* $names* $post*)
 
-      return {
-        ref       := .missing
-        modifiers := view.modifiers
-        declName  := nm
-        binders   := .node .none `null (view.binders.map (·.raw))
-        type?     := type?
-      }
+    args.reverse.foldlM (fun acc curr => `($curr → $acc)) out
 
-/- def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do -/
-/-   let view := views[0]! -/
+  return {
+    ref       := .missing
+    modifiers := view.modifiers
+    declName  := nm
+    binders   := .node .none `null (view.binders.map (·.raw))
+    type?     := type?
+  }
 
-/-   let viewCheck ← views.mapM fun view => do -/
-/-     let ⟨tyArr, out⟩ := typeToArgArr view.type -/
-/-     let argArr := (← tyArr.mapM (fun _ => mkFreshBinderName)).map mkIdent -/
+def generateIs (vss : Array (CoInductiveView × Array Ident)) (rNameEntries : Array (Ident × Term)) : CommandElabM Unit := do
+  -- It could be worth making this extract only the names that are required.
+  let boundRNames ← rNameEntries.mapM (fun ⟨i, v⟩ => do `(bb| ( $i : $v) ))
+  let coRecArgs   ← vss.mapM (fun ⟨v, _⟩ => do `(bb| ( $(mkIdent $ v.shortDeclName) : $(←v.toRelType))))
+  let names      := vss.map  (mkIdent ·.fst.shortDeclName)
+
+  for ⟨idx, topView, argArr⟩ in vss.toList.enum.toArray do
+    let shortDeclName := topView.shortDeclName ++ `Shape
+
+    let view := {
+      ref             := .missing
+      declId          := ←`(declId| $(mkIdent shortDeclName))
+      modifiers       := topView.modifiers
+      shortDeclName
+      declName        := topView.declName ++ `Shape
+      levelNames      := topView.levelNames
+      binders         := .node .none `null $ topView.binders.append coRecArgs
+      type?           := some topView.type
+      ctors           := ←topView.ctors.mapM $ handleCtor names topView $ mkIdent shortDeclName
+      derivingClasses := #[]
+      computedFields  := #[]
+    }
+
+    trace[Elab.CoInductive] s!"{repr topView.binders}"
+    trace[Elab.CoInductive] s!"{topView.toBinderIds}"
+
+    let boundNames := rNameEntries.map Prod.fst
+    let i := boundNames[idx]! -- OK since these come from the same source
+
+    let stx ← `(command|
+      abbrev $(mkIdent $ topView.shortDeclName ++ `Is) $(topView.binders)* $boundRNames* : Prop :=
+        ∀ { $argArr* }, $i $(topView.toBinderIds)* $argArr* → $(mkIdent shortDeclName) $(topView.toBinderIds)* $boundNames* $argArr*)
+
+    trace[Elab.CoInductive] "Generating Is check:"
+    trace[Elab.CoInductive] stx
+
+    elabInductiveViews #[view]
+    elabCommand stx
 
-/-     -- 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 -/
+def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
+  let viewCheck ← views.mapM fun view => do
+    let ⟨tyArr, out⟩ := typeToArgArr view.type
+    let argArr := (← tyArr.mapM (fun _ => mkFreshBinderName)).map mkIdent
 
-/-   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 -/
+    -- 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
 
--- TODO: handle mutual coinductive predicates
-def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
-  let view := views[0]!
+  let rNameEntries ← viewCheck.mapM (fun ⟨v, _⟩ => return Prod.mk (mkIdent $ ←mkFreshBinderName) (←v.toRelType))
 
-  let ⟨tyArr, out⟩ := typeToArgArr view.type
-  let argArr := (← tyArr.mapM (fun _ => mkFreshBinderName)).map mkIdent
+  generateIs viewCheck rNameEntries
+  for ⟨idx, view, argArr⟩ in viewCheck.toList.enum.toArray do
+    let boundNames := rNameEntries.map Prod.fst
+    let i := boundNames[idx]! -- OK since these come from the same source
 
-  -- 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"
+    let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
+      ∃ $[$boundNames:ident]*, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* $boundNames* ∧ $i $(view.toBinderIds)* $argArr*)
 
-  generateIs view argArr
-  let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
-    ∃ R, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* R ∧ R $(view.toBinderIds)* $argArr*)
-  elabCommand stx
+    trace[Elab.CoInductive] stx
+    elabCommand stx
 
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
index ba7195d7f8f1..e1f7ebdf1b34 100644
--- a/tests/lean/run/coindBisim.lean
+++ b/tests/lean/run/coindBisim.lean
@@ -23,14 +23,14 @@ Bisim.Shape.step : ∀ {fsm : FSM} {Bisim : (fsm : FSM) → fsm.S → fsm.S →
 
 /--
 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
+fun fsm x => ∀ {x_1 x_2 : fsm.S}, x fsm x_1 x_2 → Bisim.Shape fsm x x_1 x_2
 -/
 #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 fsm x x_1
+fun fsm x x_1 => ∃ x_2, Bisim.Is fsm x_2 ∧ x_2 fsm x x_1
 -/
 #guard_msgs in
 #print Bisim

From b4b2ad3294ff106fdc4646bc2e80a7f431fceb5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Fri, 23 Aug 2024 13:47:36 +0100
Subject: [PATCH 08/10] fix: imports

---
 src/Lean/Elab/Coinductive.lean | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index f34065b41fae..6bf02e549136 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -4,20 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: William Sørensen
 -/
 prelude
-import Lean.Util.CollectLevelParams
-import Lean.Elab.DeclUtil
-import Lean.Elab.DefView
-import Lean.Elab.Inductive
-import Lean.Elab.Structure
-import Lean.Elab.MutualDef
-import Lean.Elab.DeclarationRange
-
-import Lean.Util.Trace
-import Lean.Elab.Binders
-import Lean.Elab.DeclarationRange
 import Lean.Elab.Command
-import Lean.Elab.Inductive
+import Lean.Elab.DeclarationRange
 import Lean.Elab.Exception
+import Lean.Elab.Inductive
+import Lean.Util.Trace
 
 namespace Lean.Elab.Command
 

From 92ef36f03119907913a8ed67b746ec47f24df9da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Fri, 23 Aug 2024 13:49:32 +0100
Subject: [PATCH 09/10] fix: add trace comment

---
 src/Lean/Elab/Coinductive.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index 6bf02e549136..f0558b0eac20 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -211,6 +211,7 @@ def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit :=
     let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
       ∃ $[$boundNames:ident]*, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* $boundNames* ∧ $i $(view.toBinderIds)* $argArr*)
 
+    trace[Elab.CoInductive] "Generating co-inductive:"
     trace[Elab.CoInductive] stx
     elabCommand stx
 

From a3a1f531ae311e3c6d7ebc4c1bd5e64a96388d66 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Fri, 23 Aug 2024 17:32:41 +0100
Subject: [PATCH 10/10] fix: add comments

---
 src/Lean/Elab/Coinductive.lean | 132 +++++++++++++++++++++------------
 src/Lean/Elab/Declaration.lean |   8 +-
 2 files changed, 88 insertions(+), 52 deletions(-)

diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index f0558b0eac20..f5df85f6e95b 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -15,9 +15,9 @@ namespace Lean.Elab.Command
 open Lean Lean.Elab Lean.Elab.Term Lean.Parser Command
 
 builtin_initialize
-  registerTraceClass `Elab.CoInductive
+  registerTraceClass `Elab.Coinductive
 
-structure CoInductiveView.CtorView where
+structure CoinductiveView.CtorView where
   ref       : Syntax
   modifiers : Modifiers
   declName  : Name
@@ -25,7 +25,7 @@ structure CoInductiveView.CtorView where
   type?     : Option Term
   deriving Inhabited
 
-structure CoInductiveView where
+structure CoinductiveView where
   ref             : TSyntax ``Lean.Parser.Command.coinductive
   declId          : TSyntax ``Parser.Command.declId
   modifiers       : Modifiers
@@ -34,14 +34,15 @@ structure CoInductiveView where
   levelNames      : List Name
   binders         : TSyntaxArray ``Lean.Parser.Term.bracketedBinder
   type            : Term
-  ctors           : Array CoInductiveView.CtorView
-  /- derivingClasses : Array Lean.Elab.DerivingClassView -/
-  /- computedFields  : Array Lean.Elab.Command.ComputedFieldView -/
+  ctors           : Array CoinductiveView.CtorView
   deriving Inhabited
 
-namespace CoInductiveView
+namespace CoinductiveView
 
-def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoInductiveView.CtorView := do
+/--
+  Create a CtorView from a Name, some Modifiers, and Syntax
+-/
+def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoinductiveView.CtorView := do
   let mut ctorModifiers ← elabModifiers ref[2]
   if let some leadingDocComment := ref[0].getOptional? then
     if ctorModifiers.docString?.isSome then
@@ -62,7 +63,10 @@ def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : Co
 
   return { ref, modifiers := ctorModifiers, declName := ctorName, binders := binders.getArgs.map (⟨·⟩), type? := type?.map (⟨·⟩) }
 
-def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do
+/--
+  Create a CoinductiveView from Modifiers and Syntax
+-/
+def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoinductiveView := do
   let (binders, type) := expandDeclSig decl[2]!
 
   let binders := binders.getArgs.map (⟨·⟩)
@@ -90,49 +94,64 @@ def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoI
     modifiers
   }
 
-def ofStx (stx : Syntax) := elabModifiers stx[0] >>= (ofModifiersAndStx · stx[1])
+def ofStx (stx : Syntax) : CommandElabM CoinductiveView := 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 getBracketedBinderIds).flatten.map mkIdent
 
-def toBinderIds (c : CoInductiveView) : Array Ident := (c.binders.map extractIds).flatten
-
-def toRelType (c : CoInductiveView) : CommandElabM Term :=
+def toRelType (c : CoinductiveView) : CommandElabM Term :=
   c.binders.reverse.foldlM (fun curr acc => `($acc:bracketedBinder → $curr)) c.type
 
-end CoInductiveView
+end CoinductiveView
 
 open Parser.Term in
 section
-abbrev bb := bracketedBinder
-/- Since `bb` is an alias for `bracketedBinder`, we can safely coerce syntax of these categories  -/
+
+/-- `bb`s are an alias for `bracketedBinder` and used in quotations -/
+private abbrev bb := bracketedBinder
+/-- Since `bb` is an alias for `bracketedBinder`, we can safely coerce syntax of these categories  -/
 instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩
+
 end
 
+-- TODO: Use elaboration over syntax manipulation
+/--
+  Extract the types and the bottom value like the following:
 
-partial def typeToArgArr (type : Term) : Array Term × Term := Prod.map List.toArray id $ go type.raw
+  > a → ⋯ → bot
+  > ⟨#[a, ⋯], bot⟩
+-/
+private partial def typeToArgArr (type : Term) : Array Term × Term := Prod.map List.toArray id $ go type.raw
   where go
     | .node _ ``Parser.Term.arrow #[hd, _, tail] => Prod.map (⟨hd⟩ :: ·) id $ go tail
     | rest => ⟨[], ⟨rest⟩⟩
 
-def appsToArgArr (type : Term) : Array Term × Term := match type.raw with
+/--
+  Extract the args of a function
+
+  > bot a ⋯
+  > ⟨#[a, ⋯], bot⟩
+-/
+private def appsToArgArr (type : Term) : Array Term × Term := match type.raw with
   | .node _ ``Parser.Term.app #[v, cont] => ⟨cont.getArgs.map (⟨·⟩), ⟨v⟩⟩
   | rest => ⟨#[], ⟨rest⟩⟩
 
-def extractName : Syntax → Name
-  | .ident _ _ nm _ => nm
-  | _ => .anonymous
+/--
+  Given a list [a, b, c] split lets you split it into two arrays
 
-def split : Nat → List α → (List α) × (List α)
+  > example : split 2 [1, 2, 3] = ⟨[1, 2], [3]⟩ := by simp [split]
+-/
+private def split : Nat → List α → (List α) × (List α)
   | _, []  => ⟨[], []⟩
   | 0, arr => ⟨[], arr⟩
   | n+1, hd :: tl => Prod.map (hd :: ·) id $ split n tl
 
+/--
+  Coming in these have the form of  | name ... : ... → Nm       topBinders...         args...
+  But we want them to have the form | name ... : ... → Nm.Shape topBinders... RecName args...
 
-    -- Coming in these have the form of  | name ... : ... Nm       topBinders...         args...
-    -- But we want them to have the form | name ... : ... Nm.Shape topBinders... RecName args...
-def handleCtor (names : Array Ident) (topView : CoInductiveView) (isTy : Ident) (view : CoInductiveView.CtorView) : CommandElabM CtorView := do
+  To do this we simply replace the out type.
+-/
+private def handleCtor (names : Array Ident) (topView : CoinductiveView) (isTy : Ident) (view : CoinductiveView.CtorView) : CommandElabM CtorView := do
   let nm := view.declName.replacePrefix topView.declName (topView.declName ++ `Shape)
 
   let type? ← view.type?.mapM fun type => do
@@ -153,13 +172,17 @@ def handleCtor (names : Array Ident) (topView : CoInductiveView) (isTy : Ident)
     type?     := type?
   }
 
-def generateIs (vss : Array (CoInductiveView × Array Ident)) (rNameEntries : Array (Ident × Term)) : CommandElabM Unit := do
+/--
+  Coinductive predicates need a shape construct.
+  These are inductive datatypes that have the same constructors without any level of recursion.
+  These are then applied in the fixed point.
+-/
+private def generateShapes (vss : Array (CoinductiveView × Array Ident)) : CommandElabM Unit := do
   -- It could be worth making this extract only the names that are required.
-  let boundRNames ← rNameEntries.mapM (fun ⟨i, v⟩ => do `(bb| ( $i : $v) ))
   let coRecArgs   ← vss.mapM (fun ⟨v, _⟩ => do `(bb| ( $(mkIdent $ v.shortDeclName) : $(←v.toRelType))))
   let names      := vss.map  (mkIdent ·.fst.shortDeclName)
 
-  for ⟨idx, topView, argArr⟩ in vss.toList.enum.toArray do
+  elabInductiveViews $ ←vss.mapM fun ⟨topView, _⟩ => do
     let shortDeclName := topView.shortDeclName ++ `Shape
 
     let view := {
@@ -176,8 +199,19 @@ def generateIs (vss : Array (CoInductiveView × Array Ident)) (rNameEntries : Ar
       computedFields  := #[]
     }
 
-    trace[Elab.CoInductive] s!"{repr topView.binders}"
-    trace[Elab.CoInductive] s!"{topView.toBinderIds}"
+    trace[Elab.Coinductive] s!"{repr topView.binders}"
+
+    return view
+/--
+  `Is` is a predicate on the relation used to generate the coinductive predicate.
+  It ensures it satisfies the declaration given.
+-/
+private def generateIs (vss : Array (CoinductiveView × Array Ident)) (rNameEntries : Array (Ident × Term)) : CommandElabM Unit := do
+  -- It could be worth making this extract only the names that are required.
+  let boundRNames ← rNameEntries.mapM fun ⟨i, v⟩ => do `(bb| ( $i : $v ) )
+
+  for ⟨idx, topView, argArr⟩ in vss.toList.enum do
+    let shortDeclName := topView.shortDeclName ++ `Shape
 
     let boundNames := rNameEntries.map Prod.fst
     let i := boundNames[idx]! -- OK since these come from the same source
@@ -186,32 +220,34 @@ def generateIs (vss : Array (CoInductiveView × Array Ident)) (rNameEntries : Ar
       abbrev $(mkIdent $ topView.shortDeclName ++ `Is) $(topView.binders)* $boundRNames* : Prop :=
         ∀ { $argArr* }, $i $(topView.toBinderIds)* $argArr* → $(mkIdent shortDeclName) $(topView.toBinderIds)* $boundNames* $argArr*)
 
-    trace[Elab.CoInductive] "Generating Is check:"
-    trace[Elab.CoInductive] stx
+    trace[Elab.Coinductive] "Generating Is check:"
+    trace[Elab.Coinductive] stx
+
+    elabCommand stx
+
+private def generateCoinductive (vss : Array (CoinductiveView × Array Ident)) (rNameEntries : Array (Ident × Term)) : CommandElabM Unit := do
+  for ⟨idx, view, argArr⟩ in vss.toList.enum do
+    let boundNames := rNameEntries.map Prod.fst
+    let i := boundNames[idx]!
+
+    let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
+      ∃ $[$boundNames:ident]*, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* $boundNames* ∧ $i $(view.toBinderIds)* $argArr*)
 
-    elabInductiveViews #[view]
+    trace[Elab.Coinductive] "Generating co-inductive:"
+    trace[Elab.Coinductive] stx
     elabCommand stx
 
-def elabCoInductiveViews (views : Array CoInductiveView) : CommandElabM Unit := do
+def elabCoinductiveViews (views : Array CoinductiveView) : CommandElabM Unit := do
   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
 
   let rNameEntries ← viewCheck.mapM (fun ⟨v, _⟩ => return Prod.mk (mkIdent $ ←mkFreshBinderName) (←v.toRelType))
 
+  generateShapes viewCheck
   generateIs viewCheck rNameEntries
-  for ⟨idx, view, argArr⟩ in viewCheck.toList.enum.toArray do
-    let boundNames := rNameEntries.map Prod.fst
-    let i := boundNames[idx]! -- OK since these come from the same source
-
-    let stx ← `(def $(mkIdent view.shortDeclName) $(view.binders)* : $(view.type) := fun $argArr* =>
-      ∃ $[$boundNames:ident]*, @$(mkIdent $ view.shortDeclName ++ `Is) $(view.toBinderIds)* $boundNames* ∧ $i $(view.toBinderIds)* $argArr*)
-
-    trace[Elab.CoInductive] "Generating co-inductive:"
-    trace[Elab.CoInductive] stx
-    elabCommand stx
+  generateCoinductive viewCheck rNameEntries
 
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 492d64e7b98d..56f1a569a5fc 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -185,9 +185,9 @@ def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   let v ← inductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 
-def elabCoInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let v ← CoInductiveView.ofModifiersAndStx modifiers stx
-  elabCoInductiveViews #[v]
+def elabCoinductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let v ← CoinductiveView.ofModifiersAndStx modifiers stx
+  elabCoinductiveViews #[v]
 
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let modifiers := modifiers.addAttr { name := `class }
@@ -224,7 +224,7 @@ def elabDeclaration : CommandElab := fun stx => do
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«coinductive» then
       let modifiers ← elabModifiers stx[0]
-      elabCoInductive modifiers decl
+      elabCoinductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
       let modifiers ← elabModifiers stx[0]
       elabClassInductive modifiers decl