ssreflect inversion操作如何同时获取值与类型两个相等式？

背景定义 #

你拥有如下可编译的Coq代码定义：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Set Asymmetric Patterns.

Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive val : Set := VConst of nat | VPair of val & val.
Inductive type : Set := TNat | TPair of type & type.

Inductive tjudgments_val : val -> type -> Prop :=
| TJV_nat n :
    tjudgments_val (VConst n) TNat
| TJV_pair v1 t1 v2 t2 : 
    tjudgments_val v1 t1 ->
    tjudgments_val v2 t2 ->
    tjudgments_val (VPair v1 v2) (TPair t1 t2).

待证明引理 #

你需要证明的目标引理如下：

Lemma tjexp_pair v1 t1 v2 t2 (H : tjudgments_val (VPair v1 v2) (TPair t1 t2)) :
  tjudgments_val v1 t1 /\ tjudgments_val v2 t2.
Proof.
  case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2].
  (* case E: _ / H => // [v1' t1' v2' t2' jv1 jv2]. *)

遇到的问题 #

• 使用case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2].仅能得到等式E : VPair v1 v2 = VPair v1' v2'
• 使用case E: _ / H => // [v1' t1' v2' t2TPair t1 t2 = TPair t1' t2'' jv1 jv2].仅能得到等式E : TPair t1 t2 = TPair t1' t2'

解决方法 #

你可以在case tactic中显式为两个参数分别指定等式绑定变量，写法如下：

case E1: _ E2: _ / H => // [v1' t1' v2' t2' jv1 jv2].

执行后会同时得到两个等式：

• E1 : VPair v1 v2 = VPair v1' v2'
• E2 : TPair t1 t2 = TPair t1' t2'

后续用injection处理这两个等式导出等量关系，替换后即可完成证明，完整参考代码如下：

Lemma tjexp_pair v1 t1 v2 t2 (H : tjudgments_val (VPair v1 v2) (TPair t1 t2)) :
  tjudgments_val v1 t1 /\ tjudgments_val v2 t2.
Proof.
case E1: _ E2: _ / H => // [v1' t1' v2' t2' jv1 jv2].
by injection E1 E2 => -> -> -> ->; split.
Qed.

内容的提问来源于stack exchange，提问作者Andrey