feat: add simple co-inductive predicates #17

Equilibris · 2024-08-21T13:09:37Z

Add basic implementation of co-inductive predicates using cofix points expressed as existential quantifications. This is done by first generating a Shape inductive datatype then quantifying over this. For example, if this were to be hand implemented in the context of a bisimulation it looks something like this:

import Matlib.Data.Set.Basic

structure FSM where
  S : Type
  d : S -> Set S
  A : Set S

def IsBisim (fsm : FSM) (R : fsm.S → fsm.S → Prop) : Prop :=
  ∀ s t, R s t →
    (s ∈ fsm.A ↔ t ∈ fsm.A)
    ∧ (∀ s' ∈ fsm.d s, ∃ t' ∈ fsm.d t, R s' t')
    ∧ (∀ t' ∈ fsm.d t, ∃ s' ∈ fsm.d s, R s' t')

def Bisim (fsm : FSM) : fsm.S → fsm.S → Prop :=
  fun s t => ∃ R, IsBisim fsm R ∧ R s t

(example by @alexkeizer )

This is writable if hard, rather, a new syntax is added in this PR that looks like the following:

coinductive Bisim (fsm : FSM) : fsm.S → fsm.S → Prop
  | step {s t : fsm.S} :
    (s ∈ fsm.A ↔ t ∈ fsm.A)
    → (∀ s' ∈ fsm.d s, ∃ t' ∈ fsm.d t, Bisim fsm s' t')
    → (∀ t' ∈ fsm.d t, ∃ s' ∈ fsm.d s, Bisim fsm s' t')
    → Bisim fsm s t

An example of what this yields is generated in the test coindBisim.lean.

Currently, this does only hold for co-inductive predicates (i.e. the ones that reside in Prop).

The generation of shape types is done by taking the original written syntax and simply adding another parameter with the name and signature of the entire expression. In the case of Bisim this shape looks like this:

inductive Bisim.Shape (fsm : FSM) (Bisim : (fsm : FSM) → fsm.S → fsm.S → Prop) : fsm.S → fsm.S → Prop
  | step {s t : fsm.S} :
    (s ∈ fsm.A ↔ t ∈ fsm.A)
    → (∀ s' ∈ fsm.d s, ∃ t' ∈ fsm.d t, Bisim fsm s' t')
    → (∀ t' ∈ fsm.d t, ∃ s' ∈ fsm.d s, Bisim fsm s' t')
    → Bisim.Shape fsm Bisim s t

The fixed point is then found with the same means as listed above.

TODOs:

Tests
- Base tests
- Mutual tests
Mutual coinductives
- These could be added by allowing the type to contain multiple parameters as inputs which are then quantified over separately in the code
toBinderViews alternatives
Alternative to how quoting bracketed binders works currently
Fixing imports

tobiasgrosser · 2024-08-22T09:07:33Z

src/Lean/Elab/Coinductive.lean

+/- #check Lean.Elab.Binders.to -/
+


Suggested change

/- #check Lean.Elab.Binders.to -/

tobiasgrosser · 2024-08-22T09:07:50Z

src/Lean/Elab/Coinductive.lean

+we can safely coerce syntax of these categories  -/
+instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder)      where coe x := ⟨x.raw⟩


Suggested change

we can safely coerce syntax of these categories -/

instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩

we can safely coerce syntax of these categories. -/

instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩

alexkeizer · 2024-08-23T12:50:07Z

Mutual coinductives
These could be added by allowing the type to contain multiple parameters as inputs which are then quantified over seperately > in the code

Let's not worry about mutuals at all in this first PR

alexkeizer

I gave it a look over. @Equilibris it would help a lot if you did a pass and document all the various functions that you've defined

This doesn't feel ready to be PRd to core yet. I think we should look into how hard it would be to go the proper route and elaborate into Exprs

alexkeizer · 2024-08-23T12:50:46Z

src/Lean/Elab/Coinductive.lean

+  /- derivingClasses : Array Lean.Elab.DerivingClassView -/
+  /- computedFields  : Array Lean.Elab.Command.ComputedFieldView -/


Suggested change

/- derivingClasses : Array Lean.Elab.DerivingClassView -/

/- computedFields : Array Lean.Elab.Command.ComputedFieldView -/

Just remove these if we don't want to support them

alexkeizer · 2024-08-23T12:54:18Z

src/Lean/Elab/Coinductive.lean

+structure CoInductiveView.CtorView where
+  ref       : Syntax
+  modifiers : Modifiers
+  declName  : Name
+  binders   : TSyntaxArray ``Lean.Parser.Term.bracketedBinder
+  type?     : Option Term
+  deriving Inhabited


Isn't this the exact same as the already existing CtorView, do you reckon we could just reuse that struct instead of defining our own?

The reason I defined this is because the original uses Syntax instead of TSyntax at multiple places. I can change over to theirs and add casts and stuff if you'd prefer

alexkeizer · 2024-08-23T12:57:25Z

src/Lean/Elab/Coinductive.lean

+  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"


Suggested change

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"

if ctorModifiers.isPrivate && modifiers.isPrivate then

throwError "invalid 'private' constructor in a 'private' coinductive predicate"

if ctorModifiers.isProtected && modifiers.isPrivate then

throwError "invalid 'protected' constructor in a 'private' coinductive predicate"

I assume you copied this code from somewhere, can we not reuse that?

