Umm, how to destruct all those "if then else"?

Stream: Is there code for X?

[Ilmārs Cīrulis]

def White: Nat := 0
def Black: Nat := 1

structure Position (N: Nat) where
  WKx: Nat
  WKy: Nat
  WRx: Nat
  WRy: Nat
  BKx: Nat
  BKy: Nat
  Turn: Nat
  DimensionCheck: WKx < N ∧ WKy < N ∧ WRx < N ∧ WRy < N ∧ BKx < N ∧ BKy < N

def MirrorX {N} (P: Position N): Position N :=
  Position.mk (N - 1 - P.WKx) P.WKy (N - 1 - P.WRx) P.WRy (N - 1 - P.BKx) P.BKy P.Turn
  (by cases P
      simp
      omega)

def MirrorY {N} (P: Position N): Position N :=
  Position.mk P.WKx (N - 1 - P.WKy) P.WRx (N - 1 - P.WRy) P.BKx (N - 1 - P.BKx) P.Turn
  (by cases P
      simp
      omega)

def MirrorDiag {N} (P: Position N): Position N :=
  Position.mk P.WKy P.WKx P.WRy P.WRx P.BKy P.BKx P.Turn
  (by cases P
      simp
      omega)

def Symmetric {N} (P1 P2: Position N) :=
  P1 = P2 ∨ P1 = MirrorX P2 ∨ P1 = MirrorY P2 ∨ P1 = MirrorY (MirrorX P2) ∨
  P1 = MirrorDiag P2 ∨ P1 = MirrorDiag (MirrorX P2) ∨ P1 = MirrorDiag (MirrorY P2) ∨ P1 = MirrorDiag (MirrorY (MirrorX P2))


def NormalizeX {N} (P: Position N): Position N :=
  if 2 * P.BKx + 1 ≤ N
  then P
  else MirrorX P

def NormalizeY {N} (P: Position N): Position N :=
  if 2 * P.BKy + 1 ≤ N
  then P
  else MirrorY P

def NormalizeDiag {N} (P: Position N): Position N :=
  if P.BKy < P.BKx ∨ P.BKy = P.BKx ∧ (P.WKy < P.WKx ∨ P.WKy = P.WKx ∧ P.WRy ≤ P.WRx)
  then P
  else MirrorDiag P

def Normalize {N} (P: Position N): Position N := NormalizeDiag (NormalizeY (NormalizeX P))

def Symmetric' {N} (P1 P2: Position N) := Normalize P1 = Normalize P2


theorem SymmetricAndSymmetric' {N} (P1 P2: Position N): Symmetric P1 P2 ↔ Symmetric' P1 P2 := by
  unfold Symmetric Symmetric'
  unfold Normalize NormalizeDiag NormalizeY NormalizeX
  unfold MirrorX MirrorY MirrorDiag
  cases P1
  cases P2
  simp

1) I want to understand how one can "get rid" of those "if then else" to get multiple (well, gazillions) goals that then can be solved by omega (dunno how much total time it would take, better don't try it yourself). Sorry for noob question. :sweat_smile:
2) Is there some better approach to proving this theorem, maybe? Which is less brute-force use of omega and takes less time...

Thank you! :smile:

[Kevin Buzzard]

Try the split tactic to make progress with an if/then/else goal.

[Ilmārs Cīrulis]

So the correct way is something like repeat split <;> simp <;> omega after the simp...
Seems about right, also the lack of any response by Visual Studio Code is something I expected. :sweat_smile: :grinning_face_with_smiling_eyes:

[Ilmārs Cīrulis]

Anyway, the theorem I wanted to prove is false. Oops! :sweat:

Is there some way to make such Normalize that the theorem becomes true? :pray:
Thanks in advance

[Yury G. Kudryashov]

What are you trying to formalize? Do you have a human readable text about it?

[Ilmārs Cīrulis]

More generally, some basic knowledge about chess endgame king and rook versus lone king. Based on the approach in this document: https://poincare.matf.bg.ac.rs/~janicic/papers/2012-ceciis-chess.pdf

I have proven (in Coq for now) that there are two types of stalemates (up to symmetry) and also two types of checkmates (same). (here)

Not I've tried to prove that there are two types of positions where white checkmate in 1 move, but I am bit stuck with my current approach.

[Ilmārs Cīrulis]

Then I deviated and started to tinker around almost aimlessly. The question was caused by the idea that I could try to define canonical form for positions, such that canonical form of two positions are equal iff the positions are symmetric (one can be made into other by these MirrorX, MirrorY, SwapXY).

[Ilmārs Cīrulis]

Anyway, thank you!

[Ilmārs Cīrulis]

I tried to write such (mutually) inductive definition in Lean:

