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: Dec 20 2023 at 11:08 UTC