search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 10 forks source link

introduce 'trans' on Logos or Implis (and also use it elsewhere) #50

Open TentativeConvert opened 4 months ago

TentativeConvert commented 4 months ago

'trans' as a replacement for 'calc' will feel more natural if we introduce it early. I even think there are many instances of repeated 'rw's where repeated 'trans' will be more intuitive. Implis level 8 is a good example. The hint spells out a "calculation" (sequence of equivalences), which is easy to follow using 'trans'.

It's unfortunate that 'trans' does not apply to implications. But of course 'rw' doesn't either, so that's not a loss.

TentativeConvert commented 4 months ago

Here's a first attempt: https://github.com/hhu-adam/Robo/commit/08bf4dc207c010265f181b478c279208805c49a5

joneugster commented 3 months ago

leanprover-community/mathlib4#13719 adds functionality to trans to work with implications.

example {A B C: Prop} (h : A → B) (g : B → C) : A → C := by
  trans B
  · -- ⊢ A → B
    exact h
  · -- ⊢ B → C
    exact g