Parser Expression Grammars (PVS and Lean comparison)

Stream: lean4

[Joe Hendrix]

As an exercise to learn Parsing expression grammars (PEGs), I formalized them along with a notion of "proofs of parse" in both Lean and PVS (repo here). PEGs are rough context-free grammars with deterministic choice and a lookahead primitives.

I prove parsing is deterministic. The proofs were pretty similar, but the PVS was shorter due to some of the tactics in PVS. assert, flatten and grind were all useful. The Lean 4 VSCode interface got a little slow at times too while the PVS VScode integration has a modal proof interface and seemed to perform more consistently.

It's been a while since I've done proving in Lean, so I thought I'd share a link to the Lean file and see if others have suggestions for better tactics. The PVS is here and better documented, but you need either PVS or the VSCode plugin to view the proof.

[Mario Carneiro]

I find it difficult to compare PVS proofs to lean (or anything else, really) since the proof scripts are huge and presumably not human-written

[Joe Hendrix]

Yes, you need PVS installed to effectively read them (which I find a bit annoying). The VSCode plugin works pretty well.

[Joe Hendrix]

I've attached a screen shot of the info panel showing part of the structure PVS_is_deterministic_proof.png

[James Gallicchio]

(I've nothing helpful to contribute, but this looks really cool!)

[Leonardo de Moura]

@Joe Hendrix Thanks for sharing the example. I took a quick look, and here are some possible simplifications.

• have with patterns

    have p_sub1_bound := p_def.left
    have p_sub1_nt    := p_def.right.left.left
    have p_sub1_pos   := p_def.right.left.right
    have p_def  := p_def.right.right

==>

    have ⟨p_sub1_bound, ⟨p_sub1_nt, p_sub1_pos⟩, p_def⟩ := p_def

• induction ... using

 apply @Fin.strong_induction_on _
    (λi =>
      ∀ (j : Fin q.size),
          (p i).leftnonterminal = (q j).leftnonterminal
        → (p i).position        = (q j).position
        → (p i).record_result   = (q j).record_result) i0
 intro i ind

==>

  induction i0 using Fin.strong_induction_on with
  | ind i ind =>

• by_cases + <;>

   cases Decidable.em ((p.val.getD p_sub1 (p i)).success = true) with
    | inl p_sub1_success =>
      cases Decidable.em ((q.val.getD q_sub1 q_j).success = true) with
      | inr q_sub1_fail =>
        simp [p_sub1_success, q_sub1_fail] at ind1
      | inl q_sub1_success =>
        simp [p_sub1_success, q_sub1_success] at ind1 p_def q_def
        simp [p_def, q_def, ind1]

    | inr p_sub1_fail =>
      cases Decidable.em ((q.val.getD q_sub1 q_j).success = true) with
      | inl q_sub1_success =>
        simp [p_sub1_fail, q_sub1_success] at ind1
      | inr q_sub1_fail =>
        simp [p_sub1_fail, q_sub1_fail] at ind1 p_def q_def
        simp [p_def, q_def, ind1]

==>

    by_cases (p.val.getD p_sub1 (p i)).success = true <;>
      by_cases (q.val.getD q_sub1 q_j).success = true <;>
        simp [*] at ind1 p_def q_def <;> simp [*]

[Leonardo de Moura]

The split tactic for breaking if-then-else (and match) expressions in cases also seems useful in your example.
For example, we can further simply

    by_cases (p.val.getD p_sub1 (p i)).success = true <;>
      by_cases (q.val.getD q_sub1 q_j).success = true <;>
        simp [*] at ind1 p_def q_def <;> simp [*]

==>

    split at p_def <;> split at q_def <;>
      simp [*] at p_def q_def ind1 <;> simp [*]

==>

    split at p_def <;> split at q_def <;> simp_all

[Leonardo de Moura]

We also have the checkpoint and stop tactics for reducing the elaboration time for big proofs.
See discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Partial.20evaluation.20of.20a.20file
However, you would have to re-structure your proof to take maximum advantage of them. The idiom is

... := by
checkpoint
   <expensive tactic prefix>
<part we are working on>
stop
<rest>

[Leonardo de Moura]

In the future, it would be great to have UI support to mark the part we are working on.

[Joe Hendrix]

@Leonardo de Moura Thanks for taking a look. The split tactic in particular makes the choice of predicate splits really clear. It turns out I can replace all the use of cases with split. I think that makes the proof more maintainable and clear.