Problem with Dependent pattern matching in COQ

Question

(small update to make it closer to my real task)

How to write f2 using dependent pattern matching? (Code below compiles except definition of f2)

Inductive parse_ret : Set :=
  No : parse_ret | Yes : parse_ret.

Inductive exp : parse_ret -> Set :=
| No_parse : exp No
| Yes_parse : exp Yes.

Definition f1 (p : parse_ret) : option (exp p) :=
  match p with
  | No => Some No_parse
  | Yes => Some Yes_parse
  end.
          
Definition f2' : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | Some Yes_parse => Some 1
  | None => None
  end.

So, f2' is almost what I need, but Some Yes_parse is obviously redundant here because we provided No constructor to f1 and f1's return type becomes option (exp No).

How to write definition for f2? avoiding the Non exhaustive pattern-matching error?

Definition f2 : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | None => None                            
  end.

Answer 1

I'm not very familiar with fancy match expressions, but, in this very specific case, it seems it would be easier to just use Some _ in the match. You could prove, if you need this, a lemma stating that f1 No is always Some No_parse.

You could also instead define f2 to take an argument of type option (exp No), and delegate the issue to the function caller.

Of course, all this may be stating the obvious...