coq - ssreflect 反演，我需要两个方程而不是一个

Question

我有下一个定义(代码可以编译):

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]. *)

• 情况 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'。

但在我看来，我需要将它们一起使用。怎么做？

Answer 1

有一个way通过 ssreflect 策略使用inversion的力量。

Derive Inversion tjudgments_val_inv with (forall v t, tjudgments_val v t).

您可以将其与elim/tjudgments_val_inv: H一起使用。

此后证明就很简单了。