Finite sets two ways. #104

dolio · 2019-03-24T21:28:05Z

This implements two sorts of finite sets.

The first is Fin k in the Data hierarchy. This implements finite sets using a pair of a natural and a proof that it is less than k.

The second is Modulo k in the HITs hierarchy, which has a base constructor including arbitrary naturals, with added paths between the image of n and k + n. This differs from Fin in the case where k = 0, as Modulo 0 is isomorphic to ℕ (an extra truncation constructor is added for this).

A function for reducing naturals to their residue mod suc k is provided, and this is used to define a function for turning Modulo (suc k) into Fin (suc k).

Some properties about the naturals that were needed were also added, and a module for embeddings is included, because I was originally planning to use that for the reduction functions (but ended up not doing so).

- An embedding is the higher equivalent to an injective map. Injective maps between sets are embeddings.

- Finite sets are represented as naturals less than the index. - A procedure is defined to reduce naturals to their finite residue modulo a successor natural.

- They are defined by having an inclusion from the naturals, and adding paths between inclusions from n and k+n. - In the case of k=0, the type is equivalent to the naturals. - Mapping back to finite sets TBD.

- Rearranged the proof that the Fin reduction fibers are equivalent - Moved some Modulo stuff to a Properties module - Added an aggregate Modulo module - Added Fin and Modulo to Everything modules

dolio · 2019-03-24T21:35:16Z

I should note, the function that extracts from Modulo (suc k) is pretty slow to type check, and I'm not sure why. Toward the end of this I was bumping more into areas where cubical agda seemed to blow up in that regard. The step case of mreduce seems to be the slow part, but also, at some point when I did a split for that function, the squash case seemed to get stuck permanently, although it works all right when the absurd match is added, or the line is deleted.

Anyhow, if you want maybe Modulo should be removed from the Everything module to avoid the long checking for the time being.

riaqn · 2019-03-25T02:59:27Z

Cubical/Data/Fin/Base.agda

+open import Cubical.Relation.Nullary
+
+Fin : ℕ → Set
+Fin n = Σ[ k ∈ ℕ ] k < n


Is there some particular reason you are using this definition? There is the other inductive family definition that I usually find behaves better.

Namely this definition:

data Fin : (n : N) -> Set where zero : (n : N) -> Fin (suc n) suc : (n : N) -> Fin n -> Fin (suc n)

@riaqn that definition is an inductive family, which Agda doesn't support fully in cubical mode yet. For a different definition of Fin that would work you could define it recursively as a coproduct of unit types. I don't know the trade offs between that definition and the definition used here though.

@potato4444 Hmm, I didn't know that. The definition itself passes the type check. Do you have some example results of this Fin that couldn't be accomplished in the current cubical agda?

@riaqn this is what doesn't work #57 (comment)

@riaqn that definition is an inductive family, which Agda doesn't support fully in cubical mode yet. For a different definition of Fin that would work you could define it recursively as a coproduct of unit types. I don't know the trade offs between that definition and the definition used here though.

But I assume this issue should only be temporary? If I understand it correctly, it only needs the computation rule for the least fixpoint, since an inductive family is the initial algebra for a dependent polynomial functor/indexed container.

For instance, a while ago I was playing around with the usual Fin definition, and cubical agda wouldn't infer the value of implicit arguments k from explicit Fin k arguments.

@dolio That's weird, if it happens again please report it. It could just be that the unification constraint wasn't in the pattern fragment (maybe because it only held for some (i = i0)), but otherwise type constructors should behave the same wrt type inference.

@L-TChen The problem is constructors that specialize the index argument of their result type, they need special care for transp.

As @Saizan and others said already: inductive families are currently not supported by Cubical Agda in the sense that transp does not reduce correctly (or at all?) for them. There is no deep theoretical reason for this; it's "only" a matter of extending the internal definition of transp in Agda following http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf. This change will require us to add "formal" transp values (just like hcomp is a constructor/value for HITs), for details see the special case of Id types in section 3.3 of the linked paper (note that transp is called coe as they are working in Cartesian cubical type theory, however the same idea works for De Morgan cubical type theory with transp/hcomp).

@mortberg Shall we open the support of inductive families as an issue?

Oh, don't worry, I'm aware we need them

Cubical/Foundations/Embedding.agda

mortberg · 2019-03-27T03:30:05Z

Cubical/Foundations/Embedding.agda

+isEmbedding : (A → B) → Set _
+isEmbedding f = ∀ w x → isEquiv {A = w ≡ x} (cong f)
+
+injEmbedding


