help please

Stream: general

[Michael Werman]

def rev {α : Type*}:
Π {n m}, vector α n → vector α m → vector α (m+n)
| 0 _ _ w := w
| (n+1) m (a :: v) w := rev v (a::w)

i get
equation type mismatch, term rev v (a :: w)
has type
vector α (m + 1 + n)
but is expected to have type
vector α (m + (n + 1))

[Johan Commelin]

yeah, this is annoying, because m + 1 + n = m + (n + 1), but not by definition.

[Johan Commelin]

So you will need to use a trick to move between vector \a x and vector \a y for x = y.

[Johan Commelin]

I've never used vector. Is there something called vector.cast or vector.congr?

[Johan Commelin]

docs#vector

[Mario Carneiro]

you can use eq.rec or rw of course

[Mario Carneiro]

which is enough to get over this hurdle

[Michael Werman]

where do i do this, eq.rec?

[Mario Carneiro]

do you have a #mwe? That code you wrote doesn't typecheck for me

[Mario Carneiro]

inductive {u} vector (α : Type u) : ℕ → Type u
| nil : vector 0
| cons {n} : α → vector n → vector (n+1)

local infixl `::` := vector.cons

def rev {α : Type*} : Π {n m}, vector α n → vector α m → vector α (m+n)
| 0 _ _ w := w
| (n+1) m (a :: v) w :=
  by rw ← nat.succ_add_eq_succ_add; exact rev v (a :: w)

[Kenny Lau]

#backticks

[Michael Werman]

is there any way to do something like this
not going through normal induction?

def f: ℕ → ℕ
|5 := 1
|_ := 1

example: ∀ (n: ℕ), f n =1
| 5 := rfl
| _ := rfl

[Eric Wieser]

#backticks

[Michael Werman]

is there any way to do something like this
not going through normal induction?

def f: ℕ → ℕ
|5 := 1
|_ := 1

example: ∀ (n: ℕ), f n =1
| 5 := rfl
| _ := rfl

[Kevin Buzzard]

A formal answer to your question is:

def f : ℕ → ℕ := λ _, 1

example (n: ℕ) : f n = 1 := rfl

Perhaps you might want to say more clearly what you mean.

[Michael Werman]

maybe this is a better example,
i want the proof to follow the way the function was built

def f: ℕ → ℕ
  |5 := 1
  |_ := 0

  example: ∀ (n: ℕ), (f n = 1) ∨ (f n = 0 )
  |5:=by simp *
  |n:=by simp *

[Kevin Buzzard]

And in what sense does the example you posted not follow the way the function was built?

[Kevin Buzzard]

Oh! It doesn't compile!

[Kevin Buzzard]

import tactic

def f: ℕ → ℕ
  |5 := 1
  |_ := 0

lemma hf (n : ℕ) : f n = if n = 5 then 1 else 0 :=
by delta f; refl

example (n: ℕ) : (f n = 1) ∨ (f n = 0 ) :=
begin
  rw hf,
  split_ifs;
  simp
end

This is probably not at all what you want.

[Kevin Buzzard]

But it does show that internally f is defined using an if/then statement.

[Johan Commelin]

@Michael Werman Is it an option for you to use

def f (n : ℕ) : ℕ :=
if n = 5 then 1 else 0

example (n : ℕ) : (f n = 1) ∨ (f n = 0) :=
if h : n = 5 then by simp [f,*] else by simp [f,*]

[Eric Wieser]

I was hoping the match _, rfl trick could help here, but it doesn't:

example (n: ℕ) : f n = 1 :=
match _, rfl : ∀ n', n' = n → _ with
  | 5, h5 := rfl
  | n, h_useless := sorry
end

[Eric Wieser]

This works but I don't think it's a great solution:

example (n: ℕ) : f n = 1 ∨ f n = 0 :=
match n, decidable.em _ : ∀ n', n' = 5 ∨ n' ≠ 5 → _ with
  | 5, _ := by simp [f]
  | _, or.inr h_not_5 := by simp [f, h_not_5]
end

[Michael Werman]

so the pattern matching doesnt know that it is an "if then else" by itself?

[Eric Wieser]

The pattern matching doesn't make h available that @Johan Commelin uses in his proof

[Kevin Buzzard]

This does seem like an artificial example though, with the 5. You can do

| 0 := ...
| 1 := ...
| (n + 2) := ...

and in this case the equation compiler (the thing doing the pattern matching) knows everything (as n+2>=2).

[Kenny Lau]

def f : ℕ → ℕ
| 5 := 1
| _ := 1

#print prefix f

example (n) (hn : n ≠ 5) : f n = 1 :=
begin
  rw f,
  -- ⊢ ¬n = 5
end

[Kenny Lau]

^ a sneak peek into Lean's mechanics

[Kevin Buzzard]

def f : ℕ → ℕ
| 5 := 0
| _ := 1

example : f 5 = 0 :=
begin
  rw f,
  /-
  ⊢ 1 = 0
  ⊢ ¬5 = 5
  -/
end

lol