Zulip Chat Archive

Stream: new members

Topic: Rewriting from def


view this post on Zulip Guilherme Espada (Mar 17 2021 at 10:35):

Why does the following example not work?

abbreviation ctxtype := list bool

def lookup_list : natctxtype 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

view this post on Zulip Scott Morrison (Mar 17 2021 at 10:36):

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

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 10:37):

Try #print lookup_list to see what it actually produced.

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

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 10:40):

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

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

view this post on Zulip Guilherme Espada (Mar 17 2021 at 10:55):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:58):

The empty set is a set, not a list.

view this post on Zulip Guilherme Espada (Mar 17 2021 at 10:59):

Ah, I see, makes sense.

Thanks


Last updated: May 12 2021 at 23:13 UTC