## Stream: general

### Topic: help please

#### Michael Werman (Dec 11 2020 at 09:49):

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 (Dec 11 2020 at 09:53):

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

#### Johan Commelin (Dec 11 2020 at 09:54):

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

#### Johan Commelin (Dec 11 2020 at 09:57):

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

docs#vector

#### Mario Carneiro (Dec 11 2020 at 09:58):

you can use eq.rec or rw of course

#### Mario Carneiro (Dec 11 2020 at 09:58):

which is enough to get over this hurdle

#### Michael Werman (Dec 11 2020 at 10:45):

where do i do this, eq.rec?

#### Mario Carneiro (Dec 11 2020 at 11:00):

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

#### Mario Carneiro (Dec 11 2020 at 11:04):

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)


#backticks

#### Michael Werman (Dec 17 2020 at 13:01):

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

#backticks

#### Michael Werman (Dec 17 2020 at 13:08):

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 (Dec 17 2020 at 13:09):

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 (Dec 17 2020 at 13:29):

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 (Dec 17 2020 at 13:29):

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

#### Kevin Buzzard (Dec 17 2020 at 13:29):

Oh! It doesn't compile!

#### Kevin Buzzard (Dec 17 2020 at 13:35):

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 (Dec 17 2020 at 13:35):

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

#### Johan Commelin (Dec 17 2020 at 13:36):

@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 (Dec 17 2020 at 13:37):

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 (Dec 17 2020 at 13:44):

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 (Dec 17 2020 at 13:47):

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

#### Eric Wieser (Dec 17 2020 at 13:51):

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

#### Kevin Buzzard (Dec 17 2020 at 13:59):

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 (Dec 17 2020 at 14:10):

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

#print prefix f

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


#### Kenny Lau (Dec 17 2020 at 14:11):

^ a sneak peek into Lean's mechanics

#### Kevin Buzzard (Dec 17 2020 at 14:23):

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

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


lol

Last updated: May 11 2021 at 23:11 UTC