File size: 3,005 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 | import Mathlib.Data.List.Basic
import Mathlib.Data.Finset.Basic
namespace Hieroglyphs
/-- A deliberately bounded alphabet for the signs in the supplied stream. -/
inductive Glyph
| eye -- π
| bread -- π
| mouth -- π
| flax -- π
| stroke -- π€
| god -- πΉ
| ankh -- πΉ
| cobra -- π£
| sun -- π³
| unknownA -- π»
| water -- π
| stool -- πͺ
| owl -- π
| basket -- πΌ
deriving DecidableEq, Repr
def transliterate : Glyph β String
| .eye => "ir"
| .bread => "t"
| .mouth => "r"
| .flax => "h"
| .stroke => "Β·"
| .god => "nαΉ―r"
| .ankh => "κ₯nαΈ«"
| .cobra => "?"
| .sun => "rκ₯"
| .unknownA => "?"
| .water => "n"
| .stool => "p"
| .owl => "m"
| .basket => "g"
/-- A decoding is only certified relative to an explicit grammar and lexicon. -/
structure DecodeSpec where
lexical : List Glyph β Option String
grammatical : List Glyph β Prop
sound : β xs meaning,
lexical xs = some meaning β grammatical xs
/-- Concrete recognition is distinct from semantic translation. -/
def Recognized (xs : List Glyph) : Prop :=
β g, g β xs β
g = .eye β¨ g = .bread β¨ g = .mouth β¨ g = .flax β¨
g = .stroke β¨ g = .god β¨ g = .ankh β¨ g = .cobra β¨
g = .sun β¨ g = .unknownA β¨ g = .water β¨ g = .stool β¨
g = .owl β¨ g = .basket
/-- A formal definition of periodicity for a list. -/
def Periodic (period xs : List Glyph) : Prop :=
period β [] β§ β k, xs = List.join (List.replicate k period)
/-- Example recurring motif β not asserted to be Egyptian grammar. -/
def Motif : List Glyph :=
[.eye, .ankh, .god, .sun, .cobra, .unknownA,
.water, .bread, .flax, .mouth, .stool, .owl]
example : Periodic Motif (Motif ++ Motif) := by
refine β¨by decide, 2, ?_β©
simp [Motif]
/-- A truthful result type: never manufacture a semantic translation. -/
inductive DecodeResult
| transliteration : List String β DecodeResult
| grammatical : String β DecodeResult
| insufficientEvidence : String β DecodeResult
deriving Repr
def decode (spec : DecodeSpec) (xs : List Glyph) : DecodeResult :=
match spec.lexical xs with
| some meaning =>
if spec.grammatical xs then .grammatical meaning
else .insufficientEvidence "Lexicon returned a reading rejected by grammar."
| none =>
.insufficientEvidence
"No certified lexical-and-grammatical interpretation for this glyph sequence."
theorem no_semantic_claim_without_lexicon
(spec : DecodeSpec) (xs : List Glyph)
(h : spec.lexical xs = none) :
decode spec xs =
.insufficientEvidence
"No certified lexical-and-grammatical interpretation for this glyph sequence." := by
simp [decode, h]
end Hieroglyphs
|