13
votes
12
votes
10
votes
9
votes
Lean golf: List Game Lv1 (rev_rev)
Lean, 101 bytes
def r:∀s,rev(@rev A s)=s|[]:=rfl|(x::t):=by
conv{to_rhs,rw<-r t};simp;induction rev t;simp;simp[ih]
Try it online!
I'm pretty happy with this.
...
- 94.5k
9
votes
8
votes
Lean golf: List Game Lv1 (rev_rev)
Lean, 102 93 bytes
def R:∀s,rev(@rev A s)=s:=by let:(∀s(h:A),rev(s++h::[])=h::rev s);intro;induction s;simp*
Try it on Lean Web Editor
The 102 byte solution I ...
- 38.9k
6
votes
Every Pong is Abelian
Lean, 115 103 100 bytes
def P:=@add_assoc
def V(A)[pong A](a b:A):a+b=_:=by rw[<-right_id$a+b,<-P,P a,<-P b,left_id,left_id]
Try it on Lean Web Editor!
-...
- 70.2k
6
votes
5
votes
Tips for golfing in Lean
Introductions
If you've just finished the natural number game you may be familiar with the intro tactic, this can be used to create implications / functions. ...
- 94.5k
4
votes
Every Pong is Abelian
Lean, 141 140 121 bytes
Saved one byte thanks to Wheat Witch/Wheat Wizard
Saved 19 bytes thanks to Kyle Miller!
...
- 398
4
votes
Tips for golfing in Lean
Use by instead of begin ... end
by can be shorter than ...
3
votes
Tips for golfing in Lean
The ; and <|> combinators.
; makes it so that all subgoals created by the last tactic ...
- 227
2
votes
Only top scored, non community-wiki answers of a minimum length are eligible