## Stream: new members

#### 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: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