InsertionSortGolf

Changes

1 changed files (+21/-0)

• InsertionSortGolf.lean (new)
  • @@ -0,0 +1,21 @@
    + variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α) + + @[grind]def I(n:α) + |[]=>[n] + |h::t=>ite (n≤h) (n::h::t) (h::I n t) + + @[grind]def S:List α→List α + |[]=>[] + |h::t=>I h<|S t + + @[grind]def D:List α→Prop + |[]|[_]=>True + |h::h'::t=>h≤h'∧D (h'::t) + + theorem A:(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with + |nil=>grind + |cons _ t=>cases t<;>grind + + example:D (S l)∧l.Perm (S l):=by induction l with + |nil=>grind + |cons h t=>grind [A (n:=h)<|S t]