1

有限集合の標準定義を使用します。

Inductive fin : nat -> Set :=
| F1 : forall {n : nat}, fin (S n)
| FS : forall {n : nat}, fin n -> fin (S n).

いくつかあると仮定しましょうP : forall {m : nat} (x y : fin m) : Set(重要なことは、 の両方の引数がP同じ型であるということです)。デモンストレーションのために、P を次のようにします。

Definition P {m : nat} (x y : fin m) := {x = y} + {x <> y}.

ここで、2 つの数値を比較するカスタム関数を作成します。

Fixpoint feq_dec {m : nat} (x y : fin m) : P x y.

アイデアは単純明快です: で and 、 for にマッチするxとy、x = F1簡単y = F1に等値を返します。 forx = FS x'では、 andy = FS y'の手続きを再帰的に呼び出します。x'y'

このアイデアを Coq に直接変換すると、明らかに失敗します。

refine (
  match x, y return P x y with
  | F1 _, F1 _ => _
  | FS _ x', F1 _ => _
  | F1 _, FS _ y' => _
  | FS _ x', FS _ y' => _
  end
).

(*
 * The term "y0" has type "fin n0" while it is expected to have type "fin n".
 *)

での試合中にx型y情報が失われるため、 に適用できませんP。型等価証明を渡す標準的なトリックは、ここでは役に立ちません。

refine (
  match x in fin mx, y in fin my return mx = my -> P x y with
  | F1 _, F1 _ => _
  | FS _ x', F1 _ => _
  | F1 _, FS _ y' => _
  | FS _ x', FS _ y' => _
  end eq_refl
).

(*
 * The term "y0" has type "fin my" while it is expected to have type "fin mx".
 *)

では、等価性の証明を使用しxて、 と同じ型 をキャストできるのではないでしょyうか?

Definition fcast {m1 m2 : nat} (Heq : m1 = m2) (x : fin m1) : fin m2.
Proof.
  rewrite <- Heq.
  apply x.
Defined.

また、後でキャストを削除できるようにする必要もあります。fcast eq_refl x = xしかし、任意の等価証明で機能させる必要があるため、それだけでは不十分であることに気付き ました。私が必要としているものを正確に実行する UIP と呼ばれるものを見つけました。

Require Import Coq.Program.Program.

Lemma fcast_void {m : nat} : forall (x : fin m) (H : m = m),
  fcast H x = x.
Proof.
  intros.
  rewrite -> (UIP nat m m H eq_refl).
  trivial.
Defined.

これで、定義全体を完了する準備ができました。

refine (
  match x in fin mx, y in fin my
  return forall (Hmx : m = mx) (Hmy : mx = my), P (fcast Hmy x) y with
  | F1 _, F1 _ => fun Hmx Hmy => _
  | FS _ x', F1 _ => fun Hmx Hmy => _
  | F1 _, FS _ y' => fun Hmx Hmy => _
  | FS _ x', FS _ y' => fun Hmx Hmy => _
  end eq_refl eq_refl
); inversion Hmy; subst; rewrite fcast_void.
- left. reflexivity.
- right. intro Contra. inversion Contra.
- right. intro Contra. inversion Contra.
- destruct (feq_dec _ x' y') as [Heq | Hneq].
  + left. apply f_equal. apply Heq.
  + right. intro Contra. dependent destruction Contra. apply Hneq. reflexivity.
Defined.

通じます！ただし、有用な値には評価されません。たとえば、次の例では、単純な値 (in_rightまたはin_left) ではなく、5 つのネストされた一致を持つ用語が生成されます。問題は、私が使用した UIP 公理にあると思われます。

Compute (@feq_dec 5 (FS F1) (FS F1)).

結局、私が思いついた定義はほとんど役に立ちません。また、2 つの値を同時にマッチングする代わりに、コンボイ パターンを使用してネストされたマッチングを試みましたが、同じ障害にぶつかりPました。他の方法でできますか？

4

2 に答える 2