coq - 无法证明有关使用 Program Fixpoint 定义的函数的简单事实

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 |修剪 nat2//Pos nat2}，修剪(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 证明东西一无所知。或者也许我做错了什么。我不知道。完整代码为here 。上一个代码here .

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.