Hmm, maybe I'm wrong. But doesn't the hypotheses imply that A is a retract of B ? If that's the case then you don't need isSet A as any retract of a set is a set.

Ah, okay. I'll try and generalize. I think the HoTT book said it was true "for sets" which was kind of ambiguous.

I see, I might very well be wrong as I didn't try to prove it myself! Don't spend too much time on it if you get stuck.

I tried to do this, but it seemed impossible. Whichever isSet hypothesis I removed seemed to be the one I ended up needing to pull back the other isSet. So this might not actually be possible.

Ok, good to know!

Maybe add a comment saying that the isSet assumptions seem necessary with a pointer to where this is defined in the HoTT book?

Cubical/Foundations/Embedding.agda

mortberg

I intended to include all of my comments in a review, but I forgot to start it.... Anyway, thanks for the contribution!

I find the Modulo definition quite complicated compared to Fin... Does it offer any benefits over Fin?

mortberg · 2019-03-27T03:34:49Z

Cubical/HITs/Modulo/Properties.agda

+
+mreduce : (m : Modulo (suc k)) → MReduction k m
+mreduce (embed n) = reduce _ n
+mreduce {k} (step n i) = reduce≡ k n (suc k + n) refl i


Can you prove that Fin k is equivalent to Modulo k ?

I guess I didn't get as far as I wanted with just this, because the reduction function started consuming all my effort (and then I forgot about the other stuff). However, there are some interesting differences between Fin and Modulo.

Fin 0 is empty and Modulo 0 is the natural numbers

It's easy to have a successor function Fin k -> Fin (suc k), and harder to have one typed Fin k -> Fin k. However, the case is the opposite for Modulo.

I think this probably generalizes somewhat, and it's easy to write arithmetic internal to Modulo k, and the difficulty related to writing it in Fin k is the reduction function (although I suppose I've factored that out in this).

I can add that Fin (suc k) is equivalent to Modulo (suc k).

Oh also, I think Modulo is just kind of a cool example of how you can do stuff with higher inductive types + univalence similar to the homotopy patch theory paper, but perhaps simpler.

This is interesting! Maybe you could include some of this comment in the top of the Modulo file to explain why it's a nice alternative to Fin? I'm very interested in programming examples that get simpler with univalence and HITs.

And yes, please prove that the two types are equivalent. That would be nice to have as well as we can transport results between the two representations. I wonder if there is anything that is really painful with Fin that gets a lot simpler with Modulo....

Modulo (suc k) and Fin (suc k) have been shown equivalent.

By the way, I don't know if I mentioned this elsewhere, but I changed the definition of Modulo along the way. Instead of trying to truncate the 0 case, I avoid adding paths to it. This made things rather simpler, and a pattern synonym made it so that the successor cases weren't really any different.

- This is a wrapper for well-founded induction according to <, but is somewhat more convenient for the modular stuff. - Finite set reduction will be re-implemented in terms of this simpler induction principle.

Alizter · 2019-04-09T23:44:21Z

Travis isn't happy, subTypeEquality isn't in scope?

Alizter · 2019-04-09T23:58:30Z

Cubical/Data/Nat/Order.agda

