Zulip Chat Archive

Stream: general

Topic: error with let substitution


view this post on Zulip Mohammed Eyad Kurd-Misto (Jun 03 2018 at 23:18):

Hello, I'm not sure if this is the correct place to post this. I am Mohammed Eyad Kurd-Misto, a PhD student at Chapman university. I am having an issue with a proof where the let construct does not seem to be working the way I would think. For two steps of the proof, I am simply substituting portions of the current statement from the let, and in one instance there is no issue but in another I am getting an error. The main relevant code is:

lemma flat_sharp {B : Type} : Π {n : ℕ}, ∀ (ps: @datum_or_data B ff n), (♭ (♯ ps)) = ps | 0 datum_or_data.nil := rfl | (n+1) (datum_or_data.cons p ps) := let ⟨as, h⟩ := ♯ ps, a := ♮⁻¹ p in --let (⟨as, h⟩ : vector B n) := (♯ ps : vector B n), a := ♮⁻¹ p in calc (♭ (♯ (datum_or_data.cons p ps))) = ♭ (vector.cons (♮⁻¹ p) (♯ ps)) : rfl ... = ♭ (vector.cons (a) (♯ ps)) : rfl --this works ... = ♭ (vector.cons (a) (⟨as, h⟩)) : rfl --@rfl (vector B n) -- this does not work? ... = datum_or_data.cons (♮ (a)) (♭ ⟨as, h⟩) : rfl ...

♭ and ♯ are operations for converting data from a vector to a 'datum_or_data' and vice versa so the goal here is simply to show they invert one another. ♮and ♮⁻¹ are operations for converting the individual elements of the data. I'm really not sure why I can't simply substitute ⟨as, h⟩ for ♯ ps since they are defined to be the same in the let and I have been unable to replicate anything similar where I can't simply substitute what is defined in the let construct. Any help would be greatly appreciated!

The error message given is:

Lean]
type mismatch at application
eq.trans (eq.trans (rfl (♭♯datum_or_data.cons p ps)) (rfl (♭(♮⁻¹p) :: ♯ps))) (rfl ?m_2)
term
rfl ?m_2
has type
?m_2 = ?m_2
but is expected to have type
(♭a :: ♯ps) = ♭a :: ⟨as, h⟩

Code to support this lemma is:

import data.vector

variable {α : Type} variable {x : α} variable {xs : list α}

lemma list_len_cancel {n :ℕ} (h : list.length (x::xs) = n+1) : list.length xs = n := nat.succ.inj h -- injectivity of successor

inductive datum_or_data {B : Type} : bool → ℕ → Type | sg (a : B) : datum_or_data tt 0 | nil : datum_or_data ff 0 | cons {n : ℕ} (a : datum_or_data tt 0) (as : datum_or_data ff n) : datum_or_data ff (n+1)

@[reducible] def datum_inv {B : Type} : @datum_or_data B tt 0 → B | (datum_or_data.sg x) := x

notation x := datum_or_data.sg x
notation ♮⁻¹ a := datum_inv a

@[reducible] definition vector_from_data {B : Type} : Π {n :ℕ }, @datum_or_data B ff n → vector B n | 0 _ := vector.nil | (n+1) (datum_or_data.cons p ps) := vector.cons (♮⁻¹ p) (vector_from_data ps)

@[reducible] definition data_from_vector {B : Type} : Π {n :ℕ }, vector B n → @datum_or_data B ff n | 0 _ := datum_or_data.nil | (n+1) ⟨(a::as), h⟩ := datum_or_data.cons (♮ a) (data_from_vector ⟨as,list_len_cancel h⟩ )

notation p := vector_from_data p
notation v := data_from_vector v

-- inverses @[simp] lemma natural {B : Type}: ∀ a : B, (♮⁻¹ (♮ a)) = a := assume a, rfl @[simp] lemma natural' {B: Type}: ∀ d : @datum_or_data B tt 0, (♮ (♮⁻¹ d)) = d | (♮ b) := rfl

--prove that flat and sharp are inverses lemma flat_sharp {B : Type} : Π {n : ℕ}, ∀ (ps: @datum_or_data B ff n), (♭ (♯ ps)) = ps | 0 datum_or_data.nil := rfl | (n+1) (datum_or_data.cons p ps) := let ⟨as, h⟩ := ♯ ps, a := ♮⁻¹ p in --let (⟨as, h⟩ : vector B n) := (♯ ps : vector B n), a := ♮⁻¹ p in calc (♭ (♯ (datum_or_data.cons p ps))) = ♭ (vector.cons (♮⁻¹ p) (♯ ps)) : rfl ... = ♭ (vector.cons (a) (♯ ps)) : rfl --this works ... = ♭ (vector.cons (a) (⟨as, h⟩)) : rfl --@rfl (vector B n) -- this does not work? ... = datum_or_data.cons (♮ (a)) (♭ ⟨as, h⟩) : rfl ... = datum_or_data.cons p (♭ (♯ ps)) : congr_arg (λ x, datum_or_data.cons x (♭ (♯ ps))) (natural' p) ... = datum_or_data.cons p ps : congr_arg (λ x, datum_or_data.cons p x) (flat_sharp ps)

view this post on Zulip Simon Hudon (Jun 03 2018 at 23:22):

The way you use the let is more like a match statement than a local definition. It works but it makes definitional equality a bit weird.

view this post on Zulip Simon Hudon (Jun 03 2018 at 23:24):

You might need to use an actual match statement an include an equality lemma in the match expression. I'll just try something and get back to you.

view this post on Zulip Simon Hudon (Jun 03 2018 at 23:25):

Btw, you might like to know that it's possible to have nice formatting of Lean code by enclosing it in backticks

view this post on Zulip Mohammed Eyad Kurd-Misto (Jun 03 2018 at 23:33):

Thank you, I reformatted the initial post (though the notation portions actually contain backticks in the lean code so I left them as is).

view this post on Zulip Simon Hudon (Jun 03 2018 at 23:35):

If you put three ticks before the first line and three after the last, you don't need to format it line by line. Even better: if you put three ticks followed by lean, you get syntax highlighting

view this post on Zulip Simon Hudon (Jun 03 2018 at 23:37):

What I think you should do is:

lemma flat_sharp {B : Type} : Π {n : },  (ps: @datum_or_data B ff n), ( ( ps)) = ps
| 0   datum_or_data.nil := rfl
| (n+1) (datum_or_data.cons p ps) :=
by cases h' :  ps with as h ;
  calc
    ( ( (datum_or_data.cons p ps))) =  (vector.cons (⁻¹  p) ( ps)) : rfl
    ...                 =  (vector.cons (a) ( ps)) : rfl   --this works
    ...                 =  (vector.cons (a) (as, h)) : rw h'
    ...                 = datum_or_data.cons ( (a)) ( as, h) : rfl
    ...

view this post on Zulip Mohammed Eyad Kurd-Misto (Jun 03 2018 at 23:55):

Thank you, I'll look at continuing the proof using cases/rw instead.


Last updated: May 13 2021 at 18:26 UTC