Stream: Coq users

Topic: Relation with hypothesis

view this post on Zulip sara lee (Aug 11 2022 at 17:29):

2) I have locally generated list l1 and H1 related to this

H1: count_occ Nat.eq_dec
        match l1 with
        | [] => []
        | c :: t => c :: firstn m t
        end (S z) <=
      count_occ Nat.eq_dec
        match l1 with
        | [] => []
        | c :: t => c :: firstn m t
        end 0

z m c are nat. l1 is list nat.

2) I have an expression , then it it would be equal to below one (by using l1 from H1)

 (b :: firstn m l1)
   (b :: firstn m (c :: firstn m t))
  (b ::c::firstn m t)

3) Above can be helpful in proving

count_occ Nat.eq_dec (k1::firstn m l1) (S z) <= count_occ Nat.eq_dec  (k1 :: firstn m l1) 0

k1 is nat.

Last updated: Oct 01 2023 at 18:01 UTC