mutual
  inductive BlackLoss {N}: Position N → Nat → Prop
  | black_lost: ∀ P, Checkmate P → BlackLoss P 0
  | black_lost_S: ∀ P n, (∀ P', LegalBlackMove P P' → ∃ m, WhiteWin P' m ∧ m ≤ n) →
                         (∃ P', LegalBlackMove P P' ∧ WhiteWin P' n) → BlackLoss P (n + 1)
  inductive WhiteWin {N}: Position N → Nat → Prop
  | white_win: ∀ P n, (∃ P', LegalWhiteMove P P' ∧ BlackLoss P' n) → ¬ InsufficientMaterial P → WhiteWin P (n + 1)
end

That gives me error (kernel) invalid nested inductive datatype 'Exists', nested inductive datatypes parameters cannot contain local variables.. Does that mean it's not possible to write it in Lean? :cry: In Coq it was working nicely.

[Ilmārs Cīrulis]

Also, is there a tactic that transforms goal of form ... /\ ... /\ ... /\ ... /\ ... into multiple (in this case 5) goals to prove?
I found very nice tactic obtain that destructs disjunctions and conjunctions but that only works on hypothesis.

[Yaël Dillies]

This tactic is called constructor

[Yaël Dillies]

I would however suggest you do refine ⟨?_, ?_, ?_, ?_, ?_⟩

[Edward van de Meent]

Yaël Dillies said:

This tactic is called constructor

i'm pretty sure constructor would not eliminate into more than 2 goals in that case though?

[Ruben Van de Velde]

Yeah, Yaël meant "multiple applications of constructor"

[Ilmārs Cīrulis]

Thank you very much!

[Ilmārs Cīrulis]

This definition is wrong anyway, because constructor white_win doesn't contain necessary condition that the move LegalWhiteMove P P' is the best possible move.

Lessness said:

I tried to write such (mutually) inductive definition in Lean:

mutual
  inductive BlackLoss {N}: Position N → Nat → Prop
  | black_lost: ∀ P, Checkmate P → BlackLoss P 0
  | black_lost_S: ∀ P n, (∀ P', LegalBlackMove P P' → ∃ m, WhiteWin P' m ∧ m ≤ n) →
                         (∃ P', LegalBlackMove P P' ∧ WhiteWin P' n) → BlackLoss P (n + 1)
  inductive WhiteWin {N}: Position N → Nat → Prop
  | white_win: ∀ P n, (∃ P', LegalWhiteMove P P' ∧ BlackLoss P' n) → ¬ InsufficientMaterial P → WhiteWin P (n + 1)
end

That gives me error (kernel) invalid nested inductive datatype 'Exists', nested inductive datatypes parameters cannot contain local variables.. Does that mean it's not possible to write it in Lean? :cry: In Coq it was working nicely.

[Ilmārs Cīrulis]

Maybe I could take a depth-limited minimax algorithm/function from Wikipedia and define stuff using it?
I can't think a way to work around this limitation of Lean to make inductive definition work.

[Ilmārs Cīrulis]

Is there a better way to do this? Maybe somehow adding some annotation or smth that would force Lean to deduce the instance automatically?

def White: Nat := 0
def Black: Nat := 1

structure Position (N: Nat) where
  WKx: Nat
  WKy: Nat
  WRx: Nat
  WRy: Nat
  BKx: Nat
  BKy: Nat
  Turn: Nat
  DimensionCheck: WKx < N ∧ WKy < N ∧ WRx < N ∧ WRy < N ∧ BKx < N ∧ BKy < N

def NotOnSameSquare {N} (P: Position N): Prop :=
  (P.WKx ≠ P.WRx ∨ P.WKy ≠ P.WRy) ∧ (P.Turn = Black → (P.WRx ≠ P.BKx ∨ P.WRy ≠ P.BKy))

instance: ∀ {N} (P: Position N), Decidable (NotOnSameSquare P) := by
  unfold NotOnSameSquare
  intros
  apply instDecidableAnd

[Damiano Testa]

After unfold, infer_instance works.

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

have temp: (0 < P.BKx ∧ 0 < P.BKy) ∨ ¬ (0 < P.BKx ∧ 0 < P.BKy) := by omega
I can prove this using omega, sure, but is there to use the fact that this is Decidable? To do something like cases (0 < P.BKx ∧ 0 < P.BKy) to get two different cases (the statement and its negation)? With something else in the place of cases, of course.

[Ilmārs Cīrulis]

Oh, it's by_cases tactic, it seems. :)

[Damiano Testa]

decide is a tactic that uses Decidable instances, so you may try that.

[Ilmārs Cīrulis]

Next noob question - how to destruct "if then else" if it is in the hypothesis? :pray:

[Edward van de Meent]

something that you can do in most of these cases:
use if h:cond then rw [if_pos h] ;sorry else rw [if_neg h];sorry

[Daniel Weber]

You can also use split at h

[Ilmārs Cīrulis]

Thank you!

[James Sully]

It seems like it would be useful to have a tactic that checks the context for a hypothesis h matching either the condition or its negation, then either rewrites with if_pos or if_neg as appropriate.
simp does it

example (hp : p = true) (h2 : if p then q else r) : q := by
  simp [hp] at h2
  exact h2

[Ilmārs Cīrulis]

The last infer_instance isn't working for some reason. :(
As far as I can see, everything necessary for it is already declared as Decidable. Did I do something wrong?

[Ilmārs Cīrulis]

I found my mistake. I declared instance of Decidable (OtherAfterMoveWhiteking P1 P2) twice.

[Ilmārs Cīrulis]

I got such mistake from Lean:

code generator does not support recursor 'List.rec' yet, consider using 'match ... with' and/or structural recursion

So, I'm trying to make this tiny def to work by using match ... with (for training purposes):

def test {N} (L: List Nat): (∀ i, i ∈ L → i < N) -> List (Fin N) :=
  match L with
  | nil => fun _ => List.nil
  | a :: l => fun H => List.cons (by sorry) (by sorry)

But it says something about redundant alternative. Stuck with this, probably, very noob problem.

[Ruben Van de Velde]

Try .nil =>

[Ilmārs Cīrulis]

O, thank you very much!

[Ilmārs Cīrulis]

The current work can be seen here.

How would you approach the proof? Maybe by rewriting AllWhiteRookMoves in some other way... :thinking:
I'm stuck at the first sorry of the last theorem (the second sorry will be done the same way as the first).

[Ilmārs Cīrulis]

rewrote AllWhiteRookMoves in simpler way, using Fin.list:

def AllWhiteRookMoves {N} (P: Position N): List (Position N) := by
  have makePosition1: ∀ (x: Fin N), Position N := by
    intros x
    refine (@Position.mk N P.WKx P.WKy x.1 P.WRy P.BKx P.BKy White (by cases x; cases P; simp at *; omega))
  have makePosition2: ∀ (y: Fin N), Position N := by
    intros y
    refine (@Position.mk N P.WKx P.WKy P.WRx y.1 P.BKx P.BKy White (by cases y; cases P; simp at *; omega))
  have L1: List (Position N) := List.map makePosition1 (Fin.list N)
  have L2: List (Position N) := List.map makePosition2 (Fin.list N)
  have L := L1 ++ L2
  exact List.filter (λ p => Decidable.decide (LegalMoveWhiteRook P p)) L

That should make following proof much simpler.

[Ilmārs Cīrulis]

I tried to find that using Loogle and looking into the Batteries, but wasn't successful for now.
How can one prove this seemingly simple theorem? :pray:

import Batteries.Data.Fin.Basic

theorem t: ∀ {N} (f: fin N), f ∈ Fin.list N := by sorry

[Edward van de Meent]

import Batteries.Data.Fin.Basic
import Batteries.Data.Fin.Lemmas


theorem t: ∀ {N} (f: Fin N), f ∈ Fin.list N := by
  intro n m
  refine List.mem_iff_get.mpr ?_
  have : m.val < (Fin.list n).length := by
    rw [Fin.length_list]
    exact m.2
  refine ⟨⟨m.val,this⟩,?_⟩
  simp only [List.get_eq_getElem, Fin.getElem_list, Fin.cast_mk, Fin.eta]

[Edward van de Meent]

there you go

[Ilmārs Cīrulis]

Maybe someone wants to help with defining/finding correct definition of Normalize? Such that
forall {N} (P1 P2: Position N), SamePosition P1 P2 <-> Normalize P1 = Normalize P2.

Necessary minimum here:

def White: Nat := 0
def Black: Nat := 1

structure Position (N: Nat) where
  WKx: Nat
  WKy: Nat
  WRx: Nat
  WRy: Nat
  BKx: Nat
  BKy: Nat
  Turn: Nat
  DimensionCheck: WKx < N ∧ WKy < N ∧ WRx < N ∧ WRy < N ∧ BKx < N ∧ BKy < N


def MirrorX {N} (P: Position N): Position N :=
  Position.mk (N - 1 - P.WKx) P.WKy (N - 1 - P.WRx) P.WRy (N - 1 - P.BKx) P.BKy P.Turn
  (by cases P
      simp
      omega)

def MirrorY {N} (P: Position N): Position N :=
  Position.mk P.WKx (N - 1 - P.WKy) P.WRx (N - 1 - P.WRy) P.BKx (N - 1 - P.BKy) P.Turn
  (by cases P
      simp
      omega)

def MirrorDiag {N} (P: Position N): Position N :=
  Position.mk P.WKy P.WKx P.WRy P.WRx P.BKy P.BKx P.Turn
  (by cases P
      simp
      omega)

def SamePosition {N} (P1 P2: Position N) :=
  P1 = P2 ∨ P1 = MirrorX P2 ∨ P1 = MirrorY P2 ∨ P1 = MirrorY (MirrorX P2) ∨
  P1 = MirrorDiag P2 ∨ P1 = MirrorDiag (MirrorX P2) ∨
  P1 = MirrorDiag (MirrorY P2) ∨ P1 = MirrorDiag (MirrorY (MirrorX P2))

def Normalize {N} (P: Position N): Position N := sorry

theorem Thm {N} (P1 P2: Position N): SamePosition P1 P2 ↔ Normalize P1 = Normalize P2 := sorry

[Yakov Pechersky]

You could give your Positions a lexicographic order. Then for each Mirror op, show that doing it (or reverse) monotonically decreases the Position. Then if you have that SamePosition, normalization would be to keep running allowed ops to decrease the larger of the two to the smaller

[Ilmārs Cīrulis]

Interesting idea, thank you!

Although, I found a few mistakes in my previous approach, will try it once again.

[Ilmārs Cīrulis]

Yes, replaced wrong <= with <... I already started doubting omega... :grimacing:

Never doubt omega! :sweat_smile:

[Ilmārs Cīrulis]

Hello again! Noob question time... :sweat_smile:

What's the easiest way to do development in multiple files, compiling (?) finished ones and then importing them into currently developed one?

[Edward van de Meent]

i'd say the best way is to create a project, and let vscode/lake handle the management of what compiles when. if you do this, you can simply write import MyProject.Path.To.File and it will expose the declarations you need.

[Ilmārs Cīrulis]

Ok, will try. Thank you!

[Edward van de Meent]

for creating a project using vscode, you can click the forall symbol in the toolbar, it's really useful

[Edward van de Meent]

ofcourse assuming you have the lean4 extension

[Ilmārs Cīrulis]

Thank you. Yes, I have, and actually I'm doing this KRk endgame stuff inside a project (which I made some time ago).

Now dividing the single lean file into multiple ones and hoping that everything works.

[Ilmārs Cīrulis]

Kinda success. :smile: Except maybe the proof is too big or smth for Visual Studio, it slows it down.

Anyway, now it's located here

[Ilmārs Cīrulis]

Is there something that I can do to make VS Code and/or Lean faster? Dunno, give it more RAM in some way or smth?

[Ilmārs Cīrulis]

:sob: I can't finish the proof because Lean has slowed to crawl :sob:

Probably my punishment for making unwieldy proofs, but still...

[Ilmārs Cīrulis]

image.png
No idea, if this is normal or not. (Used memory by lean keeps increasing.)

[Kim Morrison]

Usually it is an indication that you've given the kernel something terrible that it is struggling with. Can you post a #mwe (perhaps in a new thread!).

If you're not on v4.9.1 or v4.10.0-rc2, you might try those, as there was a recent cancellation bug fix that previously had sometimes resulted in excessive memory usage.

[Ilmārs Cīrulis]

Could this terrible thing be too many omegas, maybe together with lots of simps? Like this?

I will try to make #mwe, of course

[Kim Morrison]

Doesn't look terrible at first glance...

[Ilmārs Cīrulis]

Here is explanation for the slowness of omega tactics. Maybe it's useful for someone else too.

[Ilmārs Cīrulis]

Back to beginner questions... Is it possible to name new hypotheses as I want, when doing split of if then else construction in goal? :pray:

[Edward van de Meent]

yes, using rename_i, you can rename shadowed hypotheses in order of most-recently introduced to last.

[Ilmārs Cīrulis]

Thank you!

[Edward van de Meent]

i.e. rename_i h1 h2 h3 renames the most recent to h3, the second most recent to h2, etc

[Ilmārs Cīrulis]

I want to destruct all disjunctions and conjunctions in hypotheses (recursively?) until there's nothing left to destroy. Something like intuition tactic does in Coq.

Do I need to write my own tactic for that?

[Ilmārs Cīrulis]

It seems that tauto tactic from Mathlib does that.

[Edit]: Not exactly, afaict, because "This is a finishing tactic: it either closes the goal or raises an error." But still will be useful sometimes.

[Kevin Buzzard]

I think that using this (already poorly-named) thread to ask a series of questions unrelated to its title is not really a good idea. Why not start a new thread in an appropriate channel for the next question?

[Ilmārs Cīrulis]

Thank you, will do!