Add Conat

[ice1000]

Add conat, prove that mugen plus one equals mugen :)

[mortberg]

The code looks fine to me, but is there anything univalent you can do with the co-natural numbers?

[ice1000]

I can't think of any. Maybe proving bisimulation on conat is equivalent to path?
I'll have a try.

Happy Chinese new year!

[mortberg]

That sounds like a good idea! Maybe you can construct some non-trivial equivalence on conat as well? Or to some other type. You can then transport some things back and forth just to check that transp works for coinductives

[mortberg]

Xīnnián kuàilè! (I hope Google translate got that right)

[ice1000]

Yes the pronunciation is correct!

I'm truggling with the definition of plus. TBH, I don't like Sized Types. I'm trying to get rid of it (while the Conat in the stdlib is completely based on Sized Types)

[martinescardo]

A univalent thing you can do is to show that conat is equivalent and hence equal to the type of decreasing binary sequences, which is how I define conat here:

http://www.cs.bham.ac.uk/~mhe/agda-new/CoNaturals.html
http://www.cs.bham.ac.uk/~mhe/agda-new/CoNaturalsExercise.html

[ice1000]

I've just found that bisimulation on a sum type is quite hard to define since some definitional equalities are lost due to guarded recursion. I'll take a look at @martinescardo@'s code.

[ice1000]

