Stream: General

Topic: Trimming proof state output

Hanno Becker (May 02 2024 at 04:03):

Hi. I'm working with very large goals contains dozens to hundreds of assumptions and very long conclusions. This makes stepping through a proof and tracking changes very tedious, since the goal window always jumps to the top upon changes, and also does not highlight changes in any way (as e.g. the Lean VS Code extension does).

Are there ways to (a) fix the goal state output to a certain position, or even (b) temporarily enter different 'goal visualization modes' which e.g. omit premises or apply any other techniques to reduce visual clutter?

Mathias Fleury (May 02 2024 at 04:51):

I have used subgoal premises p (*but you need using p*) to hide assumptions when they are very long

Mathias Fleury (May 02 2024 at 04:52):

For the first part I am not aware of any tool… I usually copy-paste it to another buffer and then use tools like git diff --no-index --word-diff to compare the outputs.

Hanno Becker (May 02 2024 at 05:02):

Thanks Mathias! Can you give a minimal example for how to use subgoal premises p? I have not come across it before.

Mathias Fleury (May 02 2024 at 05:11):

definition P :: ‹nat ⇒ bool› where
  ‹P i = True›

fun generate_assms :: ‹nat ⇒ bool› where
‹generate_assms 0 = True› |
‹generate_assms (Suc n) ⟷ P (Suc n) ∧ generate_assms n›


lemma ‹generate_assms 25 ⟹ generate_assms 40›
  apply (auto simp: numeral_eq_Suc) (*just making sure we have many assumptions*)
  subgoal (*here first goal with all assumptions*)
(*
Goal:
proof (prove)
goal (1 subgoal):
 1. ...
    P (Suc 0) ⟹
    P (Suc (Suc (Suc (Suc (Suc
    (Suc (Suc (Suc (Suc (Suc
  (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc
   (Suc (Suc (Suc (Suc (Suc
 (Suc (Suc (Suc (Suc (Suc (Suc
    (Suc (Suc (Suc (Suc (Suc
  (Suc (Suc (Suc 0))))))))))))))))))))))))))))))))))))))))
*)
    sorry
  subgoal (*now we go to the next goal*)
    sorry
  subgoal premises p
    (*no premises printed only the goal ⇒ printing very fast*)
(*
Goal:
proof (prove)
goal (1 subgoal):
 1. P (Suc (Suc (Suc (Suc (Suc
    (Suc (Suc (Suc (Suc (Suc
  (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc
   (Suc (Suc (Suc (Suc (Suc
 (Suc (Suc (Suc (Suc (Suc (Suc
    (Suc (Suc (Suc (Suc (Suc
  (Suc 0))))))))))))))))))))))))))))))))))))))
*)
    using p (*if you need to use the premises*)
    sorry

Hanno Becker (May 02 2024 at 05:12):

Cool! Is subgoal premises p merely a printing tweak, or does it actually affect the proof state (e.g. shifting between facts and premises)

Hanno Becker (May 02 2024 at 05:15):

Ah, seems to be the latter...

Mathias Fleury (May 02 2024 at 05:15):

For reasons (that I believe to be "this is how you should do it" (TM)), it fixes schematic variables making them impossible to instantiate in a subgoal:

schematic_goal "?P n"
  subgoal
(*
proof (prove)
goal (1 subgoal):
 1. P n
*)

Mathias Fleury (May 02 2024 at 05:16):

using p apply - to shift back to premises

Mathias Fleury (May 02 2024 at 05:18):

I mostly use it for refinement proofs where printing take seconds

Hanno Becker (May 02 2024 at 05:18):

Hmm, interesting. I'll need to think how to apply this in my context... the tactics I'm working with expect the assumptions be present as pure premises, but maybe one can still achieve the desired debug-ability by bracketing everything with apply - and subgoal premises ..

Mathias Fleury (May 02 2024 at 05:18):

also supply [[goals_limit=1]] can limit the printing to only one goal

Mathias Fleury (May 02 2024 at 05:19):

(instead of having multiple, I sometimes use =3 to see what other goals I have, but I rarely need to go the 10 that are used by default)

Mathias Fleury (May 02 2024 at 05:21):

I would be interested in pinning the position of the output too actually (mostly for debugging while developing tactics).

Hanno Becker (May 02 2024 at 05:21):

Yes, that's a pain

Hanno Becker (May 02 2024 at 05:31):

A more hacky solution to the premise-hiding problem would be to register a print translation

Hanno Becker (May 02 2024 at 05:35):

syntax (output) "_premise_elided" :: ‹prop› ("…")
translations
  "CONST Pure.imp _premise_elided z" ↽ "CONST Pure.imp x (CONST Pure.imp y z)"

lemma ‹generate_assms 25 ⟹ generate_assms 40›
  apply (auto simp: numeral_eq_Suc) (*just making sure we have many assumptions*)

But obviously one would want to programmatically tweak this

Hanno Becker (May 02 2024 at 05:38):

Slightly cleaner:

syntax (output) "_premise_elided" :: ‹prop ⇒ prop› ("… ⟹ _")
translations
  "_premise_elided z" ↽ "CONST Pure.imp y z"
  "_premise_elided z" ↽ "_premise_elided (_premise_elided z)"

Kevin Kappelmann (May 02 2024 at 08:03):

Having more control over the proof state output seems to be a larger problem. Has this been put forward to the mailing list before?

Hanno Becker (May 03 2024 at 05:18):

I'm not aware -- might be worthwhile pinging Makarius

Last updated: Dec 21 2024 at 12:33 UTC