help with relations in a logic puzzle

Stream: new members

[Lucas Bazante]

I'm formalizing a logic puzzle described in Leanprover 3 - A Logic Puzzle for a lecture. The book is from Lean 3, but I'm using Lean 4. I've already solved it (at least i think i did), but i think the code is very messy.

I've defined an inductive type for the persons in the puzzle, and propositions/relations about them. This part of the code looks like this

inductive Person : Type where
  | Alice
  | Husband
  | Brother
  | Son
  | Daughter
  deriving Repr

open Person

-- relations
def inBar : Person -> Prop := λ_ => True
def inBeach : Person -> Prop := λ_ => True
def isAlone : Person -> Prop := λ_ => True
def isVictim : Person -> Prop := λ_ => True
def isKiller : Person -> Prop := λ_ => True
def hasTwin : Person → Prop := λ_ => True
def isOlder : Person → Person → Prop := λ_ _ => True

I've done it so it works with the rest of my code, and it works as it should, i can use them as long as i have a proof of them.
But I'm really new to Lean, and this looks very odd to me. Is there a better way of defining a proposition like this?

[Luigi Massacci]

Well you could move the Person term to the left of the colon, but that seems reasonable

[Luigi Massacci]

and presumably you have some kind of match statement in the body of the definitions

[Lucas Bazante]

OK! After this topic, i've changed the defs for axioms, so i don't have to define a body for a predicate/relation that really doesn't have one. I hope it isn't weird and hacky still.

[Mark Fischer]

I think this is a great place for opaque. The compiler will create a term that inhabits the type (from the Inhabited type class) if it can, but you don't have access to the proof term. This acts a bit like Axiom, but there's no risk that you've introduced an inconsistency.

-- relations
opaque inBar : Person -> Prop
opaque inBeach : Person -> Prop
opaque isAlone : Person -> Prop
opaque isVictim : Person -> Prop
opaque isKiller : Person -> Prop
opaque hasTwin : Person → Prop
opaque isOlder : Person → Person → Prop

---

I'd be interested too see the rest of formalization :)

[Mark Fischer]

This is my natural language style interpretation of the puzzle, I'm not sure if it's correct. Feels like this might not be the best approach.

The idea was to get each h1 through h6 to read more or less directly like the puzzle clues. e1 through e18 are meant to be facts about the world that the puzzle author might reasonably grant the solver.

Seems like you really need to lean on the fact that there are exactly 5 roles, which is one role per person. I dunno, I gave it a quick try but it felt a bit tedious as it seemed like quite often the only way to solve certain goals was to list every possibility and eliminate all but one. I'm sure that there are tactics I'm not too familiar with that would help it along.

inductive Person : Type where
  | Alice
  | Husband
  | Brother
  | Son
  | Daughter

open Person

opaque man : Person → Prop
opaque woman : Person → Prop
opaque inBar : Person → Prop
opaque victim : Person → Prop
opaque killer : Person → Prop
opaque atBeach : Person → Prop
opaque alone : Person → Prop
opaque together : Person → Person → Prop
opaque twin : Person → Person → Prop
opaque younger : Person → Person → Prop

theorem summers
  -- Some extralogical assumptions
  -- -- man/woman
  (e₁ : ∀x, woman x ∨ man x)
  (e₂ : woman x ↔ ¬man x)
  (e₃ : woman Alice)
  (e₄ : man Husband)
  (e₅ : man Brother)
  (e₆ : man Son)
  (e₇ : woman Daughter)
  -- -- age
  (e₈ : younger Son Alice)
  (e₉: younger Son Husband)
  (e₁₀: younger Daughter Alice)
  (e₁₁: younger Daughter Husband)
  -- -- twins
  (e₁₂: ∀x y, younger x y → ¬twin x y)
  -- -- location
  (e₁₃: ∀x y, alone x → ¬together x y)
  (e₁₄: ∀x, inBar x ∨ atBeach x ∨ alone x)
  (e₁₅: ∀x y, inBar x ∧ inBar y → together x y)
  (e₁₆: ∀x y, atBeach x ∧ atBeach y → together x y)
  -- -- murder
  (e₁₇: ∃!x, killer x)
  (e₁₈: ∃!x, victim x)
  -- Translated Clues
  (h₁ : ∃x y, man x ∧ woman y ∧ inBar x ∧ inBar y)
  (h₂ : ∀x y, killer x ∧ victim y → together x y ∧ atBeach x ∧ atBeach y)
  (h₃ : alone Son ∨ alone Daughter)
  (h₄ : ¬together Alice Husband )
  (h₅ : ∀x y, twin x y ∧ victim x → ¬killer y)
  (h₆ : ∀x y, killer x ∧ victim y → younger y x)
  : victim Brother ∧ killer Husband := sorry

