Zulip Chat Archive

Stream: new members

Topic: Inductive definitions


view this post on Zulip Ken Roe (Aug 28 2018 at 16:06):

I see a number of comments in my code that a definition of the form:

inductive allFirsts {t1} {t2} : list t1  list (t1 × t2)  Prop
 | AFNil : allFirsts list.nil list.nil
 | AFCons :  fx fy r r', allFirsts r r'  allFirsts (fx::r) ((fx,fy)::r')

can be rewritten as:

allFirsts l1 l2 <-> l2.map prod.fst = l1

The second form is not a complete definition. How can I use this form as a definition?

view this post on Zulip Chris Hughes (Aug 28 2018 at 16:11):

def allFirsts {t1 t2} (l1 : list t1) (l2 : list (t1 × t2)) : Prop := l2.map prod.fst = l1

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 16:20):

import tactic.interactive

inductive allFirsts {t1} {t2} : list t1  list (t1 × t2)  Prop
 | AFNil : allFirsts list.nil list.nil
 | AFCons :  fx fy r r', allFirsts r r'  allFirsts (fx::r) ((fx,fy)::r')

example {t1 t2} (l1 : list t1) (l2 : list (t1 × t2)) :
allFirsts l1 l2 <-> l2.map prod.fst = l1 :=
begin
  split,
    intro H,
    induction H,
    refl,
    simpa,
  intro H,
  induction H,
  induction l2 with f12 l2,
  exact allFirsts.AFNil,
  cases f12 with f1 f2,
  refine allFirsts.AFCons _ _ _ _ l2_ih,
end

Last updated: May 12 2021 at 05:19 UTC