Multiple Assignements in a Coq Map to the same value

Question

I'm given the following definition of com that sssigns new values to more than one variable in a single command.:

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').

I need to define:

Definition c : com 
 := Admitted.

Definition st : state
  := Admitted.

Definition st1 : state
  := Admitted.

Definition st2 : state
 := Admitted.

such that I can prove the following lemmas:

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

In addition, I have these predefined types:

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".

and

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)

I've tried this:

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

proving states_neq and ceval_example1 works fine, but when trying to prove ceval_example2, Coq asks me to prove the case when 1 = 2:

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

Answer 1

If one of the hypotheses of your goal has the shape "1 = 2" then the tactic discriminate discards this goal. This is the usual way in which your sentence "the case when 1=2" turns up and is treatable.

If on the other hand, "1=2" is the conclusion you need to prove, this is usually the sign that you made a mistake, either in writing your code, or in supposing some behavior which is actually not consistent with your code.

Answer 2

It seems that you are following the chapter Imp in the book Software Foundations, right (I managed to make your code work but made some slight modification)?

From LF Require Import Maps.
From LF Require Import Imp.
Require Import String.
Require Import List.

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).
Notation "xs := es"  :=
         (CAsgn xs es)
            (in custom com at level 0, xs constr at level 0,
             es at level 85, no associativity).
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity).

Reserved Notation
         "st '=[' c ']=>' st'"
         (at level 40, c custom com at level 99,
          st constr, st' constr at next level).
 
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 W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

Definition st : state
  := empty_st.

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

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

Lemma ceval_example2:
forall c, c = CAsgn (X :: X :: nil) (ANum 1 :: ANum 2 :: nil) ->
  st =[[ c ]]=> st2.
Proof.
  intros. subst.
  unfold st, st2.
  apply E_Asgn_cons2. simpl.

(BTW, I don't see why ceval1 should be defined, it seems irrelevant here.) Now the goal becomes 1 = 2.

Your command c is defined in a way that assigns X with two different values, in which case we need to see how your ceval2 is defined.

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')

Instantiating each variable we know that a = ANum 1 and n = 2, but your rule states that assigning a to x makes x updated to what a evaluates to. Why ANum 1 -> 2? This doesn't seem right. The reason why this happens is that you have written the wrong proposition that can never be proved.

Instead, this lemma is provable under your inductive rules.

Lemma ceval_example2:
forall c, c = CAsgn (X :: X :: nil) (ANum 1 :: ANum 2 :: nil) ->
  st =[[ c ]]=> st1.
Proof.
  intros. subst.
  repeat (constructor; auto).
Qed.