Coq 映射中的多个赋值给同一个值

Question

我得到了以下 com 定义，它可以在单个命令中将新值分配给多个变量。：

Inductive com : Type :=
  | CSkip
  | CAsgn (xs : list string) (es : list aexp) (* <--- NEW *)
  | CSeq (c1 c2 : com).
Notation "'skip'"  :=
         CSkip (in custom com at level 0) : com_scope.
Notation "xs := es"  :=
         (CAsgn xs es)
            (in custom com at level 0, xs constr at level 0,
             es at level 85, no associativity) : com_scope.
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity) : com_scope.
Inductive ceval1 : com -> state -> state -> Prop :=
  | E_Skip1 : forall st,
      st =[ skip ]=> st
  | E_Asgn_nil1  : forall st,
        st =[ nil := nil ]=> st
  | E_Asgn_cons1  : forall st st' a es n x xs,
      aeval st' a = n ->
      st =[ xs := es ]=> st' ->
      st =[ CAsgn (x :: xs) (a :: es) ]=> (x !-> n ; st')
  | E_Seq1 : forall c1 c2 st st' st'',
      st  =[ c1 ]=> st'  ->
      st' =[ c2 ]=> st'' ->
      st  =[ c1 ; c2 ]=> st''

  where "st =[ c ]=> st'" := (ceval1 c st st').

Reserved Notation
         "st '=[[' c ']]=>' st'"
         (at level 40, c custom com at level 99,
          st constr, st' constr at next level).

Inductive ceval2 : com -> state -> state -> Prop :=
  | E_Skip2 : forall st,
      st =[[ skip ]]=> st
  | E_Asgn_nil2  : forall st,
        st =[[ nil := nil ]]=> st
  | E_Asgn_cons2  : forall st st' a es n x xs,
      aeval st a = n ->
      st =[[ xs := es ]]=> st' ->
      st =[[ CAsgn (x :: xs) (a :: es) ]]=> (x !-> n ; st')
  | E_Seq2 : forall c1 c2 st st' st'',
      st  =[[ c1 ]]=> st'  ->
      st' =[[ c2 ]]=> st'' ->
      st  =[[ c1 ; c2 ]]=> st''

  where "st =[[ c ]]=> st'" := (ceval2 c st st').

我需要定义：

Definition c : com 
 := Admitted.

Definition st : state
  := Admitted.

Definition st1 : state
  := Admitted.

Definition st2 : state
 := Admitted.

这样我就可以证明以下引理：

Lemma states_neq : st1 <> st2.
Lemma ceval_example1: st =[ c ]=> st1.
Lemma ceval_example1: st =[[ c ]]=> st2.

此外，我还有这些预定义类型：

Inductive aexp : Type:=
| ANum (n : nat)
| AId (x : string)              
| APlus (a1 a2 : aexp)
| AMinus (a1 a2 : aexp)
| AMult (a1 a2 : aexp).
    
Inductive bexp : Type :=
| BTrue
| BFalse
| BEq (a1 a2 : aexp)
| BNeq (a1 a2 : aexp)
| BLe (a1 a2 : aexp)
| BGt (a1 a2 : aexp)
| BNot (b : bexp)
| BAnd (b1 b2 : bexp).

Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

和

Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if String.eqb x x' then v else m x'.

Notation "x '!->' v ';' m" := (t_update m x v)

我试过这个：

Definition c : com 
 := <{[X;X] := [ ANum 1; ANum 2]}>.

Definition st : state
  := empty_st.

Definition st1 : state
  := (X !-> 1;X !-> 2).

Definition st2 : state
 := (X !-> 2;X !->2).

证明

states_neq

和

ceval_example1

效果很好，但是当试图证明

ceval_example2

时，Coq 要求我在

1 = 2

:

时证明这种情况

Lemma ceval_example2:
  st =[[ c ]]=> st2.
Proof.
  unfold st,c,st2. 
  apply E_Asgn_cons2.

Answer 1

如果您的目标假设之一具有“1 = 2”的形状，则策略

discriminate

会放弃该目标。这是你的句子“the case when 1=2”出现并且可以处理的通常方式。

另一方面，如果“1=2”是您需要证明的结论，这通常表明您犯了错误，无论是在编写代码时，还是在假设某些行为实际上与您的代码不一致时.