Can't use inversion on inductive predicate

Question

I'm stuck on a simple proof about an inductive predicate. I have to prove that the natural 0 is not positive, where a natural is a list of bits, and 0 is any list with only bits that are 0s.

H1: pos Empt
____________ (1/1)
Nat

This chapter of Certified Programming with Dependents Types seems to suggest I use inversion, but I get an error message.

Require Import Coq.Program.Program.

Inductive Bit: Type :=
  | Zer: Bit
  | One: Bit.

Inductive List (type1: Type): Type :=
  | Empt: List type1
  | Fill: type1 -> List type1 -> List type1.

Implicit Arguments Empt [[type1]].

Implicit Arguments Fill [[type1]].

Definition Nat: Type := List Bit.

Inductive pos: Nat -> Prop :=
  | pos_1: forall nat1: Nat, pos (Fill One nat1)
  | pos_2: forall nat1: Nat, pos nat1 -> forall bit1: Bit, pos (Fill bit1 nat1).

Program Fixpoint pred (nat1: Nat) (H1: pos nat1): Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat2 => Fill One (pred nat2 H1)
  | Fill One nat2 => Fill Zer nat2
  end.

Next Obligation.
inversion H1.

Answer 1

Your Theorem T1 is not equivalent to the Obligation. In the latter, you're supposed to build an element of Nat, which itself is a Type (btw, why aren't you using Set here? You do not seem to be manipulating higher-order types in this development).

As the error message says, you cannot perform a case analysis (inversion is built upon that) on an element of Prop for that (see in particular section 4.5.4 of the Coq manual). However, in this case, you're not interested in building an actual Nat, you merely want to prove that this case is impossible. For that, you can apply False_rect (or False_rec if you choose to go with Set rather than Type), which will leave you to prove False. False being a Prop, you then can use inversion H1.

Note that there is a problem in the second branch of your definition of pred: you cannot use (pred nat2 H1), as H1 is not a proof of pos nat2. The easiest way is probably to leave an hole here also: (pred nat2 _), which can be trivially solved with an inversion (this time, you must build a term of type pos nat2, i.e. something that lives in Prop).