## Stream: math-comp users

### Topic: Wordle in MathComp

#### Karl Palmskog (Feb 10 2022 at 19:41):

Joey Dodds posted the following formalization of wordle in Coq:

``````Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope string_scope.

(* Make it print lists one item per line*)
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
(format "[ '[' x ;  '//' y ;  '//' .. ;  '//' z ']' ]") : list_scope.

Record gameState {word : string} := mkState
{
turn : nat
; responses : list string
}.

Definition freshGameState {word: string} : @gameState word :=
{| turn := O; responses := ["_ _ _ _ _ "] |}.

(* allow simpl to unfold this *)
Arguments freshGameState /.

Fixpoint containsChar (str : string) (char : ascii) : bool :=
match str with
| "" => false
| String c rest => if eqb c char then true else containsChar rest char
end.

Fixpoint matchLetters (startGoal : string) (goal : string) (guess : string) : string :=
match goal, guess with
| String c1 r1, String c2 r2 => (if eqb c1 c2
then "X "
else if containsChar startGoal c2
then "O "
else "_ ") ++
(matchLetters startGoal r1 r2)
| _, _ => ""
end.

Definition updateGameState {word} (guess : string) (state : @gameState word) : @gameState word :=
{|turn := S (turn state); responses := (responses state) ++ [matchLetters word word guess]|}.

Arguments updateGameState /.

Compute updateGameState "stain" (@freshGameState "saint").

Inductive wonGame {word} : @gameState word -> Prop :=
| advance : forall (guess: string) (st: gameState), wonGame (updateGameState guess st) -> wonGame st
| win : forall st : gameState, turn st < 6 -> In "X X X X X " (responses st) -> wonGame st.

Ltac start := simpl.
Ltac guess st := apply (advance st); try (solve [apply win; repeat constructor]); simpl.

Notation "> rs" := (wonGame {|turn := _; responses := rs|}) (at level 70).

Goal wonGame (@freshGameState "value").
start.
guess "stain".
guess "overt".
guess "venue".
guess "value".
Qed.
``````

I think a MathComp formalization would look a lot nicer, even though I'm not aware of one, just saying :wink:

Last updated: Jul 15 2024 at 21:02 UTC