decidability theorems in iset.mm could be a bit better structured

[jkingdon]

Some of the theorems around decidability in iset.mm were introduced by me before I really had a good feel for set.mm/iset.mm conventions or what would be convenient, and have not been revisited. Mostly this is a minor annoyance, or not even much of an annoyance at all, but there is potentially room for some revisions if anyone has the interest in taking a closer look.

There are a number which use exported form when imported form is more typical of what we do elsewhere in iset.mm. For example, https://us.metamath.org/ileuni/dcan.html is

DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓))

but under this theory should be

( DECID 𝜑 ∧ DECID 𝜓 ) → DECID (𝜑 ∧ 𝜓)

There are also a number of theorems involving ≠, for example necon1ddc is

necon1ddc.1	⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)))
necon1ddc	⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)))

but would seem to be more natural as

necon1ddc.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)))
necon1ddc.dc	⊢ (𝜑 → DECID 𝐴 = 𝐵)
necon1ddc	⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))

(compare with https://us.metamath.org/mpeuni/necon1d.html which is what it looked like before decidability was added).

I might take a closer look at this some day but I'm particularly making this issue in case it encourages someone else to get to it first.

[david-a-wheeler]

That makes complete sense to me! I think "refactoring after more experience" is normal and necessary. I have limited time, but I might try my hand at these. I want to do more with Metamath & life keeps interfering :-).

[jkingdon]

That makes complete sense to me! I think "refactoring after more experience" is normal and necessary. I have limited time, but I might try my hand at these. I want to do more with Metamath & life keeps interfering :-).

Should be doable in small pieces. If you do look at one of these (or anyone else does), and aren't sure what to do about it, feel free to ask.

[david-a-wheeler]

I'm thinking this should be dcan:

( DECID 𝜑 ∧ DECID 𝜓 ) → DECID (𝜑 ∧ 𝜓)

Then use that to prove dcan2:

DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓))

As a first step, just rename current uses of dcan -> dcan2. Then do other steps later.

[benjub]

Yes, for closed forms, the uncurried form is indeed the form of choice. It would be nice to add deduction forms, especially when there is more than one hypothesis. In the case of stable formulas, compare https://us.metamath.org/ileuni/bj-stan.html and https://us.metamath.org/ileuni/bj-stand.html.

edit: I've just made a minor related MR (#4386) while looking at nearby theorems. Many propcalc theorems which hold with a decidability hypothesis also hold with a weaker stability hypothesis, see e.g., https://us.metamath.org/ileuni/const.html and https://us.metamath.org/ileuni/bj-pm2.18st.html (whose respective comments link to the decidability version).

[jkingdon]

I'm thinking this should be dcan:

( DECID 𝜑 ∧ DECID 𝜓 ) → DECID (𝜑 ∧ 𝜓)

Then use that to prove dcan2:

DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ 𝜓))

As a first step, just rename current uses of dcan -> dcan2. Then do other steps later.

Sounds like a good way to approach it.

[david-a-wheeler]

First step is here: #4390 - it's a trivial step, but it gets things started. I don't really deserve credit in "Revised by", it just tells people who to blame :-).

[david-a-wheeler]

I just did dcan as I suggested, which is a trivial start. That said, would it be better to created the deduction forms, then derive the others?

[david-a-wheeler]

@benjub makes a good point about deduction form. I plan to merge my first change, then build on it to add deduction form to end up with this:

dcand:

( ph -> ( ( DECID ps ∧ DECID ch ) → DECID ( ps ∧ ch ) ) )

dcan:

( ( DECID 𝜑 ∧ DECID 𝜓 ) → DECID (𝜑 ∧ 𝜓) )

dcan2:

( DECID 𝜑 → ( DECID 𝜓 → DECID (𝜑 ∧ 𝜓 ) ) )

The "dcan2" is there so that we can easily use existing theorems (we can change them later).

I'll also do the same for dcor (dcord, dcor, dcor2). That should make it easier to apply deduction form.

[benjub]

dcand would rather be

dcand.1 $e |- ( ph -> DECID ps ) $.
dcand.2 $e |- ( ph -> DECID ch ) $.
dcand $p |- ( ph -> DECID ( ps /\ ch ) ) $=

see for instance https://us.metamath.org/ileuni/bj-stand.html

You can script, for each theorem xxx currently using dcan2,

PROVE xxx
EXPAND dcan2
MINIMIZE_WITH * /MAY_GROW /EXCEPT dcan2
SAVE NEW_PROOF /COMPACT
EXIT

and then deprecate dcan2.

[david-a-wheeler]

@benjub - you're right, much better. "show usage dcan2" shows the list of theorems that use dcan2, so that is easy to script. That is definitely the new plan.