Stream: new members

Topic: Rewriting from def

Guilherme Espada (Mar 17 2021 at 10:35):

Why does the following example not work?

abbreviation ctxtype := list bool

def lookup_list : nat→ctxtype→ option bool
| n (head :: tail) := lookup_list (n-1) tail
| _ [] := none

theorem aaa {t} : lookup_list t ∅ ≠ none -> false :=
begin
intro a,
rw lookup_list at a, ---here
end


Thanks

Scott Morrison (Mar 17 2021 at 10:36):

The pattern matching sometimes splits into finer cases than you actually wrote.

Scott Morrison (Mar 17 2021 at 10:36):

I suspect that's happened here: it's doing a case split on the nat argument first, so there's no equation lemma for your case yet.

Scott Morrison (Mar 17 2021 at 10:37):

Try #print lookup_list to see what it actually produced.

Guilherme Espada (Mar 17 2021 at 10:39):

It prints out

def lookup_list._main : ℕ → ctxtype → option bool :=
λ (ᾰ : ℕ) (ᾰ_1 : ctxtype),
list.brec_on ᾰ_1
(λ (ᾰ : ctxtype) (_F : list.below bool ᾰ) (ᾰ_1 : ℕ),
(λ (ᾰ : ℕ) (ᾰ_1 : ctxtype) (_F : list.below bool ᾰ_1),
ite (ᾰ = 0)
(list.cases_on ᾰ_1 (λ (_F : list.below bool list.nil), id_rhs (option bool) none)
(λ (ᾰ_hd : bool) (ᾰ_tl : list bool) (_F : list.below bool (ᾰ_hd :: ᾰ_tl)),
id_rhs (option bool) (some ᾰ_hd))
_F)
(list.cases_on ᾰ_1 (λ (_F : list.below bool list.nil), id_rhs (option bool) none)
(λ (ᾰ_hd : bool) (ᾰ_tl : list bool) (_F : list.below bool (ᾰ_hd :: ᾰ_tl)),
id_rhs (option bool) (_F.fst.fst (ᾰ - 1)))
_F))
ᾰ_1
ᾰ
_F)
ᾰ


I'm not sure how to interpret it.

How do you suggest I fix it?

Scott Morrison (Mar 17 2021 at 10:39):

Write your own simp lemmas first, and don't rely on the behaviour of the pattern matcher? (I know that's pessimistic advice.)

Scott Morrison (Mar 17 2021 at 10:40):

Sorry, I guess you need to write #print prefix lookup_list

Scott Morrison (Mar 17 2021 at 10:41):

to see what equation lemmas it produced automatically. I agree the actual definition is not something a human should try to read. :-)

Guilherme Espada (Mar 17 2021 at 10:55):

It seems it's handling ∅ as different than list.nil
how can I convert between them

Kevin Buzzard (Mar 17 2021 at 10:58):

The empty set is a set, not a list.

Guilherme Espada (Mar 17 2021 at 10:59):

Ah, I see, makes sense.

Thanks

Last updated: May 12 2021 at 23:13 UTC