Skip to content

Commit

Permalink
feat: mutual co-inductives
Browse files Browse the repository at this point in the history
  • Loading branch information
William Sørensen committed Aug 23, 2024
1 parent 0615cb5 commit fa1545f
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 74 deletions.
141 changes: 69 additions & 72 deletions src/Lean/Elab/Coinductive.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

4 changes: 2 additions & 2 deletions tests/lean/run/coindBisim.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit fa1545f

Please sign in to comment.