Is it possible to do rw and simp in term mode?

Stream: new members

[Ching-Tsun Chou]

Is it possible to transform a term using rw and/or simp in term mode? I need to construct a function in which I want to use Fintype.card_coe to simplify a term.

[Aaron Liu]

You can enter tactic mode with by, then rw or simp and go back to term mode with exact, but I don't recommend it. These tactics are not meant to generate data, and you could have a bad time proving stuff about your function. There are better ways, depending on what exactly you want to rewrite. For example, docs#Fin.cast lets you rewrite the argument of a Fin without introducing Eq.mpr into your function definition at the term level.

[Matt Diamond]

also remember that every equality h is also two functions, one forward (h.mp) and one backward (h.mpr)... you don't need to rewrite to take advantage of an equality

[Ching-Tsun Chou]

The term I want to rewrite is a subterm of a bigger term

[Aaron Liu]

What is the type you are performing the rewrite in?

[Aaron Liu]

This would be much easier if you give a #mwe

[Aaron Liu]

Then I wouldn't have to ask so many questions

[Ching-Tsun Chou]

I'm trying to fix the failures on lines 100 and 107 of LeanCamCombi/ProbLYM.lean at this branch:
https://github.com/YaelDillies/LeanCamCombi/tree/personal/ctchou/prob-lym-OLD-1
Note, however, that I may decide to work around the problem rather than meeting it head-on.

[Ching-Tsun Chou]

The failures are caused by changing the definition of NumberingOn on line 46. (The old definition is on the following, commented out line.) The crux of the problem is this: Previously NumberingOn s is definitionally equal to {x // x ∈ s} ≃ Fin s.card. Now it is definitionally equal to {x // x ∈ s} ≃ Fin (Fintype.card { x // x ∈ s}). In the tactic mode, I can just rw or simp using the theorem Fintype.card_coe. (The top commit of the branch shows some fixes I was able to make this way.). But everything becomes a pain in the term mode.

[Aaron Liu]

Just docs#Equiv.trans with docs#finCongr.

[Ching-Tsun Chou]

I think I'm going to prove the equivalence of the old and new definitions at the top level and reuse the old code, rather than fixing each failure separately. The term mode is too painful to work with and very hard to read.

[suhr]

You can use eq ▸ t to rewrite t by eq in term mode.

[suhr]

If a relation is transitive, you can use calc to chain it.

The term mode is too painful to work with and very hard to read.

The term mode is perfectly fine if you know how to use it. I would prefer it over tactic mode if there was a term mode version of refine.

[Aaron Liu]

I think it's fine to use refine to create data too, it isn't doing anything too complicated and what you type is what you get.

[Yaël Dillies]

suhr said:

I would prefer it over tactic mode if there was a term mode version of refine.

The term-mode version of refine is... term-mode. I'm not sure I understand what you mean

[suhr]

Here's an example of a lemma using refine:

def lt_wf (n: Nat): Acc Nat.lt n := by
  refine n.recOn (Acc.intro 0 ?_) ?_
  · intro y (h: y < 0)
    exact absurd h (not_succ_le_zero y)
  · intro n (an: Acc Nat.lt n)
    suffices ih: ∀m, m < n.succ → Acc Nat.lt m from Acc.intro n.succ ih
    intro m h
    have elt: m = n ∨ m < n := eq_or_lt_of_le (le_of_succ_le_succ h)
    exact elt.elim
      (λ(e: m = n) => e.symm ▸ an)
      (λ(l: m < n) => Acc.inv an l)

This is what a term-mode refine would look like:

def lt_wf (n: Nat): Acc Nat.lt n :=
  refine n.recOn (Acc.intro 0 g1) g2 with
  | g1 => λy (h: y < 0) =>
    absurd h (not_succ_le_zero y)
  | g2 => λn (an: Acc Nat.lt n) =>
    suffices ih: ∀m, m < n.succ → Acc Nat.lt m from Acc.intro n.succ ih
    λm h =>
      have elt: m = n ∨ m < n := eq_or_lt_of_le (le_of_succ_le_succ h)
      elt.elim
        (λ(e: m = n) => e.symm ▸ an)
        (λ(l: m < n) => Acc.inv an l)

refine can produce many goals, so you need a syntax that allows to specify several values.

[suhr]

Some languages like Haskell or Agda have where expressions, which work essentially the same way.

[Ruben Van de Velde]

Lean has where expressions

[Kyle Miller]

import Mathlib

open Nat

def lt_wf (n: Nat): Acc Nat.lt n :=
  n.recOn (Acc.intro 0 g1) g2
where
  g1 := λy (h: y < 0) =>
    absurd h (not_succ_le_zero y)
  g2 := λn (an: Acc Nat.lt n) =>
    suffices ih: ∀m, m < n.succ → Acc Nat.lt m from Acc.intro n.succ ih
    λm h =>
      have elt: m = n ∨ m < n := eq_or_lt_of_le (le_of_succ_le_succ h)
      elt.elim
        (λ(e: m = n) => e.symm ▸ an)
        (λ(l: m < n) => Acc.inv an l)

[suhr]

Oh, that's nice. Is where a part of def or you can use it freely in any expression?

[Kyle Miller]

It's part of def/theorem

[Kyle Miller]

This is syntax sugar for let rec

[suhr]

Which makes it much less useful unfortunately, since you can't do nesting. For example, this does not work:

example: Nat := a + a
where
  a := b + b
  where
    b := 3

[Aaron Liu]

Does this work for you?

example: Nat := a + a
where
  a := b + b
  b := 3

[suhr]

Not quite, since nesting is essential for a complex proof. where in Lean is just not as flexible as refine.