Stream: Coq users

Topic: use of tactic?

zohaze (Mar 24 2023 at 07:23):

Output argument of f1 is list. But f1 depends on f2.

match
       f1 (c :: f2 k (c' :: l3))
     with
     | [] => false
     | [r0] => true
     | r0 :: (_ :: _) as l5 =>

To simplify above ,what step i should take?
1) induction (f1 (c :: f2 k (c' :: l3)))
2) unfold f2.
3) match l5 with []=true (meaning of this statement? c exist and c' does not exist or under what condition l5 is nil and it is true?

Last updated: Oct 04 2023 at 23:01 UTC