Stream: Coq users

Topic: List Subset in Coq

Davis Silverman (Oct 29 2020 at 18:55):

Hi, is this a reasonable subset inductive proposition?

Inductive is_subset : list string -> list string -> Prop :=
  | subs_nil (xs : list string) : is_subset [] xs
  | subs_headmatch (xs ys : list string) (n:string) (H : is_subset xs ys)
    : is_subset (n::xs) (n::ys)
  | subs_rightextra (xs ys : list string) (n : string) (H : is_subset xs ys)
    : is_subset xs (n::ys)
.

Davis Silverman (Oct 29 2020 at 18:56):

I feel like im missing something in it, but not sure what

Yishuai Li (Oct 29 2020 at 21:31):

is_subset ["a";"b"] ["b";"a"] does not hold under your definition.

Yishuai Li (Oct 29 2020 at 21:33):

Try adding a rule like forall a b c, is_subset a c -> is_subset b c -> is_subset (a ++ b) c?

Yishuai Li (Oct 29 2020 at 21:34):

This would imply is_subset ["";""] [""], but that should be expected.

Last updated: Apr 20 2024 at 09:01 UTC