Inductive definitions

Stream: new members

[Ken Roe]

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?

[Chris Hughes]

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

[Kevin Buzzard]

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