Tactics for permut

[Ayertienna]

Self-explanatory; rewriting permutations 1000 times per proof reduces readability, we don't want to do this manually anymore!

[Ayertienna]

Depending on #29 and #19

[Ayertienna]

This is currently been done:

• there are 2 libraries: PermutLib and PPermutLib - in label-free language we mostly use the latter

PPermut

• most of the lemmas are admitted
• there is some automation, but not all of the cases are covered, there are also way too specialized lemmas
• might be a good idea to look at how permut_simpl in Metatheory was implemented

Permut

• almost nothing there, except for the proof that permut is in fact equivalence relation

Usage

• in label-free language definition there are currently no known skipped lemmas about permutation
• types_LF was added as a morphism for PPermut, so we can rewrite the background freely
• need some auto rewrite tactic for that (one that auto-finds and prooves the required permutation)
• the same should be done for the main context and simple permut (also to allow rewrites here; it's used less often, but it is still used nevertheless)

Summary

• needs more work!

[Ayertienna]

PPermut

• nothing admitted; automation done like in Metatheory (PPermut_simpl)
• this is more or less complete

Permut

• two lemmas left in "admitted" state, they have their separate bugs assigned

So for label free language, this is basically completed