Skip to content

Commit 75d247e

Browse files
claudeclaude
committed
feat(proofs): Coq port of the universal parser metatheory (Lean↔Coq parity)
WokeGrammarParser.v mirrors WokeGrammar.lean's expression-grammar proofs in Coq 8.18.0: a faithful fuel-based precedence-climbing parser + the concrete precedence/associativity/rejection battery + the universal round-trip: - prefix_rt (the parser inverts the fully-parenthesised renderer rp), - parse_closed, completeness_rp (∀ e, parseAll (rp e) = Some e), - parse_deterministic (unambiguity), rp_injective. Print Assumptions: all axiom-free ("Closed under the global context") — even cleaner than the Lean development. CI-gated via coq-proofs.yml. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL
1 parent 0b1b031 commit 75d247e

2 files changed

Lines changed: 302 additions & 0 deletions

File tree

‎.github/workflows/coq-proofs.yml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,13 @@ on:
1313
paths:
1414
- 'docs/proofs/verification/WokeLang.v'
1515
- 'docs/proofs/verification/WokeGrammarStructure.v'
16+
- 'docs/proofs/verification/WokeGrammarParser.v'
1617
- '.github/workflows/coq-proofs.yml'
1718
pull_request:
1819
paths:
1920
- 'docs/proofs/verification/WokeLang.v'
2021
- 'docs/proofs/verification/WokeGrammarStructure.v'
22+
- 'docs/proofs/verification/WokeGrammarParser.v'
2123
- '.github/workflows/coq-proofs.yml'
2224

2325
permissions:
@@ -49,3 +51,10 @@ jobs:
4951
cd docs/proofs/verification
5052
coqc WokeGrammarStructure.v
5153
echo "✅ WokeGrammarStructure.v verified"
54+
55+
- name: Verify WokeGrammarParser.v (universal parser metatheory; axiom-free)
56+
run: |
57+
set -euo pipefail
58+
cd docs/proofs/verification
59+
coqc WokeGrammarParser.v
60+
echo "✅ WokeGrammarParser.v verified"

‎docs/proofs/verification/WokeGrammarParser.v‎

