Rewriting from def

Stream: new members

[Guilherme Espada]

Why does the following example not work?

abbreviation ctxtype := list bool

def lookup_list : nat→ctxtype→ option bool
| 0 (head :: tail) := some head
| 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]

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

[Scott Morrison]

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]

Try #print lookup_list to see what it actually produced.

[Guilherme Espada]

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]

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]

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

[Scott Morrison]

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

[Guilherme Espada]

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

[Kevin Buzzard]

The empty set is a set, not a list.

[Guilherme Espada]

Ah, I see, makes sense.

Thanks