feat: add more tactic examples and documentation

[jcreedcmu]

No description provided.

[david-christiansen]

Do we want to call out implication here?

It seems to me that centering function types is the wrong way to present this, and that it'd be better to lead with universal quantifiers, then implications; we're not really in the business of producing computable functions with tactics, but it's fine to have that as the third alternative.

[jcreedcmu]

Ah, agree that centering the propositional angle is better.

[david-christiansen]

This should mention hygiene (it's really the binder's name plus macro scopes, right?)

[jcreedcmu]

I don't actually have any clear idea how intro interacts with macro scopes. Is there another section of the manual that I should be linking to?

[david-christiansen]

https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=tactic-language-hygiene

[david-christiansen]

Basically, it does the usual macro introduction thing. If the identifier occurs in the syntax that the user wrote, then it's available for reference in further things the user wrote. If the identifier was produced by metaprogram internals (including "give me a default name from this internal binder name"), then it can't be referenced from things the user wrote. And different metaprograms (and invocations of the same metaprogram) get distinct local namespaces as well, preventing painful capture issues.

[david-christiansen]

It also works for other reflexive relations. Should we center that and have an example?

[david-christiansen]

Oh, there is an example. Mention it here, perhaps?

[jcreedcmu]

Good idea!

[david-christiansen]

What about adding another reflexive relation in an example? Like:

def Univ (_ _ : α) := True

@[refl]
theorem Univ.refl (x : α) : Univ x x := True.intro

example : Univ 2 2 := by rfl

[jcreedcmu]

Good idea.

[david-christiansen]

There should also be an example of the symm attribute on a relation here.

Perhaps something like:

def Univ (_ _ : α) := True

@[symm]
theorem Univ.symm (x : α) : Univ x y → Univ y x := by
  intro; exact True.intro

example : Univ 2 3 → Univ 3 2 := by
  intro
  symm
  assumption

[jcreedcmu]

Done.

[david-christiansen]

"close" is not the verb we usually use in this manual. What about "which is unprovable"?

Also, this sentence is long. Can it be two sentences?

[jcreedcmu]

Done.

[david-christiansen]

Is "closes" the right verb?

[jcreedcmu]

Going with "prove" here.

[david-christiansen]

What about apply here, for extra oomph?

[jcreedcmu]

Sgtm.

[david-christiansen]

This could use an example.

[jcreedcmu]

Done.

[david-christiansen]

It's also nice when the proof being applied isn't just a lemma that mostly matches, but is built up with things like anonymous constructor syntax.

[david-christiansen]

This strikes me as a strange use of change, because normally I'd use rw [Not] or perhaps unfold [Not] for this kind of thing.

What about instead proving that x + 2 = 1 + x + 1 by first changeing it to x + 1 + 1 and then applying associativity? That seems similarly small, but it matches the pattern of "put it into this other form from the same defeq equivalence class that my solver can deal with"

[jcreedcmu]

Feel free to keep pushing back if you want to, but I would have found this example helpful when I was learning to know that change can let the user deliberately set the goal to exactly the defeq equivalence class representative they want to, even if there are other ways to use other tactics to get to the same endpoint. But the 2 defeq 1+1 is a fine example as well, and I'd be enthusiastic about including both.

[david-christiansen]

Both makes sense. I guess the key is that many defeq rules read like directional reduction steps (beta or delta, for instance), but defeq is an equality and change works "backwards" too.

[david-christiansen]

Or use have to create the specialized version!

[jcreedcmu]

True! Fixed.

[david-christiansen]

This also uses the rcases pattern language, right?

[jcreedcmu]

I'm not knowledgeable enough to know what is the best thing to include here to that effect textually.

[david-christiansen]

Right now, the rcases pattern language is described in the rcases docstring. This is not good - it should be described in a manual section and linked to from docstrings. I just haven't gotten to it yet. It would be really useful to extract that to a section that all these can xref.

[david-christiansen]

We actually don't get a lot into unification in these docs. It might be nice to unpack this a bit to increase accessibility for those not well-versed in PL implementation.

[jcreedcmu]

I currently feel like that's another topic out of scope of "improve tactic documentation".

[david-christiansen]

