Tweety Triangle and Nixon Diamond

[GP96] [AP13]

The two classic default-reasoning testbeds, as finite world types shared by the rival accounts in Studies/GoldszmidtPearl1996 and Studies/AsherPelletier2013:

1. Tweety Triangle (specificity): birds normally fly; penguins are birds; penguins normally don't fly. The more specific default wins.
2. Nixon Diamond (conflicting defaults): Quakers are normally pacifist; Republicans are normally not; Nixon is both.

Main declarations

• TweetyWorld, isBird, isPenguin, flies, penguin_is_bird
• NixonWorld, isQuaker, isRepublican, isPacifist

inductive TweetyNixon.TweetyWorld : Type

The Tweety world: 4 possible states of an entity.

• birdFlies : TweetyWorld
• birdNoFly : TweetyWorld
• penguinFlies : TweetyWorld
• penguinNoFly : TweetyWorld

@[instance_reducible]

instance TweetyNixon.instDecidableEqTweetyWorld : DecidableEq TweetyWorld

Equations

• TweetyNixon.instDecidableEqTweetyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TweetyNixon.instReprTweetyWorld : Repr TweetyWorld

Equations

• TweetyNixon.instReprTweetyWorld = { reprPrec := TweetyNixon.instReprTweetyWorld.repr }

def TweetyNixon.instReprTweetyWorld.repr : TweetyWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TweetyNixon.instFintypeTweetyWorld : Fintype TweetyWorld

Equations

• One or more equations did not get rendered due to their size.

def TweetyNixon.isBird : TweetyWorld → Prop

Equations

• TweetyNixon.isBird TweetyNixon.TweetyWorld.birdFlies = True
• TweetyNixon.isBird TweetyNixon.TweetyWorld.birdNoFly = True
• TweetyNixon.isBird TweetyNixon.TweetyWorld.penguinFlies = True
• TweetyNixon.isBird TweetyNixon.TweetyWorld.penguinNoFly = True

@[instance_reducible]

instance TweetyNixon.instDecidablePredTweetyWorldIsBird : DecidablePred isBird

Equations

• One or more equations did not get rendered due to their size.

def TweetyNixon.isPenguin : TweetyWorld → Prop

Equations

• TweetyNixon.isPenguin TweetyNixon.TweetyWorld.penguinFlies = True
• TweetyNixon.isPenguin TweetyNixon.TweetyWorld.penguinNoFly = True
• TweetyNixon.isPenguin x✝ = False

@[instance_reducible]

instance TweetyNixon.instDecidablePredTweetyWorldIsPenguin : DecidablePred isPenguin

Equations

• One or more equations did not get rendered due to their size.

def TweetyNixon.flies : TweetyWorld → Prop

Equations

• TweetyNixon.flies TweetyNixon.TweetyWorld.birdFlies = True
• TweetyNixon.flies TweetyNixon.TweetyWorld.penguinFlies = True
• TweetyNixon.flies x✝ = False

@[instance_reducible]

instance TweetyNixon.instDecidablePredTweetyWorldFlies : DecidablePred flies

Equations

• One or more equations did not get rendered due to their size.

theorem TweetyNixon.penguin_is_bird (w : TweetyWorld) : isPenguin w → isBird w

Every penguin is a bird.

inductive TweetyNixon.NixonWorld : Type

The Nixon world: 4 possible states.

• quakerPacifist : NixonWorld
• quakerNotPacifist : NixonWorld
• repPacifist : NixonWorld
• repNotPacifist : NixonWorld

@[instance_reducible]

instance TweetyNixon.instDecidableEqNixonWorld : DecidableEq NixonWorld

Equations

• TweetyNixon.instDecidableEqNixonWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TweetyNixon.instReprNixonWorld.repr : NixonWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TweetyNixon.instReprNixonWorld : Repr NixonWorld

Equations

• TweetyNixon.instReprNixonWorld = { reprPrec := TweetyNixon.instReprNixonWorld.repr }

def TweetyNixon.isQuaker : NixonWorld → Prop

Equations

• TweetyNixon.isQuaker TweetyNixon.NixonWorld.quakerPacifist = True
• TweetyNixon.isQuaker TweetyNixon.NixonWorld.quakerNotPacifist = True
• TweetyNixon.isQuaker x✝ = False

def TweetyNixon.isRepublican : NixonWorld → Prop

Equations

• TweetyNixon.isRepublican TweetyNixon.NixonWorld.repPacifist = True
• TweetyNixon.isRepublican TweetyNixon.NixonWorld.repNotPacifist = True
• TweetyNixon.isRepublican x✝ = False

def TweetyNixon.isPacifist : NixonWorld → Prop

Equations

• TweetyNixon.isPacifist TweetyNixon.NixonWorld.quakerPacifist = True
• TweetyNixon.isPacifist TweetyNixon.NixonWorld.repPacifist = True
• TweetyNixon.isPacifist x✝ = False