error puzzle

Stream: lean4

[Damiano Testa]

In the spirit of Patrick's recent post, here is another puzzle: can you guess the error in the code below, without using Lean?

example : False ↔ False :=
  ⟨fun h => by cases h, fun h => by cases h⟩

Trivia: there are a couple of porting notes about this.

[Kyle Miller]

It helped knowing that there was an error to be able to figure it out: cases supports multiple targets if the recursor for the types supports it (which I've never seen used in the wild yet), and the syntax is cases x,y,z

This fixes it:

example : False ↔ False :=
  ⟨fun h => (by cases h), fun h => by cases h⟩

[Damiano Testa]

Correct!

also this fixes it:

example : False ↔ False :=
  ⟨fun h => by cases h;, fun h => by cases h⟩

[Eric Rodriguez]

Kyle Miller said:

It helped knowing that there was an error to be able to figure it out: cases supports multiple targets if the recursor for the types supports it (which I've never seen used in the wild yet), and the syntax is cases x,y,z

This fixes it:

example : False ↔ False :=
  ⟨fun h => (by cases h), fun h => by cases h⟩

This is useful for induction with for example docs#Nat.le_induction, but what's the expected usecase for this cases extension? A similar thing?

[Mario Carneiro]

By the way, use has a similar issue

[Damiano Testa]

Another one: what is the error in

example (x : Bool) (h : false ∨ true) : True := by
  match x with
    | true => rcases h with ⟨⟩
    | false
              exact .intro
              exact .intro
    | false => exact .intro

[Damiano Testa]

example : True := trivial

/-- /-  <-- What do you think that the error is on this line?

Error

unused `termination_by?`, function is not recursive