type of nonempty finset?

Stream: new members

[Vaibhav Karve]

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?

[Jalex Stark]

(deleted)

[Kenny Lau]

{ s : finset A // s ≠ ∅ }

[Kyle Miller]

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

[Jalex Stark]

s.nonempty avoids all that coercion

[Jalex Stark]

but yes, i also like the version with \ne

[Kyle Miller]

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

[Jalex Stark]

s.nonempty is approximately equal to finset.nonempty s

[Kyle Miller]

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.

[Jalex Stark]

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

[Kyle Miller]

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

[Vaibhav Karve]

@Kenny Lau that works perfectly. Thanks!

[Vaibhav Karve]

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?

[Kyle Miller]

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.

[Vaibhav Karve]

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

[Kyle Miller]

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)

[Patrick Massot]

What are you actually trying to do?

[Patrick Massot]

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

[Reid Barton]

Why not just write the instances you want by hand?

[Kevin Buzzard]

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

[Vaibhav Karve]

Patrick Massot said:

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

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

[Vaibhav Karve]

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})

[Vaibhav Karve]

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

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

[Vaibhav Karve]

Cnf stands for conjunctive normal form

[Kyle Miller]

Does a CNF actually need to be nonempty?

[Kyle Miller]

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.

[Kyle Miller]

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.

[Kyle Miller]

(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.)

[Vaibhav Karve]

@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.

[Reid Barton]

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

[Kyle Miller]

@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.

[Vaibhav Karve]

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