Lines changed: 293 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,293 @@
1+
(*
2+
SPDX-License-Identifier: MPL-2.0
3+
Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
5+
WokeGrammarParser.v — Coq 8.18.0 port of the universal parser metatheory in
6+
WokeGrammar.lean (Lean↔Coq parity for the expression-grammar proofs). A faithful
7+
fuel-based precedence-climbing parser, with termination (totality), the concrete
8+
precedence/associativity/rejection battery, and the universal completeness
9+
round-trip `completeness_rp` via the key lemma `prefix_rt`.
10+
*)
11+
12+
Require Import List.
13+
Import ListNotations.
14+
Require Import PeanoNat.
15+
Require Import Lia.
16+
17+
Inductive BinOp := Or | And | EqB | Ne | Lt | Gt | Le | Ge | Add | Sub | Mul | DivB | ModB.
18+
Inductive UnOp := Neg | Notb.
19+
Inductive Tok :=
20+
| TNum (n:nat) | TIdent (s:nat) | TLpar | TRpar
21+
| TOr | TAnd | TEq | TNe | TLt | TGt | TLe | TGe
22+
| TPlus | TMinus | TStar | TSlash | TPercent | TNot.
23+
Inductive Expr :=
24+
| ELit (n:nat) | EVar (s:nat) | EUn (u:UnOp) (e:Expr) | EBin (op:BinOp) (l r:Expr).
25+
26+
Definition binLevel (op:BinOp) : nat :=
27+
match op with
28+
| Or => 1 | And => 2 | EqB | Ne => 3 | Lt | Gt | Le | Ge => 4
29+
| Add | Sub => 5 | Mul | DivB | ModB => 6 end.
30+
Definition unaryLevel := 7.
31+
32+
Definition tokBin (t:Tok) : option BinOp :=
33+
match t with
34+
| TOr => Some Or | TAnd => Some And | TEq => Some EqB | TNe => Some Ne
35+
| TLt => Some Lt | TGt => Some Gt | TLe => Some Le | TGe => Some Ge
36+
| TPlus => Some Add | TMinus => Some Sub | TStar => Some Mul
37+
| TSlash => Some DivB | TPercent => Some ModB | _ => None end.
38+
39+
(* Precedence-climbing parser, fuel-structural (hence total — T3.3). *)
40+
Fixpoint parsePrec (fuel minl:nat) (ts:list Tok) {struct fuel} : option (Expr * list Tok) :=
41+
match fuel with
42+
| 0 => None
43+
| S f =>
44+
match parsePrefix f ts with
45+
| None => None
46+
| Some (lhs, rest) => parseInfix f minl lhs rest
47+
end
48+
end
49+
with parseInfix (fuel minl:nat) (lhs:Expr) (ts:list Tok) {struct fuel} : option (Expr * list Tok) :=
50+
match fuel with
51+
| 0 => None
52+
| S f =>
53+
match ts with
54+
| [] => Some (lhs, [])
55+
| t :: rest =>
56+
match tokBin t with
57+
| None => Some (lhs, t :: rest)
58+
| Some op =>
59+
if Nat.ltb minl (binLevel op) then
60+
match parsePrec f (binLevel op) rest with
61+
| None => None
62+
| Some (rhs, rest') => parseInfix f minl (EBin op lhs rhs) rest'
63+
end
64+
else Some (lhs, t :: rest)
65+
end
66+
end
67+
end
68+
with parsePrefix (fuel:nat) (ts:list Tok) {struct fuel} : option (Expr * list Tok) :=
69+
match fuel with
70+
| 0 => None
71+
| S f =>
72+
match ts with
73+
| TNum n :: rest => Some (ELit n, rest)
74+
| TIdent s :: rest => Some (EVar s, rest)
75+
| TLpar :: rest =>
76+
match parsePrec f 0 rest with
77+
| Some (e, TRpar :: rest') => Some (e, rest')
78+
| _ => None
79+
end
80+
| TMinus :: rest =>
81+
match parsePrec f unaryLevel rest with
82+
| None => None
83+
| Some (e, rest') => Some (EUn Neg e, rest')
84+
end
85+
| TNot :: rest =>
86+
match parsePrec f unaryLevel rest with
87+
| None => None
88+
| Some (e, rest') => Some (EUn Notb e, rest')
89+
end
90+
| _ => None
91+
end
92+
end.
93+
94+
Definition budget (ts:list Tok) := 2 * length ts + 2.
95+
Definition parseAll (ts:list Tok) : option Expr :=
96+
match parsePrec (budget ts) 0 ts with
97+
| Some (e, []) => Some e
98+
| _ => None
99+
end.
100+
101+
(* ---- Precedence (T6.1) and associativity (T6.3): concrete checks ---- *)
102+
Example prec_mul_over_add :
103+
parseAll [TNum 1; TPlus; TNum 2; TStar; TNum 3]
104+
= Some (EBin Add (ELit 1) (EBin Mul (ELit 2) (ELit 3))).
105+
Proof. vm_compute. reflexivity. Qed.
106+
107+
Example prec_add_after_mul :
108+
parseAll [TNum 1; TStar; TNum 2; TPlus; TNum 3]
109+
= Some (EBin Add (EBin Mul (ELit 1) (ELit 2)) (ELit 3)).
110+
Proof. vm_compute. reflexivity. Qed.
111+
112+
Example assoc_sub_left :
113+
parseAll [TNum 1; TMinus; TNum 2; TMinus; TNum 3]
114+
= Some (EBin Sub (EBin Sub (ELit 1) (ELit 2)) (ELit 3)).
115+
Proof. vm_compute. reflexivity. Qed.
116+
117+
Example grouping_overrides :
118+
parseAll [TLpar; TNum 1; TPlus; TNum 2; TRpar; TStar; TNum 3]
119+
= Some (EBin Mul (EBin Add (ELit 1) (ELit 2)) (ELit 3)).
120+
Proof. vm_compute. reflexivity. Qed.
121+
122+
Example full_ladder :
123+
parseAll [TNum 1; TOr; TNum 2; TAnd; TNum 3; TEq; TNum 4; TLt;
124+
TNum 5; TPlus; TNum 6; TStar; TNum 7]
125+
= Some (EBin Or (ELit 1)
126+
(EBin And (ELit 2)
127+
(EBin EqB (ELit 3)
128+
(EBin Lt (ELit 4)
129+
(EBin Add (ELit 5) (EBin Mul (ELit 6) (ELit 7))))))).
130+
Proof. vm_compute. reflexivity. Qed.
131+
132+
Example unary_tighter :
133+
parseAll [TMinus; TNum 2; TStar; TNum 3]
134+
= Some (EBin Mul (EUn Neg (ELit 2)) (ELit 3)).
135+
Proof. vm_compute. reflexivity. Qed.
136+
137+
(* ---- Rejection battery (T3.1, no over-acceptance) ---- *)
138+
Example rej_lead_op : parseAll [TPlus; TNum 1] = None.
139+
Proof. vm_compute. reflexivity. Qed.
140+
Example rej_two_atoms : parseAll [TNum 1; TNum 2] = None.
141+
Proof. vm_compute. reflexivity. Qed.
142+
Example rej_trail_op : parseAll [TNum 1; TPlus] = None.
143+
Proof. vm_compute. reflexivity. Qed.
144+
Example rej_unclosed : parseAll [TLpar; TNum 1] = None.
145+
Proof. vm_compute. reflexivity. Qed.
146+
Example rej_extra_rpar : parseAll [TLpar; TNum 1; TRpar; TRpar] = None.
147+
Proof. vm_compute. reflexivity. Qed.
148+
Example rej_empty : parseAll [] = None.
149+
Proof. vm_compute. reflexivity. Qed.
150+
151+
(* ===== Universal metatheory: completeness + unambiguity ===== *)
152+
153+
Definition opTok (op:BinOp) : Tok :=
154+
match op with
155+
| Or => TOr | And => TAnd | EqB => TEq | Ne => TNe | Lt => TLt | Gt => TGt
156+
| Le => TLe | Ge => TGe | Add => TPlus | Sub => TMinus | Mul => TStar
157+
| DivB => TSlash | ModB => TPercent end.
158+
159+
Lemma tokBin_opTok : forall op, tokBin (opTok op) = Some op.
160+
Proof. destruct op; reflexivity. Qed.
161+
162+
Lemma binLevel_pos : forall op, Nat.ltb 0 (binLevel op) = true.
163+
Proof. destruct op; reflexivity. Qed.
164+
165+
Fixpoint rp (e:Expr) : list Tok :=
166+
match e with
167+
| ELit n => [TNum n]
168+
| EVar s => [TIdent s]
169+
| EUn Neg e => [TLpar; TMinus] ++ rp e ++ [TRpar]
170+
| EUn Notb e => [TLpar; TNot] ++ rp e ++ [TRpar]
171+
| EBin op l r => [TLpar] ++ rp l ++ [opTok op] ++ rp r ++ [TRpar]
172+
end.
173+
174+
Lemma rp_len_pos : forall e, 1 <= length (rp e).
175+
Proof. intros e; destruct e; try destruct u; simpl; lia. Qed.
176+
177+
(* One-step unfold equations (definitional). *)
178+
Lemma u_lpar : forall f rest, parsePrefix (S f) (TLpar :: rest) =
179+
match parsePrec f 0 rest with Some (e, TRpar :: r) => Some (e, r) | _ => None end.
180+
Proof. reflexivity. Qed.
181+
Lemma u_minus : forall f rest, parsePrefix (S f) (TMinus :: rest) =
182+
match parsePrec f unaryLevel rest with None => None | Some (e, r) => Some (EUn Neg e, r) end.
183+
Proof. reflexivity. Qed.
184+
Lemma u_not : forall f rest, parsePrefix (S f) (TNot :: rest) =
185+
match parsePrec f unaryLevel rest with None => None | Some (e, r) => Some (EUn Notb e, r) end.
186+
Proof. reflexivity. Qed.
187+
Lemma u_prec : forall f minl ts, parsePrec (S f) minl ts =
188+
match parsePrefix f ts with None => None | Some (lhs, rest) => parseInfix f minl lhs rest end.
189+
Proof. reflexivity. Qed.
190+
Lemma u_infix_nil : forall f minl lhs, parseInfix (S f) minl lhs [] = Some (lhs, []).
191+
Proof. reflexivity. Qed.
192+
193+
(* Key lemma: the prefix parser recovers any fully-parenthesised expression. *)
194+
Lemma prefix_rt : forall e rest F,
195+
2 * length (rp e) <= F -> parsePrefix F (rp e ++ rest) = Some (e, rest).
196+
Proof.
197+
induction e as [n|s|u e IH|op l IHl r IHr]; intros rest F HF.
198+
- (* ELit *) destruct F; simpl in HF; [lia|]. reflexivity.
199+
- (* EVar *) destruct F; simpl in HF; [lia|]. reflexivity.
200+
- (* EUn *)
201+
pose proof (rp_len_pos e) as Hpe.
202+
assert (Hlen: length (rp (EUn u e)) = 3 + length (rp e))
203+
by (destruct u; cbn [rp]; rewrite !app_length; cbn [length]; lia).
204+
rewrite Hlen in HF.
205+
do 5 (destruct F as [|F]; [lia|]).
206+
destruct u.
207+
+ (* Neg *)
208+
assert (Hnorm: rp (EUn Neg e) ++ rest = TLpar :: TMinus :: (rp e ++ TRpar :: rest)).
209+
{ cbn [rp]. rewrite <- ?app_assoc. reflexivity. }
210+
rewrite Hnorm.
211+
assert (H1: parsePrefix (S F) (rp e ++ TRpar :: rest) = Some (e, TRpar :: rest))
212+
by (apply IH; lia).
213+
assert (H3: parsePrec (S (S F)) unaryLevel (rp e ++ TRpar :: rest) = Some (e, TRpar :: rest))
214+
by (rewrite u_prec, H1; reflexivity).
215+
assert (H4: parsePrefix (S (S (S F))) (TMinus :: (rp e ++ TRpar :: rest))
216+
= Some (EUn Neg e, TRpar :: rest))
217+
by (rewrite u_minus, H3; reflexivity).
218+
assert (H6: parsePrec (S (S (S (S F)))) 0 (TMinus :: (rp e ++ TRpar :: rest))
219+
= Some (EUn Neg e, TRpar :: rest))
220+
by (rewrite u_prec, H4; reflexivity).
221+
rewrite u_lpar, H6. reflexivity.
222+
+ (* Notb *)
223+
assert (Hnorm: rp (EUn Notb e) ++ rest = TLpar :: TNot :: (rp e ++ TRpar :: rest)).
224+
{ cbn [rp]. rewrite <- ?app_assoc. reflexivity. }
225+
rewrite Hnorm.
226+
assert (H1: parsePrefix (S F) (rp e ++ TRpar :: rest) = Some (e, TRpar :: rest))
227+
by (apply IH; lia).
228+
assert (H3: parsePrec (S (S F)) unaryLevel (rp e ++ TRpar :: rest) = Some (e, TRpar :: rest))
229+
by (rewrite u_prec, H1; reflexivity).
230+
assert (H4: parsePrefix (S (S (S F))) (TNot :: (rp e ++ TRpar :: rest))
231+
= Some (EUn Notb e, TRpar :: rest))
232+
by (rewrite u_not, H3; reflexivity).
233+
assert (H6: parsePrec (S (S (S (S F)))) 0 (TNot :: (rp e ++ TRpar :: rest))
234+
= Some (EUn Notb e, TRpar :: rest))
235+
by (rewrite u_prec, H4; reflexivity).
236+
rewrite u_lpar, H6. reflexivity.
237+
- (* EBin *)
238+
pose proof (rp_len_pos l) as Hpl. pose proof (rp_len_pos r) as Hpr.
239+
assert (Hlen: length (rp (EBin op l r)) = 3 + length (rp l) + length (rp r))
240+
by (cbn [rp]; rewrite !app_length; cbn [length]; lia).
241+
rewrite Hlen in HF.
242+
do 5 (destruct F as [|F]; [lia|]).
243+
assert (Hnorm: rp (EBin op l r) ++ rest
244+
= TLpar :: (rp l ++ opTok op :: (rp r ++ TRpar :: rest))).
245+
{ cbn [rp]. rewrite <- ?app_assoc. reflexivity. }
246+
rewrite Hnorm.
247+
assert (HR: parsePrefix (S F) (rp r ++ TRpar :: rest) = Some (r, TRpar :: rest))
248+
by (apply IHr; lia).
249+
assert (HRp: parsePrec (S (S F)) (binLevel op) (rp r ++ TRpar :: rest)
250+
= Some (r, TRpar :: rest))
251+
by (rewrite u_prec, HR; reflexivity).
252+
assert (HL: parsePrefix (S (S (S F))) (rp l ++ opTok op :: (rp r ++ TRpar :: rest))
253+
= Some (l, opTok op :: (rp r ++ TRpar :: rest)))
254+
by (apply IHl; lia).
255+
assert (HLi: parseInfix (S (S (S F))) 0 l (opTok op :: (rp r ++ TRpar :: rest))
256+
= Some (EBin op l r, TRpar :: rest)).
257+
{ cbn [parseInfix]. rewrite tokBin_opTok. simpl Nat.ltb. rewrite binLevel_pos.
258+
rewrite HRp. reflexivity. }
259+
assert (HLp: parsePrec (S (S (S (S F)))) 0 (rp l ++ opTok op :: (rp r ++ TRpar :: rest))
260+
= Some (EBin op l r, TRpar :: rest))
261+
by (rewrite u_prec, HL; exact HLi).
262+
rewrite u_lpar, HLp. reflexivity.
263+
Qed.
264+
265+
Lemma parse_closed : forall e F, 2 * length (rp e) + 2 <= F -> parsePrec F 0 (rp e) = Some (e, []).
266+
Proof.
267+
intros e F HF. pose proof (rp_len_pos e).
268+
destruct F as [|[|F]]; try lia.
269+
assert (Hp: parsePrefix (S F) (rp e) = Some (e, [])).
270+
{ pose proof (prefix_rt e [] (S F)) as Hpr. rewrite app_nil_r in Hpr. apply Hpr. lia. }
271+
rewrite u_prec, Hp. apply u_infix_nil.
272+
Qed.
273+
274+
(* T3.2 completeness (universal): every expression's concrete syntax parses back. *)
275+
Theorem completeness_rp : forall e, parseAll (rp e) = Some e.
276+
Proof.
277+
intros e. unfold parseAll. rewrite (parse_closed e (budget (rp e))).
278+
- reflexivity.
279+
- unfold budget. lia.
280+
Qed.
281+
282+
(* T2.2 unambiguity: the parser is a function. *)
283+
Theorem parse_deterministic : forall ts e1 e2,
284+
parseAll ts = Some e1 -> parseAll ts = Some e2 -> e1 = e2.
285+
Proof. intros ts e1 e2 H1 H2. rewrite H1 in H2. injection H2; auto. Qed.
286+
287+
(* Distinct expressions have distinct concrete forms (via the parser). *)
288+
Theorem rp_injective : forall a b, rp a = rp b -> a = b.
289+
Proof.
290+
intros a b H.
291+
assert (He: parseAll (rp a) = parseAll (rp b)) by (rewrite H; reflexivity).
292+
rewrite !completeness_rp in He. injection He; auto.
293+
Qed.

0 commit comments

Comments
 (0)