Remi (Feb 11 2024 at 15:23): Remi (Feb 11 2024 at 15:23):I have parser combinators theory that I'm currently writing. For every parser combinator I need to prove that it does not produce any new input if it succeeded. And for most of them proofs were trivial, except one.
many combinator takes in another parser, which is guaranteed to eat input, which is why I was able to prove that this function is terminated, but I couldn’t prove that it does not produce input.
At first I tried to prove it by contradiction, but that didn’t lead me anywhere. Next, I thought that induction could help me, but the inductive rule that Isabelle itself derived turned out to be of little use, since it did not reflect recursion. Attempts to formulate it myself also did not lead me anywhere, although this does not mean that it cannot be formulated.
Next, I decided to try to model it through the proof of the following statement "∃n. many'_raw p i = repeated_raw n (run_greedy p) i". From it I was able to deduce that many does not produce input, but couldn't prove statement itself.
Can you give any advice on how to approach the proof? I need to prove either many'_raw_repeated_relation or many'_raw_is_parser.
Here's the code.
Mathias Fleury (Feb 11 2024 at 15:46):which library are you importing? (which return?)
Remi (Feb 11 2024 at 15:55):Mathias Fleury said:
which library are you importing? (which return?)
It's from Certification_Monads.Error_Monad, but those return and error are just abbreviations to Inr and Inl.
Remi (Feb 11 2024 at 16:13):Mathias Fleury said:
which library are you importing? (which return?)
Sorry, haven't tested code, it apparently not working, and you'll need full file. It just requires AFP to be installed.
Mathias Fleury (Feb 11 2024 at 16:17):I have the AFP, I just needed the import :-)
Mathias Fleury (Feb 12 2024 at 06:50):What do you mean with does not respect the structure? A tried for a while and got:
lemma
"\<exists>n. many'_raw p i = repeated_raw n (run_greedy p) i"
apply (induction i arbitrary: p)
subgoal for p
apply (auto split: if_splits simp: sum.case_eq_if pure_raw_def)
apply (cases "run_greedy p []")
apply (rule exI[of _ 0])
apply (auto split: if_splits simp: sum.case_eq_if pure_raw_def)[2]
by (metis (no_types, lifting) greedy_parser_def list.size(3) mem_Collect_eq mem_case_prodE mem_case_prodI2 run_greedy sum.collapse(2) zero_order(3))
subgoal for a i p
apply (rule exI[of _ "Suc _"]) (*actually Suc n where n is coming from IH*)
apply (auto split: if_splits simp: sum.case_eq_if pure_raw_def map_raw_def)
(I was too lazy to go one, because I did not understand why I do not get a run_greedy p (a # i) out of the goal)
Mathias Fleury (Feb 12 2024 at 06:51):but I might also be missing something here
Remi (Feb 12 2024 at 12:03):@Mathias Fleury Didn't understand your question.
I nitpicked goal and it found counterexample. So this lemma about relation between many'_raw and repeated_raw is poorly formulated.
But that goal now auxulary, as @Mikhail Mandrykin wrote proof for main lemma is_parser (many'_raw)!
lemma "is_parser (many'_raw p)" unfolding is_parser_def proof (rule allI)
show "∀r v. many'_raw p i = Inr (r, v) ⟶ length r ≤ length i" for i proof (induct rule: many'_raw.induct)
case (1 xs) thus ?case using run_greedy
by (subst many'_raw.simps) (fastforce split: sum.splits simp del: many'_raw.simps)
qed
qed
@Mathias Fleury Thanks for help, and wonderful isabelle-emacs!
Last updated: Apr 28 2024 at 12:28 UTC