Paper-Proof/paperproof

Some notes

Closed this issue · 2 comments

lakesare commented

[Some notes that we could forget if we don't write them down]

UPDATE: done, top vs bottom rendering is added to instructions

  • It is not super obvious to the new user that the arrows from goals to goals have ↑ direction, and the arrows from hypotheses to hypotheses have ↓ direction. That you are supposed to read the proof "from the outside in" (rather than top-down, or bottom-up).
    We should probably insert a gif/[pic with arrows] in the readme at some point about this (I'm writing this down because I already think it's obvious, and of course it isn't). A gif that shows us typing in some proof with the tree appearing on the right should work as such demonstration, bc will show how hypotheses appear from the top, and goals appear from the bottom.
image
lakesare commented
  • There is a question of how we want to handle weirdSituation where the hypothesis changes, but its type or username do not change. We might want to create fakeIds. Atm we're just changing it in-place:
image

This happens sorta frequently (e.g. during the rename tactics; or when some hypothesis gets tomstoned) for hypotheses, and we never saw it happening for the goals yet; but it's possible to create an artificial situation where that would happen with hypotheses, too. This leads to the creator tactic appearing on top of one of the goals instead of trivial. So, if we end up creating fake ids, we might want to create them for the goals too while we're at it.

elab "creator " : tactic => do
  let goal ← Lean.Elab.Tactic.getMainGoal

  let hi    ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat [])    (userName := `hi)
  let hello ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `hello)
  let wow   ← Lean.Meta.mkFreshExprMVar (Expr.const `Int [])    (userName := `wow)

  Lean.Elab.Tactic.setGoals [hi.mvarId!, hello.mvarId!, goal, wow.mvarId!]

theorem very_easy : true := by
  creator
  exact 5
  exact "hello"
  trivial
  exact 7
image

AND also: how about instead of creating fakeIds data structure we just turn all ids into a triple fvarid-username-type.
fakeIds + equivalentIds + [id as a node id] === equivalentIds + [fvarid-username-type as a node id].

lakesare commented

UPDATE: done, Anton made it render nicely

I'm noticing a lot of proofs in mathlib with induction where induction hab forks into 6 or so hypotheses, which correspondingly gives us 6+ arrows, one more reason to unite hypothesis under 1 tactic node in such cases.

Here's church_rosser proof e.g:
image
image