# Improve iCombine to derive validity properties of ghost state automatically

It would be great if `iCombine`

was also able to derive and provide validity properties of ghost state or mapsto connectives automatically. Currently, you have to search and apply such properties manually. This could be fixed if `iCombine`

takes an extra (optional) `gives`

clause, which provides extra persistent facts (if those exist).

For example, consider the following environment:

```
"H1" : l ↦{#q1} v1
"H2" : l ↦{#q2} v2
```

executing `iCombine "H1 H2" as "H" gives %[Hq Hv]`

should replace `"H1"`

and `"H2"`

with `"H": l ↦{#(q1 + q2)} v1`

and introduces two new pure hypotheses `Hq : q1 + q2 ≤ 1`

and `Hv : v1 = v2`

.

The roadmap for implementing this would be split into two merge requests:

- Change
`FromSep`

to only be used for`iSplit{L,R}`

, change`iCombine`

to rely on two new typeclasses`CombineSepAs`

and`CombineSepGives`

.

These would be defined as`CombineSepAs P1 P2 P := P1 ∗ P2 ⊢ P`

where`P1 P2`

are input,`P`

output

and`CombineSepGives P1 P2 := P1 ∗ P2 ⊢ <pers> R`

where`P1 P2`

are input,`R`

output.

This MR would provide some instances for stuff in`base_logic.lib`

,`mapsto`

.

The new syntax would be`iCombine "Hs" [as "H"] [gives "P"]`

, where either the`as`

clause or the`gives`

clause must be present.- If
`as "H"`

is present, all hypotheses`"Hs"`

will be replaced by`"H"`

, which can be an introduction pattern.

If not present, all`"Hs"`

are kept as is - If
`gives "P"`

is present, additionally learn persistent fact`"P"`

, which can be an introduction pattern. Also supports`%?`

introduction if this fact is pure. - If more than two hypotheses are provided in
`"Hs"`

, repeatedly run`CombineSep`

with the accumulated results - There will be an additional boolean indicating whether
`CombineSepAs`

used the default instance.

- If
- Give general instance for
`own`

(= MR !771 (closed), addresses #251)

This is a summary of a discussion by @jung, @robbertkrebbers, @snyke7 and @gmalecha at the Iris Workshop. Let me know if I forgot something.