Zulip Chat Archive

Stream: new members

Topic: type of nonempty finset?


view this post on Zulip Vaibhav Karve (Jul 14 2020 at 18:48):

Given a type A, how do I represent the type of all nonempty finsets of A. Is it inhabited (finset A) or nonempty (finset A) or something completely different?

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:51):

(deleted)

view this post on Zulip Kenny Lau (Jul 14 2020 at 18:55):

{ s : finset A // s ≠ ∅ }

view this post on Zulip Kyle Miller (Jul 14 2020 at 18:56):

@Jalex Stark If you want nonempty, maybe {s : finset A // nonempty (↑s : set A)}. I think I like Kenny's more, though.

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:56):

s.nonempty avoids all that coercion

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:56):

but yes, i also like the version with \ne

view this post on Zulip Kyle Miller (Jul 14 2020 at 18:57):

Oh, didn't know about that. {s : finset A // s.nonempty}

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:58):

s.nonempty is approximately equal to finset.nonempty s

view this post on Zulip Kyle Miller (Jul 14 2020 at 18:59):

I wonder if the s.nonempty version might be better in practice because you get a witness, and you don't have to rewrite with nonempty_iff_ne_empty.

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:59):

you also see things like n.succ for nat.succ n sometimes, though I think many people find the latter form preferable

view this post on Zulip Kyle Miller (Jul 14 2020 at 18:59):

Sorry, I just meant I didn't know about finset.nonempty.

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 19:11):

@Kenny Lau that works perfectly. Thanks!

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 19:58):

I have a new problem now:

constant A : Type
constant myset : {x : finset A // x.nonempty}
constant a : A
#check a  myset

This final check gives me the error

failed to synthesize type class instance for
 has_mem A {x // x.nonempty}

How do I create this instance has_mem? I think I somehow need to derive it using finset.has_mem?

view this post on Zulip Kyle Miller (Jul 14 2020 at 20:30):

The subtype doesn't inherit any of the instances from finset, and I think you have to manually derive all the ones you want yourself (as far as I know). One thing you can do without doing that is write a ∈ myset.val instead.

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 20:33):

Phew. I will do that. I definitely don't want to derive these instances by hand if I can avoid it.

view this post on Zulip Kyle Miller (Jul 14 2020 at 20:34):

Remember that the { ... // ... } notation is shorthand for this type:

structure subtype {α : Sort u} (p : α  Prop) :=
(val : α) (property : p val)

It bundles together a value with the property the value satisfies. Depending on what you're doing, it might be easier to make all your functions/lemmas take two arguments: (x : finset A) (h : x.nonempty)

view this post on Zulip Patrick Massot (Jul 14 2020 at 20:34):

What are you actually trying to do?

view this post on Zulip Patrick Massot (Jul 14 2020 at 20:34):

All those constant are not in your real code, right?

view this post on Zulip Reid Barton (Jul 14 2020 at 20:36):

Why not just write the instances you want by hand?

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 20:42):

There's only \in and maybe \subset, right?

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 20:50):

Patrick Massot said:

All those constant are not in your real code, right?

Right. This was just for the sake of the MWE.

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 20:54):

Slightly larger MWE to show what I am doing:

/-Define CNFs in Lean-/

import data.bool data.finset
import tactic


variables (V : Type) [decidable_eq V]


/-Literals of V are either positive V, negative V, or booleans.-/
@[derive decidable_eq]
inductive Lit
| pos : V  Lit
| neg : V  Lit
| bool : bool  Lit

def neg : Lit V  Lit V
| (Lit.pos v) := Lit.neg v
| (Lit.neg v) := Lit.pos v
| (Lit.bool tt) := Lit.bool ff
| (Lit.bool ff) := Lit.bool tt

/-A Clause is a non-empty, finite set of Literals of V.-/
structure Clause : Type :=
(lits : {c : finset (Lit V) // c.nonempty})

/-A Cnf is a non-empty, finite set of Clauses of V.-/
structure Cnf : Type :=
(clauses : {x : finset (Clause V) // x.nonempty})

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 20:56):

Another thing I am unsure about is if I should make defs instead of structures.

def Clause : Type := {c : finset (Lit V) // c.nonempty}

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 20:57):

Cnf stands for conjunctive normal form

view this post on Zulip Kyle Miller (Jul 14 2020 at 20:57):

Does a CNF actually need to be nonempty?

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:00):

There's also the consideration of using lists instead of finsets. A finset is a list with no duplicates modulo permutations, but a specific CNF might be an actual expression in a specific order. You could have lemmas that say you can reorder things while preserving satisfiability.

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:01):

I forgot to mention that you might not need the no duplicates assumption. You could have additional lemmas that let you deduplicate literals or clauses in the CNF.

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:05):

(Just for completeness: you could interpret an empty clause as being false, and an empty CNF as being true. If I remember correctly, these sorts of things can naturally occur over the course of SAT solving.)

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 21:21):

@Kyle Miller
I agree with everything you have said. However, I am trying to build towards to type of all "reduced" CNFs i.e. CNFs that have been reduced under the following tautologies:

  • a ∨ a = a
  • a ∧ a = a
  • a ∨ ¬ a = ⊤
  • a ∧ ¬ a = ⊥
    If I implement them as lists instead of finsets then I will have to define these recursive maps simplification maps, right? And then I'll have to prove that once all the tautology-rewriting is done then the resultant has no duplicates. And then I will finally be able to create a reduced CNF type. Hence I thought I will use finsets to enforce tautologies 1 and 2 from the very beginning.

view this post on Zulip Reid Barton (Jul 14 2020 at 21:40):

Don't you need to allow the empty lists to represent the true clause / false formula, then?

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:40):

@Vaibhav Karve Take what I'm saying with a grain of salt because I haven't done enough Lean, but I would probably go through the following:

  • Define the unreduced version of a CNF
  • Define what it means for a clause to be reduced (see list.nodup)
  • Define what it means for a CNF to be reduced
  • Define a subtype of reduced CNFs
  • Define a function reduce that reduces a CNF (and prove reduce results in a reduced CNF)
  • Define a satisfying assignment and the set of satisfying assignments for a CNF
  • Show that the set of satisfying assignments is unchanged after reduce. Then you'll have some confidence the definitions are good.

A complication with finset is that it is a quotient. If you use finset instead of list, then you are going to have to deal with expressions being defined only up to permutation all the time. If you really want this property, that two CNFs are equal even after permuting clauses and variables, then you might instead define an equivalence relation on CNFs (a setoid instance) and take the quotient, after the above work.

view this post on Zulip Vaibhav Karve (Jul 14 2020 at 21:59):

Thank you so much for that detailed outline. I am going to follow the list path.


Last updated: May 08 2021 at 04:14 UTC