## Stream: Beginner Questions

### Topic: evaluation value\theorem

#### Robert Soeldner (Jul 21 2021 at 17:48):

Actually, I was able to make some functions executable, e.g. running

``````value "Dang (fst r1)"
``````

prints the correct behavior

``````"⌈indeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T"
:: "form"
``````

but when trying to use the `Dang` fun in a theorem (equality in this case) like

``````lemma "(Dang (fst r1)) = (⌈indeg  ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg  ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T)"
``````

The remaining goal looks like

``````goal (1 subgoal):
1. (eval g undefined
(foldr
(λk a. ⌈indeg ↝⇩V k⌉ ⌈=⌉
▹⇩I foldr
(λka b.
if edge_trg
(the (if ka = Suc 0 then Some ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈
else [2 ↦ ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈] ka)) =
k
then Suc b else b)
(Mapping.ordered_keys
(AList_Mapping.Mapping
[(Suc 0, ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈),
(2, ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈)]))
0 ⌈∧⌉
⌈outdeg ↝⇩V k⌉ ⌈=⌉
....
``````

I guess, some simplification rules are missing (e.g. Mapping.ordered_keys, or AList_Mapping.Mapping). For me, the expected behavior would be that `simp` would equally evaluate. What peace am I missing?

#### Mathias Fleury (Jul 21 2021 at 19:05):

`apply code_simp`?

#### Robert Soeldner (Jul 21 2021 at 19:07):

yea ... actually this was what I was looking for, thanks again :-)

Last updated: Jun 20 2024 at 08:21 UTC