Zulip Chat Archive

Stream: lean4

Topic: Parser Expression Grammars (PVS and Lean comparison)


Joe Hendrix (Apr 15 2022 at 22:43):

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 (Apr 15 2022 at 22:47):

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 (Apr 15 2022 at 22:48):

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

Joe Hendrix (Apr 15 2022 at 22:52):

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

James Gallicchio (Apr 16 2022 at 00:57):

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

Leonardo de Moura (Apr 16 2022 at 13:03):

@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 (Apr 16 2022 at 13:40):

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 (Apr 16 2022 at 14:17):

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 (Apr 16 2022 at 14:19):

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

Joe Hendrix (Apr 17 2022 at 00:10):

@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.


Last updated: Dec 20 2023 at 11:08 UTC