Yes this is almost identical to the code to generate an InductiveView but the difference is TSyntax as mentioned above. Once again if its preferred to use Syntax we can just use theirs.

alexkeizer · 2024-08-23T12:58:19Z

src/Lean/Elab/Coinductive.lean

+
+namespace CoInductiveView
+
+def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoInductiveView.CtorView := do


alexkeizer · 2024-08-23T12:58:28Z

src/Lean/Elab/Coinductive.lean

+
+  return { ref, modifiers := ctorModifiers, declName := ctorName, binders := binders.getArgs.map (⟨·⟩), type? := type?.map (⟨·⟩) }
+
+def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do


alexkeizer · 2024-08-23T13:09:29Z

tests/lean/run/coindBisim.lean

+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 : 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
+-/


This doesn't feel right. FSM is a fixed parameter to Bisim (it is given as a binder, before the :), and should not show up in the motive. That is, I would've expected this to have type
(fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop

alexkeizer · 2024-08-23T13:13:57Z

src/Lean/Elab/Coinductive.lean

+    -- 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


How would you change the existential? The reason this works is because Prop is impredicative (which is a funny way of saying that Prop -> Prop is of type Prop). Once you start looking at types, you run into the issue that Type -> Type lives in Type 1, causing nasty universe bumps.

If you meant "pull in QpfTypes", sure, but that is very explicitly not something that core wants

Suggested change

-- 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 .node _ ``Parser.Term.prop _ := out.raw | throwErrorAt out "Expected return type to be a Prop"

return Prod.mk view argArr

alexkeizer · 2024-08-23T13:15:10Z

src/Lean/Elab/Coinductive.lean

+builtin_initialize
+  registerTraceClass `Elab.CoInductive
+
+structure CoInductiveView.CtorView where


Suggested change

structure CoInductiveView.CtorView where

structure CoinductiveView.CtorView where

Very minor nit, but I'd consider coinductive to be one word, and thus not capitalize the I in names

alexkeizer · 2024-08-23T13:16:25Z

src/Lean/Elab/Coinductive.lean

+def extractName : Syntax → Name
+  | .ident _ _ nm _ => nm
+  | _ => .anonymous


this exists already, Ident.getId or something similar

alexkeizer · 2024-08-23T13:17:57Z

src/Lean/Elab/Coinductive.lean

+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
+  | .node _ ``Parser.Term.app #[v, cont] => ⟨cont.getArgs.map (⟨·⟩), ⟨v⟩⟩
+  | rest => ⟨#[], ⟨rest⟩⟩
+


Manipulating Syntax like this feels rather brittle. This was fine for QpfTypes, where I number one priority was to get something that at least kind of works, but if we want to PR to core, we should strongly consider going the proper route and elaborating into Exprs

tobiasgrosser · 2024-08-23T16:42:45Z

src/Lean/Elab/Coinductive.lean

@@ -0,0 +1,253 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.


Should this have a Lean-FRO copyright?

William Sørensen added 3 commits August 21, 2024 11:16

feat: add simple co-inductive predicates

a88d3b2

fix: add copyright

409b3aa

feat: add tests

6fb6f9b

tobiasgrosser reviewed Aug 22, 2024

View reviewed changes

William Sørensen added 6 commits August 22, 2024 11:28

refactor: lift generation up to elabInductiveView for Shapes

8955cdf

refactor: remove usage of BinderViews

d808100

feat: make relation more general readying for mutuals

0615cb5

feat: mutual co-inductives

fa1545f

fix: imports

b4b2ad3

fix: add trace comment

92ef36f

alexkeizer reviewed Aug 23, 2024

View reviewed changes

fix: add comments

a3a1f53

tobiasgrosser reviewed Aug 23, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add simple co-inductive predicates #17

feat: add simple co-inductive predicates #17

Equilibris commented Aug 21, 2024 •

edited

Loading

tobiasgrosser Aug 22, 2024

tobiasgrosser Aug 22, 2024

alexkeizer commented Aug 23, 2024

alexkeizer left a comment

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

Equilibris Aug 23, 2024

alexkeizer Aug 23, 2024

Equilibris Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

alexkeizer Aug 23, 2024

tobiasgrosser Aug 23, 2024

		we can safely coerce syntax of these categories -/
		instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder) where coe x := ⟨x.raw⟩

		/- derivingClasses : Array Lean.Elab.DerivingClassView -/
		/- computedFields : Array Lean.Elab.Command.ComputedFieldView -/


		namespace CoInductiveView

		def CtorView.ofStx (declName : Name) (modifiers : Modifiers) (ref : Syntax) : CommandElabM CoInductiveView.CtorView := do


		return { ref, modifiers := ctorModifiers, declName := ctorName, binders := binders.getArgs.map (⟨·⟩), type? := type?.map (⟨·⟩) }

		def ofModifiersAndStx (modifiers : Modifiers) (decl : Syntax) : CommandElabM CoInductiveView := do

	structure CoInductiveView.CtorView where
	structure CoinductiveView.CtorView where

		@@ -0,0 +1,253 @@
		/-
		Copyright (c) 2020 Microsoft Corporation. All rights reserved.

feat: add simple co-inductive predicates #17

Are you sure you want to change the base?

feat: add simple co-inductive predicates #17

Conversation

Equilibris commented Aug 21, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexkeizer commented Aug 23, 2024

alexkeizer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Equilibris commented Aug 21, 2024 •

edited

Loading