add singleton_insert_empty

This is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.

I would use =@{M A} instead of the cast.

changed this line in version 2 of the diff

This lemma already exists:

Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}.
Proof. done. Qed.

Oh... but then why didn't it show up when I SearchAbouted Singleton Insert Empty?

Finite map lemmas are just impossible to navigate. It's typeclass spaghetti. :(

It's SingletonM not Singleton. The latter is the set singleton.

Yes that's why I did.

Search SingletonM Insert Empty.

has no result

insert_empty :
∀ (K : Type) (M : Type → Type) (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type,
                                                                      PartialAlter K A (M A)) 
  (A : Type) (i : K) (x : A), <[i:=x]> (∅ : M A) = {[i := x]}

It doesn't depend either on singleton nor on insert...

I'd have to Search Empty PartialAlter. That's kind of ridiculous.^^

(To be clear, I don't know how to design a discoverable TC-based API in Coq. But the status quo is bad.)

Search singletonM empty insert works just fine. Use the class projections, not the classes.

Ah, that's a neat trick. Is it documented?

It's as well-documented as anything, namely not.

added 1 commit

• c19fdeae - add singleton_insert_empty

Compare with previous version

closed