I'm not really sure what the best way to say something like "2/5 people are in the bar, 2/5 people are at the beach, and the last person is alone." It's a very easy step informally, but I'm not sure how to translate that idea in a way that cashes out later in the poof.

Ah well! :)

[Andrew Yang]

Here is my implementation (and I have a proof to make sure this formalization is correct)
I do not like the fact that

1. I cannot logically conclude that Alice is a woman. (edit: not assumed)

2. I cannot logically conclude that the two kids are younger than the husband
   (fun fact: My paternal grandmother is younger than some of my paternal grandfather's sons;
   but maybe "their" means "Alice and Husband's" and not just Alice's and "their son" means "their biological son", which solves 1 and 2)

3. The worst one of all: (5) actually means "The victim has a twin among the four other people who is not the killer" (and that the only permissible pair of twins are (Alice, Brother) and (Son, Daughter))

All these make me feel that this is more of a riddle than a logical puzzle. Or maybe I'm just not familiar enough with logical puzzles to know the hidden assumptions.

inductive Person : Type where
  | Alice
  | Husband
  | Brother
  | Son
  | Daughter
  deriving Inhabited

open Person

inductive Location : Type where
  | Bar
  | Beach
  | SomewhereElse
  deriving Inhabited

opaque Person.location : Person → Location

def Together (x y : Person) : Prop :=
  x.location = .Bar ∧ y.location = .Bar ∨ x.location = .Beach ∨ x.location = .Beach

inductive Gender : Type where
  | Male
  | Female
  | Unknown
  deriving Inhabited

opaque Person.gender : Person → Gender

inductive mightBeTwins : Person → Person → Prop where
  | aliceBrother : mightBeTwins Alice Brother
  | brotherAlice : mightBeTwins Brother Alice
  | sonDaughter : mightBeTwins Son Daughter
  | daughterSon : mightBeTwins Daughter Son

opaque younger : Person → Person → Prop
opaque isTwin : Person → Person → Prop

def summers
    (killer : Person)
    (victim : Person)
    (h₀ : killer ≠ victim)
    (h₁ : ∀ p₁ p₂, younger p₁ p₂ → ¬ younger p₂ p₁)
    (h₃ : ∀ p₁ p₂, isTwin p₁ p₂ → mightBeTwins p₁ p₂)
    (h₅ : younger Son Husband)      -- Maybe?
    (h₇ : younger Daughter Husband) -- Maybe?
    -- Gender Clues
    (gH : Husband.gender = .Male)
    (gS : Son.gender = .Male)
    (gD : Daughter.gender = .Female)
    (gB : Brother.gender = .Male)
    -- Translated Clues
    (H₁ : ∃ x y : Person, x.gender = .Male ∧ y.gender = .Female ∧ x.location = .Bar ∧ y.location = .Bar)
    (H₂ : killer.location = .Beach ∧ victim.location = .Beach)
    (H₃ : (∀ x, Together x Son → x = Son) ∨ (∀ x, Together x Daughter → x = Daughter))
    (H₄ : ¬ Together Alice Husband)
    (H₅ : ∃ x, isTwin victim x ∧ killer ≠ x)
    (H₆ : younger killer victim) :
    victim = Brother := by sorry

[Mark Fischer]

Yeah, I can see how including inductive types for Location and Gender makes sense. Though this means that nobody is alone at the beach as a matter of definition which doesn't seem right. The fact that people are together at the beach emerges from the clues.

I also think mightBeTwins should be derived from information about their ages (as per your second point).

Yeah, choosing how to formalize such puzzles isn't always easy. There's often room for ambiguity since the Author of the puzzle just used plain English. I think that assuming Alice is female makes sense in context, especially since assuming otherwise forces the daughter to be at the bar, which forces the son to be alone, and causes a contradiction.

This definitely has many improvements over what I did :)

[Andrew Yang]

Though this means that nobody is alone at the beach as a matter of definition which doesn't seem right.

I think renaming Alone to AloneAndNotAtTheBeachNorAtTheBar solves this.

[Andrew Yang]

No. H₃ need some tweaks in that case.

[Andrew Yang]

Okay I improved it a bit (edited the code above)