I mean "unpack" as in "use a few more words so this can make sense to nonexperts", not "fully define unification". Like "the proposed goal is matched against available goals modulo defeq and assigning of metas/holes", and then include an example that actually demonstrates this.

[david-christiansen]

If unification is important here then we should have an example that uses it more obviously.

[jcreedcmu]

I also feel here this is a thing that would be an improvement in general but I'd prefer to keep it out of the scope of this PR.

[david-christiansen]

I think this example is sufficient to demonstrate the key principles:

example : 1 ≠ 2 ∧ "two" ≠ "three" := by
  constructor
  show "two" = _ → False

Is that really too much for the PR? It demonstrates that the matching is modulo defeq (because inequality is unfolded to negation, and that to implication) and holes (because _ replaces "three")

[david-christiansen]

I don't think that's what extensionality means. Rather, it means that two terms are equal if they denote the same underlying mathematical object, right? So eta is a kind of extensional equality, and funext is a more general form, but that's because the mathematical community considers "maps equal elements of the domain to equal elements of the range" to be what it means for two functions to be equal. Similarly, we could create a quotient that collapses Nat into even and odd equivalence classes, and extensionality for that type would be precisely this equivalence class. "Nothing can distinguish them means they're equal" is another way to understand it, which I think makes most sense as an intuition here. That captures funext, but also principles like Array.ext that says that the arrays have the same size and assign equal valid indices to equal values, or structure ext theorems that are propositional versions of structure eta.

[david-christiansen]

Logical equivalence is also extensional equality for Prop, as witnessed by propext. That definitely doesn't fit "built from the same components" - (2 = 2) = True is a theorem of Lean, for example.

[jcreedcmu]

Hm here I agree that my wording is insufficent to cover propext, but I do like offering an intuition that works for some cases. Will try to reword...

[jcreedcmu]

I think appealing to Leibniz equality is too tautologous to really feel to me like it's about extensionality. A beta-reduced term has all the properties of the beta-redex, but the reason they are equal is via beta-reduction, not via eta.

[jcreedcmu]

How about: "Extensionality properties say that two objects are equal if they are equal under all appropriate observations.
For example, two functions are equal if they return the same value on every input and two pairs are equal if their components are equal."

For me, "appropriate" is doing a lot of work in that sentence, and that's ok :-)
I think this phrasing apples to Array.ext and propext, but I'm also ok with those example being silent.

[david-christiansen]

Well, they're intensionally equal due to beta, but they can be extensionally equal as well due to something like funext or propext or the eta-rule for unit-like types. We can prove that id () = () by appeal to rfl and thus defeq via delta and beta, but we can also prove it via something like Unit.ext (x : Unit) x = () (which we have definitionally in Lean too, but pretend we don't for a moment!) or its Subsingleton instance.

I think Leibnitz equality is not really the same here, right? I use Leibnitz equality to mean roughly "indistinguishable things are equal", that is,

def LEq (x y : a) : Prop := forall P : a -> Prop, P x = Py

whereas extensional equality is something defined per-type that allows us to prove Eq, of the form forall x y : a, EQS x y -> x = y where EQS is some telescope of equalities of x and y in various contexts. This is usually related to/inspired by the intended semantics of the type in the standard Lean model, so funext captures set-theoretic extensional equality of functions, propext captures the fact that there's classically only really two propositions, ext for a structure captures that it's basically just a product, etc.

[david-christiansen]

Our comments crossed :-) I think the "all appropriate observations" is a fine way to describe it for this context.

[david-christiansen]

This should cross-reference the funext section of the quotients chapter

[david-christiansen]

Technically it uses the registered cases eliminator, which for most types is just what you're specifying here. But it doesn't have to be - Nat has a special one that rephrases goals in terms of 0 and n + 1 instead of Nat.zero and Nat.succ n.

You can see this in action with this example:

def Bool' := { n : Nat // n = 0 ∨ n = 1 }

@[match_pattern] def Bool'.true : Bool' := ⟨1, by grind⟩
@[match_pattern] def Bool'.false : Bool' := ⟨0, by grind⟩ 
def Bool'.and : Bool' → Bool' → Bool'
  | .true, .true => .true
  | _, _ => .false

