Zulip Chat Archive

Stream: new members

Topic: Self help during proofs

Trevor Fancher (Sep 05 2021 at 17:57):

During a proof, one of my hypothesis has a ⟨R, hR⟩.val term. I don't know what that means or how to work with it. While specific help on this would be nice, I am looking for more general help on how I could find out during a proof (in tactic mode) on how I could figure out what such things mean and how to deal with them. Some tips along the lines of how to do "printf style debugging" when in tactic mode is what I'm after. Thanks in advance.

Ruben Van de Velde (Sep 05 2021 at 17:58):

You can click on the term in the widget

Johan Commelin (Sep 05 2021 at 17:58):

@Trevor Fancher Are you using VScode? Because you can click on things in the goal view to explore them.

Eric Rodriguez (Sep 05 2021 at 18:00):

fwiw, usually try dsimp first if you don't get the tactic state. that simplifies things up to definitional equality, and so will actually turn that into just R.

Trevor Fancher (Sep 05 2021 at 18:01):

I am using VSCode. I didn't realize clicking on things let me dig around like that. Thats really neat!

Trevor Fancher (Sep 05 2021 at 18:02):

That certainly will change how I explore during proofs :)

Kevin Buzzard (Sep 05 2021 at 18:44):

Your pointy bracket R, hR term will surely be an insurance of a structure with two fields, one called val (which will presumably be R) and one called something else (which will be hR). As Eric says, you can probably use dsimp to tidy up, but note that sometimes you can then finish the proof and delete the dsimp because all it does is changes things to definitionally equal but easier-to-read things

Last updated: Dec 20 2023 at 11:08 UTC