Plecra

Stream: new members

[Plecra]

Heya! I'm just starting to get into lean, have got through a few of the natural number/set theory games, here looking for help learning some details that I'm struggling with.
I'm particularly interested in separation logics and am aiming to get my own version of a system like HTT running soon to poke at and tweak - the end goal is putting together my own take on user-friendly dependent session protocols.

[Plecra]

I'm trying to use cases at the moment - I've got an inductive type, and I want to case split on v = Variant1 | v = Variant2 - but the tactic immediately substitutes the equality into the goal, then doesnt add the hypothesis to the context. For my own sake, I'd like to be able to name that hypothesis and keep it around to help me keep track of which state I'm in - is there a way to insist to cases that the hypothesis is given a name?

[Markus Himmel]

If you hover over cases in your editor, the docstring will tell you

cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

An example:

example {n : Nat} : n = 0 ∨ 1 ≤ n := by
  cases h : n with
  | zero =>
    -- `h : n = 0`
    simp
  | succ m =>
    -- `h : n = m + 1`
    simp

[Plecra]

right. I'm using the unstructured cases', I've got quite a bit of nesting so the automatic structure is handy, and I couldnt figure out how to get the same behaviour

[Markus Himmel]

cases' supports the same syntax. I'm not sure what you mean by "automatic structure", if you could share some code it might be possible to figure out whether what you want can also be achieved using cases.

[Plecra]

ah, fantastic thankyou :) I must have confused myself at some point

[Plecra]

https://gist.github.com/Plecra/ef1c2301f8a2fefc5626949fbbb1afc2
it's not particularly concise I'm afraid, but here's the project I'm on atm. checking a parse rule against the behaviour I want. I'm sure there're plenty of ways it can be really improved - all notes are very welcome :)

Atm have got stuck on unfolding - I want to unfold LE.le just once, but I'm only finding docs for lean 3's unfold1

[Plecra]

ooh this does the trick for now

theorem le_indentation_iff_le : .Indentation m ≤ Whitespace.Indentation n ↔ m ≤ n := by
  -- LE.le is automatically unfolded, but the transparency rules ig?
  unfold instPreorderWhitespace
  simp

[Michael Rothgang]

Does this work?

theorem le_indentation_iff_le : .Indentation m ≤ Whitespace.Indentation n ↔ m ≤ n := by
`simp [(· ≤ ·)]`

[Plecra]

no, it doesnt. Actual error is that it hits the recursion limit.

The trouble I was having before was that unfolding LE.le also unfolded m <= n to its typeclass instance, which then wasnt equivalent to the instance of le for Whitespace

[Aaron Liu]

You should write an "unfolding lemma" for LE on whitespace

[Plecra]

I did it! https://gist.github.com/Plecra/6771b592feba551dc5bd6299df518846 :) The main result is "yep2"
wasnt at all sure if it was even true so it's great to have this shown, will be using the implementation now

[Plecra]

Aaron Liu said:

You should write an "unfolding lemma" for LE on whitespace

that makes sense! Can definitely have that in mind for isolating single steps next time

[Plecra]

If anyone would, I'd really appreciate some guidance on how to improve the quality of the proof ^^ Making it shorter/more understandable/less redundant.
I think I'll try going through it myself and see what I can clean up now it's done, but I can't tell how far I am from a 'good' version of it yet

[Plecra]

woah, adding @[simp] lemmas is really powerful lmao

[Plecra]

https://gist.github.com/Plecra/ce89d698401547ef59236d00094a96eb
quite a lot better now~ almost halved the length of the main proof itself, gave everything better names, switched to some clearer definitions

[Plecra]

Translated it to automation using a few iterations of split/simp/grind, much simpler to write :D