この前の Proof Summit 2025 では、依存マッチで生成される連立方程式がコンストラクタと変数だけからなる等式なら単一化でどうにかできる (かも)、 という話をしたが、発表の中に出てきた (Lean のマニュアルからとってきた) EvenOddList はインデックスのところに negb というコンストラクタではない関数が入っているので その条件を満たさない。
これを場合分けできるかやってみよう。
From mathcomp Require Import all_ssreflect.
Import EqNotations.
Inductive EvenOddList (A : Type) : bool -> Type :=
| nil : EvenOddList A true
| cons : A -> forall (even : bool), EvenOddList A even -> EvenOddList A (negb even).
Lemma case_EvenOddList (A : Type) (P : forall (b : bool) (x : EvenOddList A b), Prop)
(Hnil : P true (nil A))
(Hcons : forall (b : bool) (a : A) (y : EvenOddList A b), P (~~ b) (cons A a b y))
(b : bool) (x : EvenOddList A b)
: P b x.
Proof.
refine (match x as x' in EvenOddList _ b'
return forall (Hb : b = b') (Hx : (rew Hb in x) = x'), P b x with
| nil => _
| cons _ _ _ => _
end erefl erefl).
(*
2 goals
A : Type
P : forall b : bool, EvenOddList A b -> Prop
Hnil : P true (nil A)
Hcons : forall (b : bool) (a : A) (y : EvenOddList A b), P (~~ b) (cons A a b y)
b : bool
x : EvenOddList A b
______________________________________(1/2)
forall Hb : b = true, rew [EvenOddList A] Hb in x = nil A -> P b x
______________________________________(2/2)
forall Hb : b = ~~ b0, rew [EvenOddList A] Hb in x = cons A a b0 e -> P b x
*)
move=> Hb.
subst b => /= Hx.
subst x.
exact Hnil.
move=> Hb.
(* Hb : b = ~~ b0 *)
subst b => /= Hx.
subst x.
exact (Hcons b0 a e).
Defined.
Check case_EvenOddList.
(*
case_EvenOddList
: forall (A : Type) (P : forall b : bool, EvenOddList A b -> Prop),
P true (nil A) ->
(forall (b : bool) (a : A) (y : EvenOddList A b), P (~~ b) (cons A a b y)) ->
forall (b : bool) (x : EvenOddList A b), P b x
*)
まぁ、できました。
ただ、ひとつ疑問がある。 cons の場合のところで、コンテキストに Hb : b = ~~ b0 があって subst b がこれを片付けてくれる (b を ~~ b0 に置換すると同時に、Hb を erefl に置換してくれる)。 しかし、 b = ~~ b0 は eq b (~~ b0) であり、パラメータが b でインデックスが ~~ b0 なので、 eq の場合分けはインデックスをパラメータに置換するので、~~ b0 を b に置換しようとしてうまくいかないはずである。
実際に試してみると、subst b のかわりに destruct Hb とするとやはり失敗する。
Lemma case_EvenOddList' (A : Type) (P : forall (b : bool) (x : EvenOddList A b), Prop)
(Hnil : P true (nil A))
(Hcons : forall (b : bool) (a : A) (y : EvenOddList A b), P (~~ b) (cons A a b y))
(b : bool) (x : EvenOddList A b)
: P b x.
Proof.
refine (match x as x' in EvenOddList _ b'
return forall (Hb : b = b') (Hx : (rew Hb in x) = x'), P b x with
| nil => _
| cons _ _ _ => _
end erefl erefl).
move=> Hb.
subst b => /= Hx.
subst x.
exact Hnil.
move=> Hb.
(* Hb : b = ~~ b0 *)
Fail destruct Hb.
(*
The command has indeed failed with message:
Abstracting over the terms "b1" and "Hb" leads to a term
fun (b2 : bool) (Hb0 : b = b2) => rew [EvenOddList A] Hb0 in x = cons A a b0 e -> P b x
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"EvenOddList A b2" : "Type"
"rew [EvenOddList A] Hb0 in x" : "EvenOddList A b2"
"cons A a b0 e" : "EvenOddList A (~~ b0)"
The 3rd term has type "EvenOddList A (~~ b0)" which should be a subtype of "EvenOddList A b2".
*)
subst に頼らずに自分でやるにはどうしたらいいか考えると、まぁ、等式の左右を逆にすればいいのである。 2回逆にするともとに戻るので、もともと Hb を使っていたところをそう書き変えて、1回逆にしたやつを destruct すればいいはずである。
逆にするのは SSReflect では esym であり、2回逆にすると戻るというのは esymK という補題がある。
About esym. (* forall {A : Type} {x y : A}, x = y -> y = x *)
About esymK (* forall [T : Type] [x y : T], cancel esym esym *).
vanilla Coq なら Logic.eq_sym と eq_sym_involutive である。
About Logic.eq_sym. (* forall [A : Type] [x y : A], x = y -> y = x *) About eq_sym_involutive. (* forall [A : Type] [x y : A] (e : x = y), Logic.eq_sym (Logic.eq_sym e) = e *)
で、esymK を使ってやってみるとやはりできた。
(* rew [EvenOddList A] Hb in x = cons A a b0 e -> P b x *) Check (@esymK _ b (~~ b0) Hb). (* esym (esym Hb) = Hb *) rewrite -(@esymK _ b (~~ b0) Hb). (* rew [EvenOddList A] esym (esym Hb) in x = cons A a b0 e -> P b x *) Check (esym Hb). (* ~~ b0 = b *) destruct (esym Hb) => /= Hx. subst x. exact (Hcons b0 a e).
Defined.
eq の場合わけをうまく使うために b = ~~ c の右辺を変数にしたいわけだが、 等式の左右を逆にするのではなく、右辺の negb (~~) を剥がして左辺にもってくることも考えられる。
今回は Hb : b = ~~ b0 の b が変数だったので左右を逆にするだけで右辺を変数にできたが、b が変数でない項だったらそれではうまくいかず、negb を左辺にもってきたいということもあるかもしれない。
結局のところ b = ~~ c と ~~ b = c は等価なので、相互に変換できるはずという話なのだが、これは実際そうで、SSReflect には以下の補題がある。
About negbLR. (* forall [b c : bool], b = ~~ c -> ~~ b = c *) About negbRL. (* forall [b c : bool], ~~ b = c -> b = ~~ c *)
しかしこれらは opaque で計算が進まないので、自前で証明しなおし、negbRL' (negbLR' H) = H を証明しておく。
Lemma negbLR' : forall [b c : bool], b = ~~ c -> ~~ b = c. Proof. by case ; case. Defined. Lemma negbRL' : forall [b c : bool], ~~ b = c -> b = ~~ c. Proof. by case; case. Defined. Lemma negbRLR : forall [b c : bool] (H : b = ~~ c), negbRL' (negbLR' H) = H. Proof. move=> b c H. subst b. by case: c. Qed.
これらを使うと、以下のように証明できた。
Lemma case_EvenOddList'' (A : Type) (P : forall (b : bool) (x : EvenOddList A b), Prop)
(Hnil : P true (nil A))
(Hcons : forall (b : bool) (a : A) (y : EvenOddList A b), P (~~ b) (cons A a b y))
(b : bool) (x : EvenOddList A b)
: P b x.
Proof.
refine (match x as x' in EvenOddList _ b'
return forall (Hb : b = b') (Hx : (rew Hb in x) = x'), P b x with
| nil => _
| cons _ _ _ => _
end erefl erefl).
move=> Hb.
subst b => /= Hx.
subst x.
exact Hnil.
move=> Hb.
(* rew [EvenOddList A] Hb in x = cons A a b0 e -> P b x *)
rewrite -(negbRLR Hb).
(* rew [EvenOddList A] negbRL' (negbLR' Hb) in x = cons A a b0 e -> P b x *)
Check negbLR' Hb. (* ~~ b = b0 *)
destruct (negbLR' Hb) => /=.
(* rew [EvenOddList A] negbRL' erefl in x = cons A a (~~ b) e -> P b x *)
destruct b => /= Hx.
subst x.
exact (Hcons false a e).
subst x.
exact (Hcons true a e).
Defined.
Hb を negbRL' (negbLR' Hb) に書き変えて、negbLR' Hb : ~~ b = b0 を destruct すると b0 が ~~ b に置換される (また negbLR' Hb が erefl になる)。
ただそこから、b : bool を場合分けしないと計算が進まない。 これは negbRL' が内部で引数を場合分けしているためで、具体的な値 (true あるいは false) にする必要がある。 b を場合分けして具体的な値にしてしまえば、あとは問題なく証明できる。
[latest]