@martinescardo@ it's a beautiful one, but the definition of CoNatural is using a different encoding from mine. I noticed that you have a PREV and SUCC which are structure-preserving, while for my Conat there isn't such (or maybe I don't know, probably) pred.

I'm still not able to define a better bisim because Agda does not support with in a path-pattern (with clauses not supported in the presence of Path patterns).

[martinescardo]

When I did this in 2010-2011 (then extended in 2012 with coinduction), I was not satisfied with Agda's native treatment of coinduction/corecursion, and this is why I implemented conat without Agda's coinduction features. Also, the way I am using to encode conat comes from traditional constructive mathematics. However, it would be nice to do everything I did with native support for coinduction/corecursion. Perhaps you can suggest an idiom to expresses what you need as a feature request. But I believe it should be possible, without additional support, to show that my conat is equivalent (and hence equal) to your conat, no?

[ice1000]

What I've found missing in Agda is the support for with abstraction and path-patterns (cc agda/agda#2461)

[martinescardo]

Can you be more precise in what you would like to be able to write, with a concrete example involving conat?

[ice1000]

You can see my unfinished proof in https://github.com/Agda-zh/cubical/tree/conat-bisi

[martinescardo]

Thanks. But your link is broken.

[ice1000]

Complete explanation

A little prelude to this comment, just plain coproduct and product:

open import Agda.Builtin.Sigma
_×_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ-max ℓ ℓ')
A × B = Σ A (λ _ → B)

data _⊎_ {ℓ ℓ'} (P : Set ℓ) (Q : Set ℓ') : Set (ℓ-max ℓ ℓ') where
  inl : P → P ⊎ Q
  inr : Q → P ⊎ Q

I have a conat which is a coinductive wrapper on a A → Unit ⊎ A instead of an inductive wrapper on a Thunk (to avoid using Sized Types):

record Conat : Set
Prev = Unit ⊎ Conat
record Conat where
  coinductive
  constructor conat
  field prev : Prev

pattern zero  = inl tt
pattern suc n = inr n

succ : Conat → Conat
prev (succ a) = inr a

I'm trying to define a bisimulation relation on it, so I came up with this definition:

module Bisimulation where
 data _≠0 : (a : Prev) → Set where
    no0 : ∀ {a} → suc a ≠0

  pred : Prev → Conat
  prev (pred  zero  ) = zero
  prev (pred (suc x)) = prev x

  -- Maybe this definition is not good enough?
  record _~_ (a b : Conat) : Set where
    coinductive
    constructor intro
    field proof : (a ≡ b) ⊎ ((pred (prev a) ~ pred (prev b)) × (prev a ≠0 × prev b ≠0))
  open _~_

With with abstraction and copatterns, I can easily define an identity function:

  identity : ∀ n → n ~ n
  proof (identity n) with prev n
  ... | zero  = inl refl
  ... | suc x = inr (identity (pred (suc x)) , no0 , no0)

And I failed to define a bisim with a signature like this:

bisim : ∀ {a b} → a ~ b → a ≡ b

Because with abstraction cannot be used with path patterns, I can't use a seem-to-better definition like the one in identity:

  -- Fake code, rejected because copattern is not supported in path patterns
  proof (bisim {a} {b} p i) with proof p

I tried to use with abstraction without path types (and of course, without copatterns), and I come up with a code like this (have to pattern match on prev a and prev b to indicate that they are not zero):

 bisim {a} {b} p with prev a | prev b | proof p
  ... | _     | _     | inl x = x
  ... | suc x | suc y | suc (bi , no0 , no0) = cong {!succ !} (bisim bi)

Agda rejects the hole because succ (pred (suc x)) != a.

Since suc x is equal to prev a definitionally, we can use Agda's inspect idiom, which becomes the code you see in the unfinished branch. However, Agda no longer knows that proof p's second member is no0 , no0 because all suc xs becomes prev as so the information that "a is never 0" is lost (which causes incomplete pattern error).

I tried a little to use the eq-reasoning style proving, as in the unfinished branch, and it causes termination error.

I have no idea about how to prove this. I hope I'm making stupid mistake here.

[ice1000]

I have no problem viewing that. Is it private? I don't think it's private:

[martinescardo]

Ah, it is here: https://github.com/Agda-zh/cubical/blob/conat-bisi/Cubical/Codata/Conat/Properties.agda

[Saizan]

@ice1000 Here's a way to do bisimulation for Conat 31f7de1

You can pull that commit into your branch if you like it, so we can stay on this PR. (or is there a better way?)

I defined _~′_ by recursion to avoid inductive families since they are not supported by cubical yet, otherwise an inductive definition would be better style.

Also, IMO Conat′ should be its own datatype with zero and suc constructors, as that works better for case splitting and overloading.

[ice1000]

I feel like what you're doing is manually lifting the with auxiliary function and it sounds like a good idea!

I like the new style mutual recursion so I'll refactor your code a little bit and do the rest of the work.

[ice1000]

Also, IMO Conat′ should be its own datatype with zero and suc constructors, as that works better for case splitting and overloading.

This is very opinion-based and actually I was using a standalone datatype and then switched to a sigma type. I'm gonna keep this anyway.

[potato4444]

It is a fairly simple corollary of the fact the conat is a set and the equivalence between bisimilution and identity, but do we want an explicit proof of bisumlation being a proposition?

[ice1000]

It is a fairly simple corollary of the fact the conat is a set and the equivalence between bisimilution and identity, but do we want an explicit proof of bisumlation being a proposition?

I don't think it's possible to extract a general definition of bisimulation as a proposition, see our discussion above (we've come up with more than three definitions, each of them sounds amazingly reasonable but they all fail due to some mysteries until Mr. @gallais@'s final version based on isSet).

[ice1000]

IIUC defining bisimulation on a coinductive structure requires you to "look into" the structure, which means you'll need to define a specific bisimulation for every coinductive structures.

If you have any idea about defining such general bisimulation proposition (except creating the definition by reflection) please explain.

[gallais]

I think @potato4444 means that bisimulation satisfies isProp.

[ice1000]

Proved that bisimulation is a prop.

[ice1000]

Please take a look @mortberg@

[ice1000]

Addressed all comments.

[mortberg]

It seems like you forgot to include Cubical.Foundations.Path

[ice1000]

Added the file.

[mortberg]

Thanks, I'm fine with merging as soon as Travis is happy

[mortberg]

Thanks to everyone who contributed to this PR!

[ice1000]

CI is very happy now.

[mortberg]

@Saizan Can you merge if you have no more comments?