Documentation

Linglib.Discourse.Role

Discourse roles #

This file defines the two discourse roles, speaker and addressee, the participants a speech-act context distinguishes ([Kap89]) and the agents of a two-party commitment model ([Gun01], [FB10]). A role's counterpart is the other participant (Discourse.Role.other), an involution without fixed points, so a statement about every role is a statement about a role and its counterpart (Discourse.Role.forall_role'), and the roles form a nontrivial type.

Main definitions #

Discourse.Role — speaker or addressee.
Discourse.Role.other — the other participant.

References #

inductive Discourse.Role :

A discourse role is one of the two participants of a speech act, its speaker or its addressee.

speaker : Role
addressee : Role

Instances For

@[instance_reducible]

instance Discourse.instDecidableEqRole :

DecidableEq Role

Equations

Discourse.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Discourse.instReprRole :

Repr Role

Equations

Discourse.instReprRole = { reprPrec := Discourse.instReprRole.repr }

def Discourse.instReprRole.repr :

Role → ℕ → Std.Format

Equations

Discourse.instReprRole.repr Discourse.Role.speaker prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Discourse.Role.speaker")).group prec✝
Discourse.instReprRole.repr Discourse.Role.addressee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Discourse.Role.addressee")).group prec✝

Instances For

@[instance_reducible]

instance Discourse.instInhabitedRole :

Inhabited Role

Equations

Discourse.instInhabitedRole = { default := Discourse.instInhabitedRole.default }

@[instance_reducible]

instance Discourse.instFintypeRole :

Fintype Role

Equations

Discourse.instFintypeRole = { elems := { val := ↑Discourse.Role.enumList, nodup := Discourse.Role.enumList_nodup }, complete := Discourse.instFintypeRole._proof_1 }

def Discourse.Role.other :

The other participant: the addressee of the speaker and the speaker of the addressee.

Equations

Instances For

@[simp]

theorem Discourse.Role.other_speaker :

speaker.other = addressee

@[simp]

theorem Discourse.Role.other_addressee :

addressee.other = speaker

@[simp]

theorem Discourse.Role.other_other (r : Role) :

r.other.other = r

theorem Discourse.Role.other_involutive :

Function.Involutive other

theorem Discourse.Role.other_injective :

Function.Injective other

@[simp]

theorem Discourse.Role.other_inj {r s : Role} :

r.other = s.other ↔ r = s

theorem Discourse.Role.other_ne_self (r : Role) :

r.other ≠ r

theorem Discourse.Role.self_ne_other (r : Role) :

r ≠ r.other

theorem Discourse.Role.eq_other_of_ne {r s : Role} :

r ≠ s → r = s.other

theorem Discourse.Role.eq_other_iff {r s : Role} :

r = s.other ↔ r ≠ s

instance Discourse.Role.instNontrivial :

Nontrivial Role

theorem Discourse.Role.card :

Fintype.card Role = 2

theorem Discourse.Role.forall_role' {p : Role → Prop} (r : Role) :

(∀ (s : Role), p s) ↔ p r ∧ p r.other

@[simp]

theorem Discourse.Role.forall_role {p : Role → Prop} :

(∀ (r : Role), p r) ↔ p speaker ∧ p addressee

theorem Discourse.Role.exists_role' {p : Role → Prop} (r : Role) :

(∃ (s : Role), p s) ↔ p r ∨ p r.other

@[simp]

theorem Discourse.Role.exists_role {p : Role → Prop} :

(∃ (r : Role), p r) ↔ p speaker ∨ p addressee