天泣記

Coq の rewrite について少し考えた。

まず、rewrite の対象として自然数を扱う実験用に、命題の中に自然数を好き勝手に書けるよう、X という命題を用意する。 (なお証明したいわけではないので、証明できないものにしてある)

Definition X (n : nat) := False.

また、簡単な定理として、2 + 4 = 1 + 5 というもの L という名前で用意しておく。

Lemma L : 2 + 4 = 1 + 5.
reflexivity.
Qed.
Print L.
(*
L = @eq_refl nat (1 + 5)
     : 2 + 4 = 1 + 5
*)

X (1 + 5) という命題の証明の中で、rewrite<- L とすると、予想通り、L の右から左への書き換えなので、命題が X (2 + 4) に書き換えられる。証明項をみると、これは eq_rec という関数の呼び出しを構築するようだ。

Goal X (1 + 5).
rewrite<- L.
(* f (2 + 4) *)
Show Proof.
(* (@eq_rec nat (2 + 4) (fun n : nat => X n) ?Goal (1 + 5) L) *)
Abort.

では、直接 eq_rec の呼び出しを構築してみよう。ここでは refine を使う。これでも同様に命題は X (2 + 4) に書き換えられる。

Goal X (1 + 5).
refine (@eq_rec nat (2 + 4) (fun n => X n) _ (3+3) (@eq_refl nat (4+2))).
(* X (2 + 4) *)
Abort.

eq_rec の中身を調べてみよう。 eq_rec は eq_rect を呼び出している。

Print eq_rec.
(*
eq_rec =
fun (A : Type) (x : A) (P : A -> Set) => @eq_rect A x P
     : forall (A : Type) (x : A) (P : A -> Set),
       P x -> forall y : A, x = y -> P y
*)

eq_rect は dependent match になっている。

Print eq_rect.
(*
eq_rect =
fun (A : Type) (x : A) (P : A -> Type) (f : P x) (y : A) (e : x = y) =>
match e in (_ = y0) return (P y0) with
| eq_refl => f
end
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall y : A, x = y -> P y
*)

あと、eq の定義は以下のようになっている。

Print eq.
(*
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
*)

dependent match を直接構築してみよう。こうすると命題は (X (2 + 4) ではなく) X (4 + 2) に書き換えられる。まぁ、構築した証明項の中に 2 + 4 は入っていないので 2 + 4 が出てきたらそれは変だけど。こうなるのは、match の body の型は return X y の y を、コンストラクタの定義から取り出した情報で埋めたものになるからである。コンストラクタ (eq_refl) の定義では、x = x という型の値を構築するとなっていて、この右側が y に対応する。で、x には引数として 4+2 を与えているので y は 4+2 になるのだろう。

Goal X (1 + 5).
refine (
  match @eq_refl nat (4+2) in _ = y return X y with
  | eq_refl => _
  end).
(* X (4 + 2) *)
Abort.

cast すれば、X (2 + 4) にすることはできる。

Goal X (1 + 5).
refine (
  match @eq_refl nat (4+2) in _ = y return X y with
  | eq_refl => (_ : X (2 + 4))
  end).
(* X (2 + 4) *)
Abort.

天泣記

2018-07-10 (Tue)