title: Arithmetic expressions and big-step semantic
body: <p>I am working on a project where i have to define a type for arithmetic expressions and an inductive predicate for big-step operational semantic.</p>
  <p>First i began with defining a type for valuations and i decided to do a list of string * Z</p>
  <pre><code>Definition valuation  := list (string * Z).
  </code></pre>
  <p>then i defined a function which is used to apply the valuation</p>
  <pre><code>Fixpoint apply_valuation (s : string) (v : valuation) : Z := 
  match v with 
  | nil =&gt; 0
  | cons (s',v') q =&gt; if  (string_dec s' s) then v'
                  else (apply_valuation s q)
  end. 
  </code></pre>
  <p>and this is how i defined my arithmetic expressions type :</p>
  <pre><code>Inductive EA : Type := 
  | Cst (n : Z)
  | Var (v : string) 
  | Plus (a1 a2 : EA) 
  | Minus (a1 a2 : EA) 
  | Mult (a1 a2 : EA)
  | Div (a1 a2 : EA).
  </code></pre>
  <p>And my inductive predicate for big-step semantic is</p>
  <pre><code> Inductive Sem_AE (s : valuation) : EA -&gt; Z -&gt; Prop :=
  | cst_sem : forall z, Sem_AE s (Cst z) z
  | var_sem : forall v , Sem_AE s (Var v) (apply_valuation v s)
  | plus_sem : forall e1 e2 z1 z2 , 
            Sem_AE s e1 z1 -&gt; Sem_AE s e2 z2 -&gt; Sem_AE s (Plus e1 e2) (z1 + z2)
  | minus_sem : forall e1 e2 z1 z2 , 
           Sem_AE s e1 z1 -&gt;  Sem_AE s e2 z2 -&gt;  Sem_AE s (Minus e1 e2) (z1 - z2)
  | mult_sem: forall e1 e2 z1 z2 , 
           Sem_AE s e1 z1 -&gt;   Sem_AE s e2 z2 -&gt;  Sem_AE s (Mult e1 e2) (z1 * z2)
  | sem_Div : forall e1 e2 z1 z2 , 
           Sem_AE s e1 z1 -&gt;  Sem_AE s e2 z2 -&gt; Sem_AE s (Div e1 e2) (z1 / z2).
  </code></pre>
  <p>Now i have to prove that big-step semantic is deteministic, but i get stuck when it arrives to prove it for plus</p>
  <pre><code>Lemma sem_det: forall s a z z', Sem_AE s a z -&gt; Sem_AE s a z' -&gt; z = z'.
  Proof.
  intros. induction H.
  - inversion H0. reflexivity.
  - inversion H0. reflexivity.
  - inversion H0. subst.
  </code></pre>
  <p>This is what i have in my context</p>
  <pre><code>1 subgoals
  s : valuation
  e1 : EA
  e2 : EA
  z1 : Z
  z2 : Z
  H : Sem_EA s e1 z1
  H1 : Sem_EA s e2 z2
  z0 : Z
  z3 : Z
  H4 : Sem_EA s e1 z0
  H6 : Sem_EA s e2 z3
  H0 : Sem_EA s (Plus e1 e2) (z0 + z3)
  IHSem_EA1 : Sem_EA s e1 (z0 + z3) -&gt; z1 = z0 + z3
  IHSem_EA2 : Sem_EA s e2 (z0 + z3) -&gt; z2 = z0 + z3
  ______________________________________(1/1)
   z1 + z2 = z0 + z3
  </code></pre>
  <p>Any ideas how to continue this proof? and am i in the right path?</p>
  <p>Thanks a lot.</p>