Zulip Chat Archive

Stream: general

Topic: help please


view this post on Zulip 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))

view this post on Zulip Johan Commelin (Dec 11 2020 at 09:53):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 11 2020 at 09:57):

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

view this post on Zulip Johan Commelin (Dec 11 2020 at 09:58):

docs#vector

view this post on Zulip Mario Carneiro (Dec 11 2020 at 09:58):

you can use eq.rec or rw of course

view this post on Zulip Mario Carneiro (Dec 11 2020 at 09:58):

which is enough to get over this hurdle

view this post on Zulip Michael Werman (Dec 11 2020 at 10:45):

where do i do this, eq.rec?

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:00):

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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Dec 11 2020 at 11:04):

#backticks

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 17 2020 at 13:01):

#backticks

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 *

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 13:29):

Oh! It doesn't compile!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 13:35):

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

view this post on Zulip 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,*]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Michael Werman (Dec 17 2020 at 13:47):

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

view this post on Zulip Eric Wieser (Dec 17 2020 at 13:51):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 17 2020 at 14:11):

^ a sneak peek into Lean's mechanics

view this post on Zulip 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