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)
.
```

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

`is_subset ["a";"b"] ["b";"a"]`

does not hold under your definition.

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

?

This would imply `is_subset ["";""] [""]`

, but that should be expected.

Last updated: Jun 24 2024 at 13:02 UTC