2

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

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'我。

但在我看来,我需要他们两个在一起。如何?

4

2 回答 2

3

有一种使用ssreflectinversion策略的方法。

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

您可以将它与elim/tjudgments_val_inv: H.

之后的证明就很简单了。

于 2021-09-16T15:58:32.963 回答
1

在这种情况下,您可以使用非常方便inversion的策略和增强case策略,它会自动执行您手动尝试执行的索引工作。到这里inversion H就差不多完成证明了。

于 2021-09-16T14:54:13.433 回答