Syntax triage

Stream: mathlib4

[Mario Carneiro]

mathlib4#256 adds some basic triage for mathport. Here's the list of E - easy tactics:

> grep "/- E -/" Mathlib/Mathport/Syntax.lean
/- E -/ syntax tactic " <;> " "[" tactic,* "]" : tactic
/- E -/ syntax (name := mapply) "mapply " term : tactic
/- E -/ syntax (name := trace) "trace " term : tactic
/- E -/ syntax (name := existsi) "exists " term,* : tactic
/- E -/ syntax (name := eConstructor) "econstructor" : tactic
/- E -/ syntax (name := left) "left" : tactic
/- E -/ syntax (name := right) "right" : tactic
/- E -/ syntax (name := symm) "symm" : tactic
/- E -/ syntax (name := trans) "trans" (ppSpace colGt term)? : tactic
/- E -/ syntax (name := substVars) "subst_vars" : tactic
/- E -/ syntax (name := inferOptParam) "infer_opt_param" : tactic
/- E -/ syntax (name := inferAutoParam) "infer_auto_param" : tactic
/- E -/ syntax (name := typeCheck) "type_check " term : tactic
/- E -/ syntax (name := guardLHS) "guard_lhs " " =ₐ " term : conv
/- E -/ syntax (name := apply') "apply' " term : tactic
/- E -/ syntax (name := fapply') "fapply' " term : tactic
/- E -/ syntax (name := eapply') "eapply' " term : tactic
/- E -/ syntax (name := applyWith') "apply_with' " (config)? term : tactic
/- E -/ syntax (name := mapply') "mapply' " term : tactic
/- E -/ syntax (name := rfl') "rfl'" : tactic
/- E -/ syntax (name := symm') "symm'" (ppSpace location)? : tactic
/- E -/ syntax (name := trans') "trans'" (ppSpace term)? : tactic
/- E -/ syntax (name := fsplit) "fsplit" : tactic
/- E -/ syntax (name := fconstructor) "fconstructor" : tactic
/- E -/ syntax (name := tryFor) "try_for " term:max tacticSeq : tactic
/- E -/ syntax (name := substs) "substs" (ppSpace ident)* : tactic
/- E -/ syntax (name := unfoldCoes) "unfold_coes" (ppSpace location)? : tactic
/- E -/ syntax (name := unfoldWf) "unfold_wf" : tactic
/- E -/ syntax (name := recover) "recover" : tactic
/- E -/ syntax (name := «continue») "continue " tacticSeq : tactic
/- E -/ syntax (name := guardHypNums) "guard_hyp_nums " num : tactic
/- E -/ syntax (name := guardTags) "guard_tags" (ppSpace ident)* : tactic
/- E -/ syntax (name := guardProofTerm) "guard_proof_term " tactic:51 " => " term : tactic
/- E -/ syntax (name := failIfSuccess?) "fail_if_success? " str ppSpace tacticSeq : tactic
/- E -/ syntax (name := triv) "triv" : tactic
/- E -/ syntax (name := revertDeps) "revert_deps" (ppSpace colGt ident)* : tactic
/- E -/ syntax (name := revertAfter) "revert_after " ident : tactic
/- E -/ syntax (name := revertTargetDeps) "revert_target_deps" : tactic
/- E -/ syntax (name := clearValue) "clear_value" (ppSpace colGt ident)* : tactic
/- E -/ syntax (name := convert) "convert " "← "? term (" using " num)? : tactic
/- E -/ syntax (name := convertTo) "convert_to " term (" using " num)? : tactic
/- E -/ syntax (name := acChange) "ac_change " term (" using " num)? : tactic
/- E -/ syntax (name := byContra') "by_contra'" (ppSpace ident)? Term.optType : tactic
/- E -/ syntax (name := renameVar) "rename_var " ident " → " ident (ppSpace location)? : tactic
/- E -/ syntax (name := swapVar) "swap_var " (colGt swapVarArg),+ : tactic
/- E -/ syntax (name := normNum1) "norm_num1" (ppSpace location)? : tactic
/- E -/ syntax (name := applyNormed) "apply_normed " term : tactic
/- E -/ syntax (name := abel1) "abel1" : tactic
/- E -/ syntax (name := abel1!) "abel1!" : tactic
/- E -/ syntax (name := ring1) "ring1" : tactic
/- E -/ syntax (name := ring1!) "ring1!" : tactic
/- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? (ppSpace location)? : tactic
/- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? (ppSpace location)? : tactic
/- E -/ syntax (name := ring!) "ring!" : tactic
/- E -/ syntax (name := noncommRing) "noncomm_ring" : tactic
/- E -/ syntax (name := nthRwLHS) "nth_rw_lhs " num rwRuleSeq (ppSpace location)? : tactic
/- E -/ syntax (name := nthRwRHS) "nth_rw_rhs " num rwRuleSeq (ppSpace location)? : tactic
/- E -/ syntax (name := isBounded_default) "isBounded_default" : tactic
/- E -/ syntax (name := unitInterval) "unit_interval" : tactic
/- E -/ syntax (name := mfldSetTac) "mfld_set_tac" : tactic
/- E -/ syntax (name := uniqueDiffWithinAt_Ici_Iic_univ) "uniqueDiffWithinAt_Ici_Iic_univ" : tactic
/- E -/ syntax (name := ghostSimp) "ghost_simp" (" [" simpArg,* "]")? : tactic
/- E -/ syntax (name := wittTruncateFunTac) "witt_truncate_fun_tac" : tactic
/- E -/ syntax (name := guardTarget) "guard_target" " =ₐ " term : conv
/- E -/ syntax (name := normNum1) "norm_num1" : conv
/- E -/ syntax (name := normNum) "norm_num" (" [" simpArg,* "]")? : conv
/- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? : conv
/- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? : conv
/- E -/ syntax (name := ring) "ring" : conv
/- E -/ syntax (name := ring!) "ring!" : conv
/- E -/ syntax (name := ringExp) "ring_exp" : conv
/- E -/ syntax (name := ringExp!) "ring_exp!" : conv

[Mario Carneiro]

These are tactics that should have very short definitions, although this only counts the complexity of the tactic itself and not its dependents; hence these might not be possible to implement properly until some larger dependency is implemented first. Still, you can always add stubs for the dependents if you get in this situation so don't let it stop you.

[Mario Carneiro]

Here's the breakdown:

• E (72 tactics): Easy. It's a simple macro in terms of existing things,
  or an elab tactic for which we have many similar examples. Example: left

• M (91 tactics): Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example: have

• N (36 tactics): Possibly requires new mechanisms in lean 4, some investigation required. Example: propagate_tags
• B (36 tactics): Hard, because it is a big and complicated tactic. Example: linarith
• S (30 tactics): Possibly easy, because we can just stub it out or replace with something else. Example: rsimp

[Arthur Paulino]

@Mario Carneiro do you want to add a link to mathlib4#193 near the syntax for push_neg? It already contains a good chunk of WIP

[Mario Carneiro]

sure, why not

[Siddhartha Gadgil]

Since porting tactics was mentioned again, let me once more alert to https://github.com/leanprover-community/mathlib4/pull/253

I can easily do reflexivity and transitivity along similar lines (the main thing I had to learn was to use attributes and environmental extensions) and also take a shot at hint. But I have no idea what is missing.

[Mario Carneiro]

It looks pretty good, I haven't had time to review of late

[Siddhartha Gadgil]

Thanks. Whenever you get the time.

[Siddhartha Gadgil]

@Arthur Paulino Thanks for triggering the CI rerun - this gives an error because of

initialize symmAttr : TagAttribute ← registerTagAttribute `symm "symmetric relation"

in the Attributes file. However I see no reference to the registered attribute. Is it a placeholder which I should remove?

[Arthur Paulino]

Considering that it's inside the Mathportfolder, I think so, yes. You can wait for a confirmation from Mario or Gabriel or go ahead and just remove it and wait for their review anyway

[Siddhartha Gadgil]

Okay thanks. I will also rename the attribute I created to match the current name.

[Siddhartha Gadgil]

Yes, thanks. I realized that after the first CI failure.

[Siddhartha Gadgil]

It runs fine now. The second CI failure was my not adding the new files to Mathlib.lean