Stream: Coq users

Topic: same result

view this post on Zulip zohaze (Apr 06 2023 at 12:43):

I have following functions, i am changing the
sequence/order of functions to show result will be same.

Fixpoint finding(l1 l2: list nat) : bool :=
 match l1 with
 | nil=> false
 |k::t'=>  if In k l2 then true else finding t' l2
eq1: a::a1::t <>[]
eq2: f2 (a :: a1 :: f1 a t) = b :: b1 :: l' ->
eq3: finding (f3 b (b1 :: l')) (b1 :: l') = true->
goal statement f2 (f1 a1 (f3  a1 (a :: a1 :: t))))  = b :: b1 :: l'

In k l2 is boolean form of In predicate. I want to ask how to start?

Last updated: Oct 04 2023 at 22:01 UTC