coq - ProgramFixpointで定義された関数に関する簡単な事実を証明することはできません

Question

forall nat1: Nat, Trim nat1 -> Trim (pred nat1)以前、私は次のの定義を証明することができましたpred。

Fixpoint pred (nat1: Nat): Nat :=
  match nat1 with
  | Empt => Empt
  | Fill Zer nat3 => Fill One (pred nat3)
  | Fill One nat3 => trim (Fill Zer nat3)
  end.

しかし、次の新しい定義ではpred、証明する方法がわかりませんforall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1)。

Program Fixpoint pred (nat1: Nat | Trim nat1 /\ Pos nat1) {measure (meas nat1)}: Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat3 => Fill One (pred nat3)
  | Fill One nat3 => trim (Fill Zer nat3)
  end.

誰かが私にヒントを教えてもらえますか？で何かを証明することについては何も知りませんsig。または多分私は何か間違ったことをしています。知らない。完全なコードはここにあります。ここに前のコード。

Answer 1

カンニングすることにしました。

Fixpoint pred' (n1: Nat): Nat :=
  match n1 with
  | Empt => Empt
  | Fill Zer n1 => Fill One (pred' n1)
  | Fill One n1 => trim (Fill Zer n1)
  end.

Definition pred (n1: Nat) (H1: Trim n1) (H2: comp n1 zer = Great): Nat :=
  pred' n1.