Strings

[dselsam]

Even though strings are only used for meta-programming, the misalignment is unpleasant since e.g. every auto_param prints as an enormous term of unreadable string.str applications. There are four issues here:

• fin vs Fin (def vs structure)
• unsigned vs UInt32 (def vs structure)
• is_valid_char vs isValidChar (Nat.le issue as in https://github.com/dselsam/mathport/issues/15)
• bits vs ofNat (number mismatch as in https://github.com/dselsam/mathport/issues/17)

The last two issues need to be solved independently. The first two seem to only be required for aligning strings.

Note: lean3 used to make fin a structure but changed it to a def so that the subtype API could be used: https://github.com/leanprover-community/lean/issues/359

I see a few options:

• don't align strings
• backport Fin
• backport a fin4 that is only used for characters, and align this
• try to auto-port char -> Char anyway and discard whatever downstream declarations fail
• forward-port Fin as def

I suggest backporting fin4 (just for char) as a default, assuming Leo wants to keep Fin a structure.

[leodemoura]

What about erasing auto_param? That is, the porting tools rewrites auto_param a t ==> a.

[dselsam]

I agree that would be better than not aligning and keeping the unreadable junk. I think the auto-param is useful information though, and figured mathlib might reimplement it and want the old annotations. We could also only auto-port the string literals used in auto-param and discard whatever breaks because of that change, which is probably nothing besides the auto_param equations themselves.

[dselsam]

I added special support for replacing auto_param calls with autoParam calls inside mathport. I think every auto_param in mathlib uses obviously, and so for now I just hard-coded syntax for Mathlib.obviously in the new autoParam terms rather than parse the names.

[digama0]

There are more than just obviously. Here's what I found (this should be an exhaustive list):

• obviously, obviously
• order_laws_tac
• try_refl_tac
• tactic.apply_instance
• tactic.interactive.refl
• unique_diff_within_at_Ici_Iic_univ
• volume_tac
• is_bounded_default
• tactic.exact_dec_trivial
• tactic.derive_reassoc_proof
• sampleable.mk_trivial_interp
• mk_decorations
• tactic.interactive.continuity'
• skip

[dselsam]

Whoops, I had a buggy grep query. Good catch, thanks. I guess I will decode the names during mathport.

[dselsam]

Now we decode the concrete strings from auto_param arguments: https://github.com/dselsam/mathport/blob/master/MathPort/Translate.lean#L63