Proofs and casts

Stream: new members

[Nelson Elhage]

Hi folks,

I'm learning Lean, and I've been playing with the Vect type from FPiL chapter 7. I'm struggling to figure out how to prove things about expressions involving casts. Here's a minimal concrete example:

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

namespace Vect

def head : (v : Vect α (Nat.succ n)) → α
  | cons a _ => a

-- If we define `append` this way, we don't need any casts
def append (lhs : Vect α m) (rhs : Vect α n) : Vect α (n + m) :=
  match lhs with
  | nil       => rhs
  | cons x xs => cons x (append xs rhs)

-- And we can easily prove a simple theorem about the interaction of
-- `head` and `append`
theorem head_append {n m : Nat} (v : Vect α (m + 1)) (rhs : Vect α n) :
  head v = head (append v rhs) := by
  cases v
  simp [head, append]

-- We could instead define `append` this way, which works, but now
-- requires a cast
def append' (lhs : Vect α m) (rhs : Vect α n) : Vect α (m + n) :=
  match lhs with
  | nil       => Nat.zero_add .. ▸ rhs
  | cons x xs => Nat.add_comm .. ▸ cons x (append xs rhs)

-- But now I get stuck with the proof
theorem head_append' {n m : Nat} (v : Vect α (m + 1)) (rhs : Vect α n) :
  head v = head (Nat.add_comm .. ▸ append' v rhs) := by
  cases v
  simp [head, append]
  -- At this point, we have a goal of the form:
  -- ⊢ a¹ =
  --     match ⋯ ▸ (cons a¹ a).append' rhs with
  --     | cons a a_1 => a
  --
  -- We're "stuck" on the cast, and I haven't figured out how to make
  -- progress.

From reading more I get the impression the usual answer is "don't do that" i.e. don't use the Vect type as defined, and instead work with something like a (l : List) paired with a proof h : len l = n. But for the sake of learning and understanding, I'm curious how to push this approach through to completion.

[Eric Wieser]

This works:

@[simp]
theorem cast_cast {m n p} (v : Vect α m) (h₁ : m = n) (h₂ : n = p) : h₂ ▸ h₁ ▸ v = (h₁.trans h₂) ▸ v := by
  cases h₁; cases h₂; rfl

theorem head_append' {n m : Nat} (v : Vect α (m + 1)) (rhs : Vect α n) :
  head v = head (Nat.add_comm .. ▸ append' v rhs) := by
  cases v
  simp [head, append']

[Eric Wieser]

Or more generally

-- I have no idea how to name this
@[simp]
theorem triangle_triangle {m n p} {F : α → Type _} (v : F m) (h₁ : m = n) (h₂ : n = p) : h₂ ▸ h₁ ▸ v = h₁.trans h₂ ▸ v := by
  cases h₁; cases h₂; rfl

[Eric Wieser]

@Kyle Miller, do you think this lemma would be a bad idea in core?

[Aaron Liu]

This is docs#cast_cast combined with docs#eqRec_eq_cast (or docs#Eq.rec_eq_cast)

[Kyle Miller]

Nelson Elhage said:

"don't do that"

Yes, don't do that, but not for the reason you're thinking. What you want is to define a Vect.cast function that's specifically for changing the length. You then use it whenever you need to deal with a definitional equality problem. You don't use the triangle operator.

There are a handful of times I've mentioned this on Zulip, but here's the last one I found via search: #Is there code for X? > ✔ noconfusion for heq @ 💬

[Kyle Miller]

Here are some exercises about Vec that I gave my students in a graduate course:

Vec exercises

import Mathlib.Tactic.Common

inductive Vec (α : Type u) : Nat → Type u where
  | nil : Vec α 0
  | cons (x : α) {n : Nat} (xs : Vec α n) : Vec α (n + 1)

variable {α : Type u}

notation "[]" => Vec.nil
infixr:67 " :: " => Vec.cons

/--
Appends `xs` to the front of `ys`.
-/
def Vec.append {m n : Nat} (xs : Vec α m) (ys : Vec α n) : Vec α (n + m):=
  match xs with
  | [] => ys
  | x :: xs' => x :: (xs'.append ys)

/-!
Note: using new notation since the `++` notation isn't good enough to make `[] ++ xs` elaborate`.
It gets stuck trying to figure out how to append `Vec ?m.22 0` and `Vec α m`, and there's sadly no mechanism
that can unify `?m.22` and `α` when `++` is heterogenous.
This `+++` operation does cause the unification to happen.
-/
infixr:65 " +++ " => Vec.append

variable {m m' n n' k k' : Nat} {xs : Vec α m} {ys : Vec α n} {zs : Vec α k}

@[simp]
theorem Vec.nil_append : [] +++ xs = xs := by
  rfl

@[simp]
theorem Vec.cons_append (x : α) :
    (x :: xs) +++ ys = x :: (xs +++ ys) := by
  rfl

/--
Updates the length of a vector using an equality.
Recall that `Vec α m` and `Vec α n` are definitionally equal iff `m` and `n` are definitionally equal.
This function can be used to patch over definitional equality issues.

**Rules:**
* In simp lemmas, casts should appear on the right-hand side, not the left-hand side.
  Exception: simp lemmas specifically about casting.
* Simp lemmas should generally try to move casts "outwards".
-/
def Vec.cast (xs : Vec α m) (h : m = n) : Vec α n :=
  h ▸ xs

@[simp]
theorem Vec.cast_rfl : xs.cast rfl = xs :=
  rfl

@[simp]
theorem Vec.cast_cast {h : m = n} {h' : n = k} : (xs.cast h).cast h' = xs.cast (h.trans h') := by
  subst_vars
  rfl

theorem Vec.cast_eq_symm {h : m = n} : xs.cast h = ys ↔ xs = ys.cast h.symm := by
  subst_vars
  rfl

-- Hint: copy the above proof!
@[simp]
theorem Vec.cons_cast {x : α} {h : m = n} :
    x :: Vec.cast xs h = (x :: xs).cast (by rw [h]) := by
  sorry

/-!
Think: Why is there no cast theorem for `Vec.nil`?
-/

@[simp]
theorem Vec.append_cast_left {h : m = m'} :
    xs.cast h +++ ys = (xs +++ ys).cast (by rw [h]) := by
  sorry

@[simp]
theorem Vec.append_cast_right {h : n = n'} :
    xs +++ ys.cast h = (xs +++ ys).cast (by rw [h]) := by
  sorry

-- Fix this theorem statement by adding a cast to the right-hand side.
@[simp]
theorem Vec.append_nil :
    xs +++ [] = xs := by
  sorry

-- Same: first fix the theorem statement.
theorem Vec.append_assoc :
    (xs +++ ys) +++ zs = xs +++ (ys +++ zs) := by
  sorry

-- We need two append lemmas since the RHSs have casts.
-- You should be able to use `Vec.cast_eq_symm` to apply `Vec.append_assoc`.
theorem Vec.append_assoc' :
    xs +++ (ys +++ zs) = (xs +++ ys) +++ zs := by
  sorry

theorem Vec.cons_eq_append {x : α} :
    x :: xs = (x :: []) +++ xs := by
  sorry

/--
Reverses `xs` and appends it to `ys`.

Tail recursive.
-/
-- We need `n` to be included in the binder list so that they may vary on recursive calls.
-- With `variable` the argument is considered to be fixed.
def Vec.reverseAux {m n : Nat} (xs : Vec α m) (ys : Vec α n) : Vec α (n + m) :=
  match m, xs with
  | 0, [] => ys
  | m' + 1, x :: xs' =>
    let zs : Vec α ((n + 1) + m') := reverseAux xs' (x :: ys)
    zs.cast (by sorry)

/--
Reverses `xs`. Tail recursive.
-/
-- Fix the definition by adding a cast.
def Vec.reverse (xs : Vec α m) : Vec α m :=
  Vec.reverseAux xs []

-- It's not necessary to state `Vec.reverseAux_nil` and `Vec.reverseAux_cons` since they're
-- the equation lemmas for `Vec.reverseAux`, but why not.
theorem Vec.reverseAux_nil :
    Vec.reverseAux [] ys = ys :=
  rfl

theorem Vec.reveresAux_cons {x : α} :
    Vec.reverseAux (x :: xs) ys = (reverseAux xs (x :: ys)).cast (by sorry) :=
  rfl

@[simp]
theorem Vec.reverseAux_cast_left (h : m = m') :
    Vec.reverseAux (xs.cast h) ys = (Vec.reverseAux xs ys).cast (by sorry) := by
  sorry

@[simp]
theorem Vec.reverseAux_cast_right (h : n = n') :
    Vec.reverseAux xs (ys.cast h) = (Vec.reverseAux xs ys).cast (by sorry) := by
  sorry

@[simp]
theorem Vec.reverse_nil :
    Vec.reverse [] = ([] : Vec α 0) := by
  sorry

theorem Vec.reverseAux_eq :
    Vec.reverseAux xs ys = Vec.reverse xs +++ ys := by
  sorry

-- Fix and prove
theorem Vec.reverse_cons_append {x : α} :
    (x :: xs).reverse +++ ys = xs.reverse +++ (x :: ys) := by
  sorry

theorem Vec.reverseAux_append :
    Vec.reverseAux (xs +++ ys) zs = Vec.reverseAux ys (xs.reverse +++ zs) := by
  sorry

theorem Vec.reverse_append :
    (xs +++ ys).reverse = ys.reverse +++ xs.reverse := by
  sorry

section Count
variable [DecidableEq α]

def Vec.countAux (a : α) {m : Nat} (xs : Vec α m) (acc : Nat) : Nat :=
  match xs with
  | [] => acc
  | x :: xs' => xs'.countAux a (acc + if x = a then 1 else 0)

/-!
Helpful tactic: `split`
It looks for `if` in the goal and splits into multiple goals.

Also: `rename_i` to name the variables produced by `split`.

Also: if you give `simp` a proof or disproof of the hypothesis of an `if`,
it can apply a conditional simp lemma to simplify the `if`.
-/

def Vec.count (a : α) (xs : Vec α m) : Nat :=
  Vec.countAux a xs 0

variable {a : α}

theorem Vec.countAux_eq {acc : Nat} :
    Vec.countAux a xs acc = Vec.count a xs + acc := by
  sorry

@[simp]
theorem Vec.count_nil :
    ([] : Vec α 0).count a = 0 := by
  sorry

@[simp]
theorem Vec.count_cons_self {x : α} :
    (x :: xs).count x = xs.count x + 1 := by
  sorry

@[simp]
theorem Vec.count_cons_of_eq {x : α} (h : x = a) :
    (x :: xs).count a = xs.count a + 1 := by
  subst_vars
  simp

@[simp]
theorem Vec.count_cons_of_neq {x : α} (h : x ≠ a) :
    (x :: xs).count a = xs.count a := by
  sorry

@[simp]
theorem Vec.count_cast (h : m = m') :
    Vec.count a (xs.cast h) = Vec.count a xs := by
  sorry

-- Example of `split`
@[simp]
theorem Vec.count_cons {x : α} :
    (x :: xs).count a = xs.count a + if x = a then 1 else 0 := by
  split <;> simp [*]

theorem Vec.count_append :
    (xs +++ ys).count a = xs.count a + ys.count a := by
  sorry

theorem Vec.length_reverseAux :
    (Vec.reverseAux xs ys).count a = xs.count a + ys.count a := by
  sorry

@[simp]
theorem Vec.count_reverse :
    xs.reverse.count a = xs.count a := by
  sorry

end Count

def Vec.map {β : Type v} (f : α → β) (xs : Vec α m) : Vec β m :=
  sorry

variable {β : Type v} {f : α → β}

/-!
For the following, you may want to develop more theorems.
-/

theorem Vec.map_map {γ : Type _} {g : β → γ} :
    (xs.map f).map g = xs.map (g ∘ f) := by
  sorry

theorem Vec.map_append :
    (xs +++ ys).map f = xs.map f +++ ys.map f := by
  sorry

theorem Vec.reverse_map :
    (xs.map f).reverse = xs.reverse.map f := by
  sorry

def Vec.countP (p : α → Bool) (xs : Vec α m) : Nat :=
  let rec go {m : Nat} (xs : Vec α m) (acc : Nat) : Nat :=
    match xs with
    | [] => acc
    | x :: xs' => go xs' (acc + if p x then 1 else 0)
  go xs 0

-- This `(... · ...)` notation is short for `fun x => (... x ...)`, for making anonymous functions.
theorem Vec.count_eq_countP [DecidableEq α] {a : α} :
    Vec.count a xs = Vec.countP (· = a) xs := by
  sorry

theorem Vec.countP_map (p : β → Bool) :
    (xs.map f).countP p = xs.countP (p ∘ f) := by
  sorry

theorem Vec.count_map [DecidableEq β] {b : β} :
    (xs.map f).count b = xs.countP (f · = b) := by
  sorry

def Vec.filterP (p : α → Bool) {m : Nat} (xs : Vec α m) : Vec α (Vec.countP p xs) :=
  match xs with
  | [] => []
  | x :: xs' =>
    if h : p x then
      (x :: xs'.filterP p).cast sorry
    else
      (xs'.filterP p).cast sorry

variable {p : α → Bool}

theorem Vec.countP_append :
    Vec.countP p (xs +++ ys) = Vec.countP p xs + Vec.countP p ys := by
  sorry

theorem Vec.filterP_append :
    Vec.filterP p (xs +++ ys)
      = (Vec.filterP p xs +++ Vec.filterP p ys).cast (by rw [Vec.countP_append, Nat.add_comm]) := by
  sorry

theorem Vec.filterP_map {p : β → Bool} {f : α → β} :
    Vec.filterP p (Vec.map f xs) = (Vec.map f (Vec.filterP (p ∘ f) xs)).cast sorry := by
  sorry

-- Isn't this `h` hypothesis a little odd?
theorem Vec.filterP_eq_self_iff_countP_eq {h : m = xs.countP p} :
    Vec.filterP p xs = xs.cast h ↔ xs.countP p = m := by
  sorry

-- A way to state the reverse:
theorem Vec.countP_eq_length_iff_filterP_eq_self :
    xs.countP p = m ↔ ∃ (h : m = xs.countP p), Vec.filterP p xs = xs.cast h := by
  sorry

theorem Vec.countP_eq_zero_iff :
    xs.countP p = 0 ↔ ∃ (h : 0 = xs.countP p), Vec.filterP p xs = [].cast h := by
  sorry

theorem Vec.countP_pos_iff_exists :
    0 < Vec.countP p xs
      ↔ ∃ (n n' : Nat) (as : Vec α n) (b : α) (cs : Vec α n') (h : n' + 1 + n = m),
          p b ∧ Vec.countP p as = 0 ∧
          xs = (as +++ (b :: cs)).cast h := by
  sorry

-- For interest, a possible relation to use when equating Vec

def Vec.eq {m n : Nat} (v : Vec α m) (w : Vec α n) : Prop :=
  ∃ h : m = n, v.cast h = w

def Vec.toList {m : Nat} (v : Vec α m) : List α := sorry

def Vec.fromList {m : Nat} (xs : List α) (h : xs.length = m) : Vec α m := sorry

[Kyle Miller]

It pushes the Vec.cast approach. Many times you can write v.cast (by omega) or something similar to have Lean figure out how to line things up when there's a mismatch.

[Nelson Elhage]

Hm, I tried using a Vect.cast approach and ran into similar challenges, but I think they're related to my next question: which is that I'm trying to understand why that cast_cast lemma helps. It doesn't let us directly get rid of the cast, but I guess simp is able to use it to add a new cast back to the original type, and then remove them, or something?

Perhaps said another way, I don't feel like I fully understand why we can't reduce the match with a cast

[Kyle Miller]

Vect.cast is superior to using the triangle because it constrains the equality to the natural number. Using triangle creates equalities between types, and these lead to many complications. Furthermore, you can write simp lemmas that state equations about Vect.cast in relation to other Vect operations.

Generally, you want to write simp lemmas that push casts 'outward' (like f v.cast = (f v).cast). Eventually they all collect at the root of the expression and cancel out, ideally.

[Kyle Miller]

Nelson Elhage said:

I don't feel like I fully understand why we can't reduce the match with a cast

You can reduce a match of a constructor application. There's a cast, so it's not a constructor application.

Casts can only reduce once the equality becomes a = a, both sides the same.

[Kyle Miller]

If you have some lemmas about cast, cons, and append, then you'd likely be able to push the cast into cons/append and reduce the match.

This is much harder to express using the triangle operator, given how generic it is.

[Eric Wieser]

Should _root_.cast also be preferred to the triangle? It seems to have more lemmas.

[Aaron Liu]

I don't like it

[Aaron Liu]

the triangle gives you access to a stronger proof

[Kyle Miller]

We don't want to be working with raw Eq.rec in terms, so can I say "neither" @Eric Wieser?

[Aaron Liu]

for example if you see cast ⋯ a in your goal you only know that Vector Nat n = Vector Nat m but if you see ⋯ ▸ a then you know that n = m

[Aaron Liu]

Kyle Miller said:

We don't want to be working with raw Eq.rec in terms, so can I say "neither" Eric Wieser?

why not?

[Kyle Miller]

Why do you know that n = m @Aaron Liu? It's just as unconstrained.

[Aaron Liu]

no since the term is (⋯ : n = m) ▸ a the proof is exposed compared to cast (⋯ : Vector Nat n = Vector Nat m) a it's buried inside a congrArg

[Aaron Liu]

of course if you have (⋯ : Vector Nat n = Vector Nat m) ▸ a then you're screwed

[Aaron Liu]

but most tactics don't look inside the proofs so having the equality be on the outside is a benefit

[Kyle Miller]

Ok, you're saying it's possible for it to be exposed. Sure.

The point still stands, Vector.cast is the way to go. That way you know for sure it will always be a Nat equality, and you stand a chance at writing lemmas about it that preserve the structure.

[Kyle Miller]

(Oh, hi @Nelson Elhage, just noticed who you were :wave: I remember you teaching me Scheme back in Jan 2009.)

[Aaron Liu]

You can write lemmas about the triangle too

[Aaron Liu]

And these lemmas apply universally whereas for custom cast functions may be nicer but you have to write the lemmas over and over again

[Aaron Liu]

Not saying it's bad to have custom cast functions just that we should also have lemmas about the triangle

[Aaron Liu]

Or docs#cast

[Nelson Elhage]

@Kyle Miller Ha, small world! The tables have turned, it seems :)

[Nelson Elhage]

You can reduce a match of a constructor application. There's a cast, so it's not a constructor application.

Casts can only reduce once the equality becomes a = a, both sides the same.

Okay, I think that was my first guess. So to the question of how/why cast_cast works, I'm guessing simp is able to use it to synthesize a cast back to the original type, and then get rid of the cast entirely via cast_eq (or the equivalent for the triangle)? Is that an accurate picture of what's going on there?

[Nelson Elhage]

(and in particular cast_cast lets you synthesize a cast and then merge the casts, at which point you have a no-op cast, which can be deleted via cast_eq)

[Kyle Miller]

Yeah, that's what it looks like it's doing. One cast uses n + (m + 1) = m + 1 + n, the next uses m + 1 + n = n + (m + 1), and the casts compose to be a single cast n + (m + 1) = n + (m + 1), and that's a no-op.

I checked simp? with Eric's proof, and that gives simp only [head, append', Nat.add_eq, cast_cast], so I guess simp doesn't end up eliminating the cast. What might be happening is that the no-op cast is definitionally equal to the identity function, so the match is able to reduce.

[Kyle Miller]

Here's an approach to it using split and some properties of heterogeneous equality:

theorem head_append''' {n m : Nat} (v : Vect α (m + 1)) (rhs : Vect α n) :
    head v = head (Nat.add_comm .. ▸ append' v rhs) := by
  cases v
  simp only [head, append']
  split
  rename_i h
  have := heq_of_eq h
  simp only [eqRec_heq_iff_heq] at this
  simp at this
  exact this.1

Sometimes it's easier to work with docs#HEq to start eliminating casts. Heterogeneous equality allows the types of the LHS and RHS to not be the same, and so it's able to "consume" the casts.

[Nelson Elhage]

One more question as I return to playing around and trying to build my understanding: Is there a way to make Lean expand the ⋯ in the output so I can see the full details of what's going on?

[Aaron Liu]

set_option pp.proofs true

[Nelson Elhage]

And is there a manual or reference I could have found that in? I looked in the reference manual but couldn't even find a mention of set_option or any list of common options.

[Aaron Liu]

no idea

[Kyle Miller]

If you hover over it in the Infoview it should tell you about the option

[Nelson Elhage]

I've been using the emacs mode instead of VS Code, which may be hamstringing me.

[Kyle Miller]

I'm an emacs user for everything but Lean. I find the UI to be too useful to give up, even though I still don't find editing in VS Code to completely comfortable.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Aaron Liu said:

And these lemmas apply universally whereas for custom cast functions may be nicer but you have to write the lemmas over and over again

I agree with Aaron here, but I think Eq.rec is not the right operator because, at least using the default triangle elaborator, you'll often end up with the relevant proof buried inside congrArgs. I made an elementary investigation into better operators that enforce that the proof you need is stored in the syntax as one of the arguments in this repo.

[Kyle Miller]

I haven't tried it, but there seems to be a fork of emacs-mode that people like: #lean4 > lean4-mode on eglot @ 💬

I'm not sure what the current state of emacs-mode development is. It would be nice to know if someone was actively maintaining it to have feature parity with the VS Code extension.