+      = case dichotomy b n return (λ d → d ≡ inr (m , p)) of λ
+      { (inl n<b) → ⊥-elim (<-asym n<b (m , +-comm m b ∙ sym p))
+      ; (inr (m' , q))
+      → cong inr (subtypeEquality


I think this is where travis is tripping up

Has subtypeEquality moved or been renamed?

Oh, it has. Now it's ΣProp≡.

- Re-implemented reduction in terms of +induction

- Modified the definition. Instead of adding k+ paths for all k, and squashing to a set for k=0, avoid adding the paths for 0. This simplifies a fair amount of stuff.

mortberg · 2019-04-10T13:21:36Z

It looks like this PR is soon ready to be merged?

Can you please add some headers to the files explaining their content. I would be good with a comment about what the pros and cons are with the different definitions so that someone who needs finite sets find the best definition for them (with pointers to the other file in each of the files)

mortberg · 2019-04-11T16:24:29Z

I'm going to merge #131 now. Let me know if you need some help resolving conflicts in this PR

dolio · 2019-04-12T00:21:48Z

I think I'll be all right. And I'll write up some actual comments this weekend probably.

- Seems like a better name.

- Add a type for embeddings in terms of propositional fibers - Show that the two types of embedding are equivalent

dolio

Never mind. I finished up proving this. But I had to add the f arguments you see, because Agda gets confused about the metas without them for some reason. Seems like it's probably a bug.

dolio · 2019-04-14T00:21:39Z

Cubical/Foundations/Embedding.agda

+
+private
+  lemma₂
+    : (p : f w ≡ f x)


So, the latest (or close) Agda stopped being able to solve a meta on this line. I think the w is yellow (I reverted to a version that doesn't have the problem, so I'm not 100% sure). Is there some reason for this, or is it just a bug?

I could just delete this right now, but I think I thought it was a step toward showing that isProp (fiber f y) is equivalent to isEmbedding f.

The unsolved meta is the reason the CI is failing on this pull request.

It seems to me like the CI is working? I restarted it just to be sure.

It's all good.

Alizter

LGTM Great stuff!

Alizter · 2019-04-15T09:15:37Z

Let's merge this before #132 and then make necessary adjustments in that pr.

mortberg · 2019-04-15T14:18:28Z

I'm merging this now so that I can merge the other PR. If you want to add more comments or add content please do it in a new PR. Thanks a lot for contributing!

dolio added 5 commits March 24, 2019 10:57

More ℕ properties.

578c599

Add embeddings with some properties.

2016054

- An embedding is the higher equivalent to an injective map. Injective maps between sets are embeddings.

Add finite sets as data.

cb9892a

- Finite sets are represented as naturals less than the index. - A procedure is defined to reduce naturals to their finite residue modulo a successor natural.

Start on a HIT analogue to finite sets, Modulo

c57c8bf

- They are defined by having an inclusion from the naturals, and adding paths between inclusions from n and k+n. - In the case of k=0, the type is equivalent to the naturals. - Mapping back to finite sets TBD.

Finish implementing extraction from Modulo to Fin

a49d63e

- Rearranged the proof that the Fin reduction fibers are equivalent - Moved some Modulo stuff to a Properties module - Added an aggregate Modulo module - Added Fin and Modulo to Everything modules

riaqn reviewed Mar 25, 2019

View reviewed changes

mortberg reviewed Mar 27, 2019

View reviewed changes

Cubical/Foundations/Embedding.agda Show resolved Hide resolved

mortberg reviewed Mar 27, 2019

View reviewed changes

Cubical/Foundations/Embedding.agda Show resolved Hide resolved

mortberg requested changes Mar 27, 2019

View reviewed changes

dolio added 3 commits March 28, 2019 20:08

Prove that isEmbedding is a proposition

c375ae3

Add a couple simple ≤ properties.

9ae58fd

Create a function for induction via b +

6ee777b

- This is a wrapper for well-founded induction according to <, but is somewhat more convenient for the modular stuff. - Finite set reduction will be re-implemented in terms of this simpler induction principle.

Alizter reviewed Apr 9, 2019

View reviewed changes

dolio added 3 commits April 9, 2019 20:59

Various Fin property additions

3cb81c4

- Re-implemented reduction in terms of +induction

Modulo improvements

3851567

- Modified the definition. Instead of adding k+ paths for all k, and squashing to a set for k=0, avoid adding the paths for 0. This simplifies a fair amount of stuff.

Modulo ≡ Fin and isSet (Modulo k)

695d0ba

dolio added 5 commits April 13, 2019 11:13

Merge changes from master and fix incompatibilities.

b28c07b

residue seems like a more appropriate name than modulus

8e8e96c

Documentation of Embedding, Fin and Modulo

6ee0625

Reduction→Residue in Fin properties.

bbd68f8

- Seems like a better name.

Embedding tweaks.

f7702d5

- Add a type for embeddings in terms of propositional fibers - Show that the two types of embedding are equivalent

dolio commented Apr 14, 2019

View reviewed changes

Alizter approved these changes Apr 14, 2019

View reviewed changes

mortberg approved these changes Apr 14, 2019

View reviewed changes

mortberg merged commit 0249030 into agda:master Apr 15, 2019

Alizter mentioned this pull request Apr 15, 2019

Rename Set to Type #132

Merged

Finite sets two ways. #104

Finite sets two ways. #104

Conversation

dolio commented Mar 24, 2019

dolio commented Mar 24, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

potato4444 Mar 25, 2019 • edited Loading

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

mortberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dolio Mar 27, 2019 • edited Loading

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

Alizter commented Apr 9, 2019

Choose a reason for hiding this comment

dolio Apr 10, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mortberg commented Apr 10, 2019

mortberg commented Apr 11, 2019

dolio commented Apr 12, 2019

dolio 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

Alizter left a comment

Choose a reason for hiding this comment

Alizter commented Apr 15, 2019

mortberg commented Apr 15, 2019

potato4444 Mar 25, 2019 •

edited

Loading

dolio Mar 27, 2019 •

edited

Loading

dolio Apr 10, 2019 •

edited

Loading