Mutual recursioon madness

Stream: new members

[Ken Roe]

How do I complete the following theorem:

inductive Value : Type
| NatValue : ℕ -> Value
| ListValue : list Value -> Value
| NoValue : Value

mutual def rangeSet, rangeSetList
with rangeSet : Value -> option (list nat)
| (Value.ListValue ((Value.NatValue loc)::r)) :=
   match rangeSetList r with
   | option.some ll := option.some (loc::ll)
   | _              := option.none
   end
| (Value.NatValue _) := option.some list.nil
| _                  := option.none
with rangeSetList : list Value → option (list nat)
| (f::r) := match rangeSet f
                     with
                     | some l :=
                         match rangeSetList r with
                         | option.some ll := (some (append l ll))
                         | _ := option.none
                         end
                     | _     := option.none
                     end
| _ := @list.nil ℕ.

def beq_nat : ℕ → ℕ → bool
| 0 0 := tt
| (x+1) (y+1) := (beq_nat x y)
| (x+1) 0 := ff
| 0 (x+1) := ff

def listmem : ℕ → list ℕ → bool
| _ list.nil := ff
| e (list.cons a b) := if beq_nat e a then tt else listmem e b

def Rmember : ℕ → Value → bool
| a v := match (rangeSet v) with
         | option.some l := listmem a l
         | option.none := ff
         end

theorem rootIsMemberAux (root:ℕ) (r:list Value) :
        Rmember root (Value.ListValue (Value.NatValue root :: r)) = to_bool true :=
begin
    unfold Rmember, unfold rangeSet,
end

I cannot find a way to properly unfold Rmember.

[Kenny Lau]

after the definition, prove the relevant equations (and tag it as a simp lemma if you want)

[Kenny Lau]

because you used match

[Kevin Buzzard]

The philosophy is: the moment you write your definition, you should decide exactly which basic statements should be "true by definition" or "true because this is an immediate consequence of the definition with no additional arguments needed", formalise those statements, give them good names if possible, prove them with rfl or discover that they're not proved with rfl and then prove them using the equation lemmas generated by the equation compiler for you (the stuff called beq_nat._main.equation8 and stuff like that) and tag them with simp. Then your definition begins to behave the way you intuitively want it to behave. It has taken me about a year to understand this but I think I'm slowly getting it straight now.

[Kenny Lau]

theorem rootIsMemberAux_false
  (H : ∀ (root:ℕ) (r:list Value),
        Rmember root (Value.ListValue (Value.NatValue root :: r)) = to_bool true) :
  false :=
begin
  specialize H 0 [Value.NoValue],
  unfold Rmember rangeSet at H,
  apply bool.ff_ne_tt H
end

[Kenny Lau]

thread is madness, mutual recursion is not

[Kenny Lau]

inductive Value : Type
| NatValue  : ℕ → Value
| ListValue : list Value → Value
| NoValue   : Value

mutual def rangeSet, rangeSetList
with rangeSet : Value → option (list nat)
| (Value.ListValue ((Value.NatValue loc)::r)) :=
  match rangeSetList r with
  | option.some ll := some (loc::ll)
  | _              := some [loc]
  end
| (Value.NatValue _) := some []
| _                  := none
with rangeSetList : list Value → option (list nat)
| (f::r) := match rangeSet f with
  | some l := match rangeSetList r with
    | option.some ll := some (append l ll)
    | _ := none
    end
  | _     := rangeSetList r
  end
| _ := some []

def beq_nat : ℕ → ℕ → bool
| 0 0 := tt
| (x+1) (y+1) := (beq_nat x y)
| (x+1) 0 := ff
| 0 (x+1) := ff

def listmem : ℕ → list ℕ → bool
| _ list.nil := ff
| e (list.cons a b) := if beq_nat e a then tt else listmem e b

def Rmember : ℕ → Value → bool
| a v := match (rangeSet v) with
         | option.some l := listmem a l
         | option.none := ff
         end

theorem rootIsMemberAux (root:ℕ) (r:list Value) :
        Rmember root (Value.ListValue (Value.NatValue root :: r)) = to_bool true :=
begin
    unfold Rmember, unfold rangeSet,
    cases rangeSetList r;
    unfold rangeSet._match_1 Rmember._match_1 listmem;
    rw if_pos,
    { refl },
    { induction root with _ ih, constructor, apply ih },
    { refl },
    { induction root with _ ih, constructor, apply ih }
end

[Kenny Lau]

changed the definition of rangeSet and rangeSetList