Coq/SSReflect の case は、基本的には、帰納的に定義された前提を match 式でコンストラクタ毎に場合分けするのだが、 等式にたいして特別な振る舞いをする
Coq reference manual, SSReflect, case
マニュアルの例でいえば、(x, y) = (1, 2) -> G を x = 1 -> y = 2 -> G というように、 コンストラクタ (ここでは notation で (?,?) となっているが、具体的には prod 型の pair コンストラクタ) を外す機能がある
そういう、基本的な機能とは別の機能を割り当てても問題ないのかな、と考えると、 eq 型に対する match は rewrite だから、それはそれで別の tactic が割り当てられていて、 case でそれが使えなくなっても問題ないかな。 しかも、rewrite は左右どちらの方向に書き換えるかで2種類の使い方があって、 case ではその指定もできないし、と思った
ただ、case の基本的な機能を eq 型に対して使うとどうなるか確認してみる
From mathcomp Require Import all_ssreflect.
(* eq 型と同じ構造の型を自分で定義する *)
Inductive eq' (A : Type) (x : A) : forall _ : A, Prop := erefl' : eq' A x x.
Arguments eq' [_] _ _.
Lemma foo x y : eq' (x,y) (1,2) -> True.
(* eq' (x, y) (1, 2) -> True *)
case.
(* True *) (* ぬぅ、前提が消えてしまった *)
Show Proof.
(*
(fun (x y : nat) (__top_assumption_ : eq' (x, y) (1, 2)) =>
(fun
_evar_0_ : (fun a : nat * nat => fun=> True) (x, y) (erefl' (nat * nat) (x, y))
=>
match
__top_assumption_ as e in (eq' _ y0)
return ((fun a : nat * nat => fun=> True) y0 e)
with
| @erefl' _ _ => _evar_0_
end) ?Goal)
*) (* うぅむ、proof term は複雑で読みにくい *)
by [].
Defined.
(* proof term を beta reduction して単純にしてみる *)
Eval cbv beta delta [foo] in foo.
(*
= fun (x y : nat) (__top_assumption_ : eq' (x, y) (1, 2)) =>
match __top_assumption_ with
| @erefl' _ _ => I
end
: forall x y : nat, eq' (x, y) (1, 2) -> True
*)
(* erefl' は (eq' 型のパラメータ以外に) 引数がないから、新しい前提が何も得られないのだな *)
うぅむ、rewrite どころか、単に前提が消えるのか。 これはなんの役にも立たないな。 違う機能を割り当てても問題ないことがわかる
[latest]