Can't prove A v B <-> B v A the usual way in lean4

Stream: lean4

[Daniel Donnelly]

image.png

I just copied / pasted from here:

https://stackoverflow.com/a/61771167/7076615

[rami3l]

Hi! What you've just copied is in fact Lean 3, which is not compatible with Lean 4.

[rami3l]

You might want to try the following:

example : p ∨ q ↔ q ∨ p :=
  Iff.intro
  (λ | .inl h => .inr h | .inr h => .inl h)
  (λ | .inl h => .inr h | .inr h => .inl h)

[Daniel Donnelly]

@rami3l That's awesome, but how does that "|" vertical bar notation work?

[rami3l]

(It turns out that assume h : p, t just a sugar of λ h : p, t in Lean 3, which should just be written with a lambda now.)

[Daniel Donnelly]

@rami3l yes, but understand, your code looks nothing like that syntax! What's |?
:)

[rami3l]

Daniel Donnelly said:

rami3l That's awesome, but how does that "|" vertical bar notation work?

Oh,

(λ
  | .inl h => .inr h
  | .inr h => .inl h)

is just the same as

(λ x => match x with
  | .inl h => .inr h
  | .inr h => .inl h)

[Daniel Donnelly]

@rami3l How can you have .inl without anything on the front of .?

[rami3l]

A more literal translation of your original code:

example : p ∨ q ↔ q ∨ p :=
Iff.intro
  (λ hpq : p ∨ q => Or.elim hpq
    (λ hp : p => Or.inr hp)
    (λ hq : q => Or.inl hq))
  (λ hqp : q ∨ p => Or.elim hqp
    (λ hq : q => Or.inr hq)
    (λ hp : p => Or.inl hp))

[Daniel Donnelly]

@rami3l Thank you!

[Daniel Donnelly]

@rami3l is there a way to do that using have / show?

[rami3l]

Daniel Donnelly said:

rami3l How can you have .inl without anything on the front of .?

Briefly speaking, because Lean knows that you are matching against an Or, that is.

[Daniel Donnelly]

We will study your proof carefully :)

[rami3l]

Daniel Donnelly said:

rami3l is there a way to do that using have / show?

I only know about Lean 4, but it seems to me that the tactics mode is quite consistent between both versions, except that in Lean 4 you should use by to start using tactics, and ; instead of , as terminators.

You should be able to learn from the examples in the tutorial:

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html?highlight=show#structuring-tactic-proofs

[rami3l]

(I guess that the usages of have and show haven't changed too much, so if you have valid Lean 3 code using those constructs, you'll probably be fine in Lean 4 after some simple syntax rewrites.)

[rami3l]

@Daniel Donnelly Do you have a more concrete example of how you want to use have or show in this case?

[Daniel Donnelly]

rami3l said:

Daniel Donnelly said:

rami3l is there a way to do that using have / show?

I only know about Lean 4, but it seems to me that the tactics mode is quite consistent between both versions, except that in Lean 4 you should use by to start using tactics, and ; instead of , as terminators.

You should be able to learn from the examples in the tutorial:

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html?highlight=show#structuring-tactic-proofs

I like this version, it's more _fun_:

example : p ∨ q ↔ q ∨ p :=
Iff.intro
  (fun hpq : p ∨ q => Or.elim hpq
    (fun hp : p => Or.intro_right q hp)
    (fun hq : q => Or.intro_left p hq))
  (fun hqp : q ∨ p => Or.elim hqp
    (fun  hq : q => Or.intro_right p hq)
    (fun hp : p => Or.intro_left q hp))