coq - Coq 中的递归函数

Question

Inductive my_type := 
| Type_pol : Z -> my_type
| Type_matrix : Z -> my_type.

Inductive redPair := 
| RedPair_interpretation : my_type -> redPair.

Inductive orderingProof := 
| OrderingProof_redPair : redPair -> orderingProof.

Inductive trsTerminationProof := 
| TrsTerminationProof_ruleRemoval : 
   orderingProof -> trsTerminationProof -> trsTerminationProof.

我想写一个函数

Definition return_mytype (t : my_type) : option nat :=
  match t with
   | Type_pol _ => None
   | Type_matrix i => Some (Z.to_nat i)
  end.
Definition return_redPair (r : redPair ) : option nat :=
  match r with
   | RedPair_interpretation mty => return_mytype mty
 end. 
Definition return_orderProof (d : orderingProof) : option nat :=
  match d with
  | OrderingProof_redPair r => return_redPair r
  end.

Definition return_trsTermProof (t : trsTerminationProof) : option nat :=
   match t with
    | TrsTerminationProof_ruleRemoval d _t => return_orderProof d
   end.

我想编写return_trsTermProof在这种情况下也可以工作的函数，不仅可以接受参数d，而且如果有t:trsTerminationProof例如

Fixpoint return_trsTermProof (t : trsTerminationProof) : option nat :=
   match t with
    | TrsTerminationProof_ruleRemoval d t => 
     (* I don't know how can I take the function (return_orderProof d) *) ...
     return_trsTermProof t 
   end.

Answer 1

你的意思是return_trsTermProof t_如果return_orderProof d退货你想退货none吗？

Fixpoint return_trsTermProof (t : trsTerminationProof) : option nat :=
  match t with
  | TrsTerminationProof_ruleRemoval d t_ =>
    match return_orderProof d with
    | None   => return_trsTermProof t_
    | Some n => Some n
    end
  end.

如果你的归纳集没有更多的构造函数，你也可以像这样定义它：

Fixpoint return_trsTermProof (t : trsTerminationProof) : option nat :=
  match t with
  | TrsTerminationProof_ruleRemoval (OrderingProof_redPair (RedPair_interpretation (Type_pol    z))) t_ => return_trsTermProof t_
  | TrsTerminationProof_ruleRemoval (OrderingProof_redPair (RedPair_interpretation (Type_matrix z))) t_ => Some (Z.to_nat z)
  end.