Search code examples
mathexpressioncoqsemantics

Arithmetic expressions and big-step semantic

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.

First i began with defining a type for valuations and i decided to do a list of string * Z

Definition valuation  := list (string * Z).

then i defined a function which is used to apply the valuation

Fixpoint apply_valuation (s : string) (v : valuation) : Z := 
match v with 
| nil => 0
| cons (s',v') q => if  (string_dec s' s) then v'
                else (apply_valuation s q)
end.

and this is how i defined my arithmetic expressions type :

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

And my inductive predicate for big-step semantic is

 Inductive Sem_AE (s : valuation) : EA -> Z -> 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 -> Sem_AE s e2 z2 -> Sem_AE s (Plus e1 e2) (z1 + z2)
| minus_sem : forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->  Sem_AE s e2 z2 ->  Sem_AE s (Minus e1 e2) (z1 - z2)
| mult_sem: forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->   Sem_AE s e2 z2 ->  Sem_AE s (Mult e1 e2) (z1 * z2)
| sem_Div : forall e1 e2 z1 z2 , 
         Sem_AE s e1 z1 ->  Sem_AE s e2 z2 -> Sem_AE s (Div e1 e2) (z1 / z2).

Now i have to prove that big-step semantic is deteministic, but i get stuck when it arrives to prove it for plus

Lemma sem_det: forall s a z z', Sem_AE s a z -> Sem_AE s a z' -> z = z'.
Proof.
intros. induction H.
- inversion H0. reflexivity.
- inversion H0. reflexivity.
- inversion H0. subst.

This is what i have in my context

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) -> z1 = z0 + z3
IHSem_EA2 : Sem_EA s e2 (z0 + z3) -> z2 = z0 + z3
______________________________________(1/1)
 z1 + z2 = z0 + z3

Any ideas how to continue this proof? and am i in the right path?

Thanks a lot.

Solution

  • This is a common gotcha. The problem is that your induction hypothesis is not general enough. You can fix this issue by generalizing over z':

    Lemma sem_det: forall s a z z', Sem_AE s a z -> Sem_AE s a z' -> z = z'.
Proof.
intros. generalize dependent z'. induction H; intros.
- inversion H0. reflexivity.
- inversion H0. reflexivity.
- inversion H1. subst.
  rewrite (IHSem_AE1 _ H4).
  now rewrite (IHSem_AE2 _ H6).

    It is instructive to compare the state of the generalized proof against your previous attempt. You can read the Software Foundations book for more information.

    Small tip: your proofs are relying on the names that Coq generates for you. You should never do this, since these choices are brittle and cause your proof scripts to break easily.