Mutual Fixpoints (Beginner Contributor Questions)

Stream: iris-lean

[Pranav S]

Hi!

First post here, apologies if this is the wrong location for this. I saw this issue on mutual fixpoints was tagged as beginner friendly, and figured it would be a good way to get my feet wet/learn a little about the ecosystem.

I've been using the rocq OFE page as a roadmap to port the FixpointAB section, but was running into some issues such that I would ask here. I'm also flying a little in the dark as I don't fully understand the underlying COFE theory and am just symbol-pushing, so please bear with me if the question doesn't fully type check.

I'm trying to port

Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
  Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
  Proof.
    intros n x x' Hx; rewrite /fixpoint_AB.
    apply fixpoint_ne⇒ y. by f_contractive.
  Qed.

and am using the OFE.ContractiveHom.fixpoint to do so. As such, I can apply OFE.ContractiveHom.fixpoint_ne.ne to unroll outside the fixpoint definition, but I'm now on the hook to show that 2 ContractiveHoms are n equivalent.

⊢ { f := fB y1, ne := ⋯, contractive := ⋯ } ≡{n}≡ { f := fB y2, ne := ⋯, contractive := ⋯ }

From my understanding, there don't seem to be rewrite rules about n equivalence that would allow me to convert this goal to a pointwise n-equivalence check on the application of the function on all points (I'm not fully sure this is even the correct definition of n equivalence for functions).

The Rocq version seems to use this f_contractive tactic for this -- is that what I should focus on porting to get this working?

Thanks!

[Zongyuan Liu]

Hi, this issue is probably not very friendly if you are not familiar with the theory. For your question, I don't think you need to port the tactic for this. The Rocq lemma can also be proven as the following

  Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
  Proof.
    intros n x x' Hx; rewrite /fixpoint_AB.
    apply fixpoint_ne=> y.
    apply fB_contractive.
    - exact Hx.
    - reflexivity.
  Qed.

The key is to apply fB_contractive.

[Pranav S]

Noted, thanks for the response -- I'll try tinkering a bit more before giving up and trying something else:

Was able to get it working in Lean for this instance, however, thank you for your help!

[Markus de Medeiros]

It's totally fine to ask! If you have a draft PR somewhere it also makes it easier to answer technical questions about your implementation like this one.

[Pranav S]

I was able to get through the rest of the proofs in the ROCQ implementation, though I skipped the Proper proofs as those were also not implemented for regular fixpoints. I've opened a PR and am happy to tweak naming or condense things. Please bear with me for any beginner mistakes, and thanks for the help :)

[Pranav S]

Also, for my own edification, circling back to the above question I had:

⊢ { f := fB y1, ne := ⋯, contractive := ⋯ } ≡{n}≡ { f := fB y2, ne := ⋯, contractive := ⋯ }

When dealing with this proof obligation, what I was having trouble with was converting this from a fact about Dist between contractive functions to Dist between the underlying types via extensionality, and I incorrectly assumed that the f_contractive tactic was somehow doing this. What I missed was that I could convert this goal to a pointwise goal by simply performing intro y. However, I cannot figure out how intro knows how to do this. There doesn't seem to be an extentionality tactic attached to any of the relevant types, so I am a tad confused. nvm found it: Dist n f g := ∀ x, f x ≡{n}≡ g x for the function instance.

[Markus de Medeiros]

Awesome thanks for contributing! I'll take a closer look and do a cleanup pass sometime but this looks good. Just re. your comment since it's been asked by a few people already: Proper ((≡) ==> (≡)) in Rocq is a corollary of NonExpansive (this follows from the equiv_dist) field of OFE. Rocq adds this in as an explicit typeclass instance to make use of generalized rewriting, but we don't have/use that, so we don't port them if we have NonExpansive or Contractive proven.

[Markus de Medeiros]

Would you be interested in porting more OFE stuff?

[Pranav S]

Thanks! I just realized that the fixpointA_ne and fixpointB_ne can probably be rephrased in terms of NonExpansive₂, so will push that change to the PR as well if I can get it working.

I'd be happy to port some more stuff here as well! Are there other sections that should be moved over?

[Markus de Medeiros]

Yeah there are a couple things left to port in OFE.v! You could do the OFE for sigma types, or look through the CMRA's that for ones missing OFunctors and port those.

[Markus de Medeiros]

These should hopefully be around the same level of difficulty but do ask if there's anything confusing

[Pranav S]

Sounds good, i'll take a look!