# Zulip Chat Archive

## Stream: new members

### Topic: Mutual recursioon madness

#### Ken Roe (Jul 25 2018 at 02:20):

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 (Jul 25 2018 at 02:29):

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

#### Kenny Lau (Jul 25 2018 at 02:29):

because you used `match`

#### Kevin Buzzard (Jul 25 2018 at 09:01):

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 (Jul 29 2018 at 10:26):

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 (Jul 29 2018 at 10:26):

thread is madness, mutual recursion is not

#### Kenny Lau (Jul 29 2018 at 10:51):

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 (Jul 29 2018 at 10:52):

changed the definition of `rangeSet`

and `rangeSetList`

Last updated: May 09 2021 at 19:11 UTC