partial image of finset? / finset comprehension?

Stream: new members

[Malvin Gattinger]

Could someone help me with this?

import data.set.finite
import data.finset.basic
import data.finset.pimage

@[derive decidable_eq]
inductive formula : Type
| atom : char -> formula
| neg : formula → formula
| and : formula → formula → formula
| box : formula → formula

open formula

-- Do I have to do this manually? I saw Lean 4 has "deriving Repr", but Lean 3 does not?
def formToString : formula → string
| (atom c)  := "atom " ++ repr c
| (neg f)   := "neg " ++ formToString f
| (and f g) := "and (" ++ formToString f ++ ") (" ++ formToString g ++ ")"
| (box f)   := "box ("++ formToString f ++ ")"

instance form_repr : has_repr (formula) := ⟨formToString⟩

def projection : formula → option formula
| (box f) := some f
| _       := none

def uglySetProjection : finset formula → finset formula :=  finset.pimage (part.of_option ∘ projection)

#eval uglySetProjection { neg (atom 'p'), box (box (atom 'q')), box (atom 'q') }

--  Maybe it is better to use a "pfun"?
def pfunProjection : pfun formula formula
| (box f) := some f
| _       := none

-- But now I need something decidable here?
def niceSetProjection : finset formula → finset formula := finset.pimage pfunProjection

-- It would be great if I could say projection X := { f | (box f) ∈ X }
-- but it is impossibe to define finsets using set comprehension?
-- (because then there is no proof that the result is finit?)

[Yaël Dillies]

Indeed, the finset images require decidability, and a general part has undecidable domain. This is the content of the noncomputability of docs#part.equiv_option

[Malvin Gattinger]

Ok. So it is better to use option instead of part (or pfun) in my case? It mostly feels weird to use part.of_option instead of using a part in the first place ;-)

[Yaël Dillies]

I think so, yeah