Consider adding motives to the terms for `if` and `nat-rec`

[jonsterling]

I would like to propose or open for discussion the matter of adding motives to nat-rec, etc. Right now, it is not possible to automatically check membership for terms defined using nat-rec, nor is it possible to synthesize their types. This results in frustratingly requiring the user to intervene and write down a type in their tactic script, somewhere far away from where the nat-rec was defined.

I want to advance the Thought, "It's OK If Hard Things Are Hard, But Easy Things Should Be Easy". A corollary to this Thought is that we should be able to typecheck routine uses of nat-rec that arise from proof-refinement.

One disadvantage of doing this is that term sizes will increase.

[favonia]

I would like to see how this goes. In particular, if #534 is no longer needed, I would strongly support this.

[favonia]

I think nat-rec and int-rec (with recursion, in general) are more problematic than if. I could be wrong.

[jonsterling]

@favonia Can you give a it more detail about why if is not as problematic? I can believe that recursion can make things harder, but the problem I'm trying to solve is "Synthesize the type of this expression"; in general, I think this is just as impossible with if as it is with nat-rec, but I may be missing something.

[favonia]

You can cheat---if m0 is in type ty0 and m1 is in type ty1, then (if b m0 m1) is in type (if b ty0 ty1).

[jonsterling]

@favonia Yes, but that doesn't get us anywhere! We also can't necessarily synthesize m0 and m1. The situation with synth and if is basically the same as with nat-rec for this reason; with elimination forms of positive types, you can never synthesize generally unless you supply a motive. This corresponds to the fact that usually synthesis applies in left focus, whereas the positive eliminators usually are part of inversion.

[favonia]

Did we reach some consensuses? This change is trivial to make, and I wonder if there is any objection.

[jonsterling]

@favonia I think we should do it, in order to "make easy things easy"; but I don't think I ever got a final opinion from Carlo on it. @cangiuli what do you think?

[I have experimentally carried out this change in a branch, and together with some changes to how type synthesis works, it has enabled us to resolve a number of usability issues.]

[cangiuli]

@jonsterling and I discussed the possibility of adding a secret motive when provided by an elim, but I don't remember where that conversation ended.

[jonsterling]

To give a bit more detail, Carlo and I had an idea that one could make the motive for if and nat-rec optional, so that users could write it without a motive if they preferred.

My feeling is that it may not be worthwhile to make it optional; here's why:

1. Difference in term size is likely to be minimal; users won't be writing big motives by hand anyway (I think that big motive will only occur without user intervention, from proof refinement---since who can be bothered to write something gnarly by hand?)

2. Terms with motives are easy to prove things about, and ones without motives are very hard to prove things about. If we make it optional, we open the door for users to get very confused and angry when some proofs are harder for strange reasons.

While the story is different both in the context of semantics and in the context of compilation (something we have not yet considered), I think that in a proof assistant we should aim to make things easy to automate.

ultimately I would like the main differences between redprl and other proof assistants not to be some sad-heroic thing like "They had a few less annotations in their terms, RIP", but rather "They made it possible to do things that were not expressible elsewhere".

[cangiuli]

Given that eliminators for HITs (CITs?) need motives anyway, I think it's reasonable to demand motives everywhere. This would also allow us to unify wif/if fwiw.