@[cases_eliminator]
def Bool'.cases {motive : Bool' → Sort u} (f : motive .false) (t : motive .true) (b : Bool') : motive b := by
  let ⟨n, ok⟩ := b
  match n with
  | 0 => exact f
  | 1 => exact t

example : Bool'.and x y = .true → x = .true ∧ y = .true := by
  cases x <;> cases y <;> simp [Bool'.and]

Bool' clearly has only one constructor, but cases x and cases y follow Bool'.cases in creating two cases. What's really going on is that it's creating one proof goal for each minor premise of the registered cases_eliminator, which by default is the one generated by the inductive machinery from the recursor but doesn't need to be.

[david-christiansen]

It's important here that the rcases pattern language is not the same one used by match, let, etc.

[david-christiansen]

This can also be rigged up to use a custom eliminator.

[david-christiansen]

This is technically not following the rules you state above, because it's phrasing the goal in simp normal form instead of in terms of constructors. This is accomplished by having a custom induction_eliminator set up for Nat.

Perhaps List is a better example?

[david-christiansen]

(it's good to at least mention the custom eliminator here for attentive readers)

[david-christiansen]

These subgoals include hypotheses that rule out the control-flow branches not taken, which means they preserve the "first match wins" semantics of match. This is crucial.

[david-christiansen]

There should be a first-match-wins example here. Something like:

def classify (n : Nat) : Option String :=
  match n with
  | 7 => some "seven"
  | 12 => some "twelve"
  | _ => none

Using spliton that will result in goals that include hypotheses that 7 and 12 were not matched. This is a big part of the value of split.

[jcreedcmu]

I can do this but I don't know the canonical way to get names for these hypotheses. If split with is a thing, it seems to only be a mathlib thing. I can use next but I'm not stoked about using it so.

When splitting a case match, hypotheses are available that show that previous arms of the case did not match.
````lean
def classify (n : Nat) : Option String :=
  match n with
  | 7 => some "seven"
  | 12 => some "twelve"
  | _ => none

example (n : Nat) :
    classify n = some "seven" ∨ classify n = some "twelve" ∨
      (n ≠ 7 ∧ n ≠ 12) := by
  unfold classify
  split
  · left; rfl
  · right; left; rfl
  · right; right; next hx hy => refine ⟨hx, hy⟩

[david-christiansen]

You can name them yourself with rename_i. But I think it's sufficient to state the proposition in the hypothesis without giving it a name here, like:

In the second case, split inserts the hypothesis n \ne 7 to indicate that the first case in classify was not taken. In the third case, it inserts both n \ne 7 and n \ne 12, indicating that neither the first nor the second case matched.

[david-christiansen]

Usually we say "is true" for a proposition. "holds" isn't wrong, but sometimes it's useful to reserve that for metalanguage statements (ie judgments). In any case, consistency of terminology is useful.

[jcreedcmu]

Sure, happy to change.

[david-christiansen]

Why is that so bad? grind and other automation does just fine with inaccessible hypothesis names.

An xref to tactic hygiene here would be useful.

[jcreedcmu]

Ok, I'm happy to soften the wording.

[jcreedcmu]

I don't really understand why tactic hygiene is relevant here? This isn't challenging the relevance so much as confessing I'm missing information.

[david-christiansen]

If you don't name the hypothesis, then a name is assigned automatically. Due to hygiene, that name is inaccessible, so you can't refer to it later in the proof (but automation can still use it).

[david-christiansen]

This tactic can be extended, right?

[david-christiansen]

Strictly speaking, propositional logic doesn't have a point of view :-)

[jcreedcmu]

Nor does a mountain have one, but one may speak of the point of view of the peak, no? :) In any case that's my intent here. Feel free to suggest another wording if you'd like, I'm not too attached to it.

[david-christiansen]

"goals that are sufficiently easy to prove" perhaps?

[david-christiansen]

Normally I'd use generalizing here rather than a low-level revert-then-induction dance.

[jcreedcmu]

I don't ever use revert, so I didn't have a strong notion of how to make a super unimpeachably high-quality example.

[david-christiansen]

Same here. It is a kind of low-level thing that I expect I'd only really use in a tactic macro or something. I'd just leave the example alone.

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit a16ddd3.