Port proofmode/coq_tactics.v and ltac_tactics.v

[lzy0505]

Summary

Port the remaining items from proofmode/coq_tactics.v and proofmode/ltac_tactics.v.

Note: Split into the files in Tactics/ in the Lean port.

Subtasks

• iStartProof with bi specified feat: istart with BI specified #505
• iEval feat: ieval, isimp and iunfold #490
• iSimpl feat: ieval, isimp and iunfold #490
• iUnfold feat: ieval, isimp and iunfold #490
• iPure: pure destructuring patterns (also for other tactics using ipure)
• iFrame Port iFrame #358 Support existential quantifiers in iFrame #390
• iRevert: intoIH revert feat: iinduction #430
• iSpecialize: all specialization patterns feat: remaining specialisation patterns #500
• iNext (with later credits)
• iDestruct (icases): all destruct patterns feat: remaining introduction patterns and case destruction patterns #496
• iCombine Port iCombine #359
• iIntros: all intro patterns feat: remaining introduction patterns and case destruction patterns #496
• iInduction Port iInduction #360
• iLöb Port iLöb #361
• iRewrite Port iRewrite #362
• iInv Port iInv #363
• iAccu Port iAccu #364
• Rules for trivial

Already ported

• iSolveSideCondition
• iStartProof (basic)
• iStopProof
• iRename
• iClear (basic + selection patterns)
• iExact
• iAssumption
• iExFalso
• iPure (basic)
• iEmpIntro
• iPureIntro
• iRevert (basic + selection patterns)
• iPoseProof (Lean: ihave _ := _)
• iSpecialize (basic + duplicate context for persistent conclusion)
• iApply
• iLeft
• iRight
• iSplit(L/R)
• iExists
• iModIntro
• iMod
• iDestruct (basic)
• iIntros (basic)
• iAssert (Lean: ihave _ : _)

Dependencies

Rocq dependencies:

• bi/bi (aggregation)
• Port bi/telescopes.v #211
• Port proofmode/classes.v #219
• Port proofmode/classes_make.v #212
• Port proofmode/intro_patterns.v #213
• Port modality_embed_mixin in proofmode/modality_instances.v #225
• Port proofmode/spec_patterns.v #215